---

Step * of Lemma coprime-exp1

∀a,b:ℤ.  (CoPrime(a,b) ⇒ (∀n:ℕ. CoPrime(a,b^n)))
BY
{ (InductionOnNat THEN Reduce 0) }

1
1. a : ℤ@i
2. b : ℤ@i
3. CoPrime(a,b)@i
⊢ CoPrime(a,1)

2
.....upcase..... 
1. a : ℤ@i
2. b : ℤ@i
3. CoPrime(a,b)@i
4. n : ℤ@i
5. [%2] : 0 < n@i
6. CoPrime(a,b^n - 1)@i
⊢ CoPrime(a,b^n)

---

Latex:

---

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


By

---

Latex:
(InductionOnNat  THEN  Reduce  0)

---

Home Index