Nuprl Lemma : coprime_functionality_wrt_eqmod2

a,a',m:ℤ.  ((a' ≡ mod m)  (CoPrime(m,a') ⇐⇒ CoPrime(m,a)))


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m coprime: CoPrime(a,b) all: x:A. B[x] iff: ⇐⇒ Q implies:  Q int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q member: t ∈ T rev_implies:  Q uall: [x:A]. B[x] prop:
Lemmas referenced :  coprime_inversion coprime_wf iff_wf eqmod_wf coprime_functionality_wrt_eqmod
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut addLevel sqequalHypSubstitution productElimination thin independent_pairFormation impliesFunctionality lemma_by_obid dependent_functionElimination hypothesisEquality hypothesis independent_functionElimination because_Cache isectElimination intEquality

Latex:
\mforall{}a,a',m:\mBbbZ{}.    ((a'  \mequiv{}  a  mod  m)  {}\mRightarrow{}  (CoPrime(m,a')  \mLeftarrow{}{}\mRightarrow{}  CoPrime(m,a)))



Date html generated: 2016_05_14-PM-04_22_41
Last ObjectModification: 2015_12_26-PM-08_18_34

Theory : num_thy_1


Home Index