Nuprl Lemma : coprime_symmetry

a,b:ℤ.  (CoPrime(a,b)  CoPrime(b,a))


Proof




Definitions occuring in Statement :  coprime: CoPrime(a,b) all: x:A. B[x] implies:  Q int:
Definitions unfolded in proof :  coprime: CoPrime(a,b) all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x]
Lemmas referenced :  gcd_p_wf gcd_p_sym
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality natural_numberEquality hypothesis intEquality dependent_functionElimination independent_functionElimination

Latex:
\mforall{}a,b:\mBbbZ{}.    (CoPrime(a,b)  {}\mRightarrow{}  CoPrime(b,a))



Date html generated: 2016_05_15-PM-04_49_47
Last ObjectModification: 2015_12_27-PM-02_35_40

Theory : general


Home Index