Nuprl Lemma : coprime-mod

n:ℕ+. ∀x:ℤ.  (CoPrime(n,x) ⇐⇒ CoPrime(n,x mod n))


Proof




Definitions occuring in Statement :  coprime: CoPrime(a,b) modulus: mod n nat_plus: + all: x:A. B[x] iff: ⇐⇒ Q int:
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q implies:  Q prop: uall: [x:A]. B[x] nat_plus: + rev_implies:  Q subtype_rel: A ⊆B
Lemmas referenced :  mod-eqmod nat_plus_wf coprime_wf coprime_functionality_wrt_eqmod2 modulus_wf_int_mod int-subtype-int_mod iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis intEquality independent_pairFormation isectElimination setElimination rename because_Cache addLevel productElimination impliesFunctionality applyEquality sqequalRule independent_functionElimination

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbZ{}.    (CoPrime(n,x)  \mLeftarrow{}{}\mRightarrow{}  CoPrime(n,x  mod  n))



Date html generated: 2018_05_21-PM-01_09_50
Last ObjectModification: 2018_01_28-PM-02_03_36

Theory : num_thy_1


Home Index