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