Nuprl Lemma : coprime-equiv-unique-pair

`∀[p:ℤ]. ∀[q:ℤ-o]. ∀[a,b:ℤ].`
`  (<p, q> = <a, b> ∈ (ℤ × ℤ-o)) supposing `
`     ((q < 0 `⇐⇒` b < 0) and `
`     (p < 0 `⇐⇒` a < 0) and `
`     ((p * b) = (a * q) ∈ ℤ) and `
`     CoPrime(a,b) and `
`     CoPrime(p,q))`

Proof

Definitions occuring in Statement :  coprime: `CoPrime(a,b)` int_nzero: `ℤ-o` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` pair: `<a, b>` product: `x:A × B[x]` multiply: `n * m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` int_nzero: `ℤ-o` implies: `P `` Q` rev_implies: `P `` Q` nequal: `a ≠ b ∈ T ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` prop: `ℙ` guard: `{T}`
Lemmas referenced :  int_nzero_wf coprime_wf iff_wf nequal_wf equal_wf int_formula_prop_eq_lemma intformeq_wf decidable__equal_int less_than_wf int_formula_prop_wf int_formual_prop_imp_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformimplies_wf itermConstant_wf itermVar_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt int_nzero_properties coprime-equiv-unique
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality setElimination rename independent_isectElimination hypothesis independent_pairFormation lambdaFormation dependent_functionElimination natural_numberEquality unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll independent_pairEquality dependent_set_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry multiplyEquality

Latex:
\mforall{}[p:\mBbbZ{}].  \mforall{}[q:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[a,b:\mBbbZ{}].
(<p,  q>  =  <a,  b>)  supposing
((q  <  0  \mLeftarrow{}{}\mRightarrow{}  b  <  0)  and
(p  <  0  \mLeftarrow{}{}\mRightarrow{}  a  <  0)  and
((p  *  b)  =  (a  *  q))  and
CoPrime(a,b)  and
CoPrime(p,q))

Date html generated: 2016_05_15-PM-10_36_28
Last ObjectModification: 2016_01_16-PM-09_37_34

Theory : rationals

Home Index