---

Step * of Lemma coprime-exp1

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

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

2
.....upcase..... 
1. a : ℤ
2. b : ℤ
3. CoPrime(a,b)
4. n : ℤ
5. [%2] : 0 < n
6. CoPrime(a,b^(n - 1))
⊢ 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