---

Step * of Lemma coprime-mod

∀n:ℕ+. ∀x:ℤ.  (CoPrime(n,x) ⇐⇒ CoPrime(n,x mod n))
BY
{ ((UnivCD THENA Auto) THEN (Assert (x mod n) ≡ x mod n BY (BLemma `mod-eqmod` THEN Auto))) }

1
1. n : ℕ+@i
2. x : ℤ@i
3. (x mod n) ≡ x mod n
⊢ CoPrime(n,x) ⇐⇒ CoPrime(n,x mod n)

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Assert  (x  mod  n)  \mequiv{}  x  mod  n  BY  (BLemma  `mod-eqmod`  THEN  Auto)))

---

Home Index