Nuprl Lemma : qrep-coprime

`∀[r:ℚ]. (|gcd(fst(qrep(r));snd(qrep(r)))| = 1 ∈ ℤ)`

Proof

Definitions occuring in Statement :  qrep: `qrep(r)` rationals: `ℚ` gcd: `gcd(a;b)` absval: `|i|` uall: `∀[x:A]. B[x]` pi1: `fst(t)` pi2: `snd(t)` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  false: `False` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` bfalse: `ff` pi2: `snd(t)` pi1: `fst(t)` it: `⋅` unit: `Unit` bool: `𝔹` spreadn: spread3 btrue: `tt` ifthenelse: `if b then t else f fi ` has-valueall: `has-valueall(a)` has-value: `(a)↓` callbyvalueall: callbyvalueall nat: `ℕ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` top: `Top` implies: `P `` Q` qmul: `r * s` qinv: `1/r` qrep: `qrep(r)` qdiv: `(r/s)` prop: `ℙ` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` not: `¬A` cand: `A c∧ B` nat_plus: `ℕ+` exists: `∃x:A. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` gcd_p: `GCD(a;b;y)` coprime: `CoPrime(a,b)` assoced: `a ~ b` absval: `|i|` rev_implies: `P `` Q` true: `True` less_than': `less_than'(a;b)` le: `A ≤ B` squash: `↓T` iff: `P `⇐⇒` Q` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)`
Lemmas referenced :  le_wf assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert assert_of_le_int eqtt_to_assert bool_wf le_int_wf gcd_reduce_wf gcd_reduce_property evalall-sqequal product-valueall-type evalall-reduce int-valueall-type valueall-type-has-valueall nat_wf nat_plus_wf pi2_wf equal_wf pi1_wf_top qrep_wf gcd_wf absval_wf equal-wf-T-base int_subtype_base rationals_wf equal-wf-base not_wf qeq_wf2 assert_wf int-subtype-rationals assert-qeq nat_plus_properties q-elim one_divs_any gcd_is_divisor_2 gcd_is_divisor_1 iff_weakening_equal false_wf absval_pos assoced_elim coprime_bezout_id1 coprime_bezout_id2 nat_properties decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermAdd_wf itermMultiply_wf itermMinus_wf itermVar_wf itermConstant_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_minus_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf
Rules used in proof :  cumulativity instantiate promote_hyp dependent_pairFormation equalityElimination unionElimination multiplyEquality closedConclusion baseApply productEquality isintReduceTrue callbyvalueReduce lambdaEquality independent_functionElimination equalityTransitivity voidEquality voidElimination isect_memberEquality independent_pairEquality intEquality lambdaFormation applyLambdaEquality equalitySymmetry hyp_replacement baseClosed because_Cache independent_isectElimination natural_numberEquality sqequalRule applyEquality impliesFunctionality addLevel rename setElimination hypothesis isectElimination productElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_pairFormation imageMemberEquality dependent_set_memberEquality levelHypothesis equalityUniverse imageElimination minusEquality dependent_pairFormation_alt approximateComputation lambdaEquality_alt int_eqEquality Error :memTop,  universeIsType equalityIstype inhabitedIsType sqequalBase productIsType

Latex:
\mforall{}[r:\mBbbQ{}].  (|gcd(fst(qrep(r));snd(qrep(r)))|  =  1)

Date html generated: 2020_05_20-AM-09_13_18
Last ObjectModification: 2020_02_01-AM-11_26_41

Theory : rationals

Home Index