Nuprl Lemma : coprime-equiv-unique-pair

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


Definitions occuring in Statement :  coprime: CoPrime(a,b) int_nzero: -o less_than: a < b uimplies: supposing a uall: [x:A]. B[x] iff: ⇐⇒ Q pair: <a, b> product: x:A × B[x] multiply: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a iff: ⇐⇒ Q and: P ∧ Q int_nzero: -o implies:  Q rev_implies:  Q nequal: a ≠ b ∈  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

\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 

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

Theory : rationals

Home Index