---

Step * 1 1 1 1 of Lemma p-adic-inv-lemma1


∀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)
⊢ CoPrime(a,1)

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