---

Step * of Lemma exp_functionality_wrt_eqmod

No Annotations
∀m,i,j:ℤ.  ((i ≡ j mod m) ⇒ (∀n:ℕ. (i^n ≡ j^n mod m)))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN TACTIC:InductionOnNat) }

1
.....basecase..... 
1. m : ℤ
2. i : ℤ
3. j : ℤ
4. i ≡ j mod m
⊢ i^0 ≡ j^0 mod m

2
.....upcase..... 
1. m : ℤ
2. i : ℤ
3. j : ℤ
4. i ≡ j mod m
5. n : ℤ
6. [%2] : 0 < n
7. i^(n - 1) ≡ j^(n - 1) mod m
⊢ i^n ≡ j^n mod m

---

Latex:

---

Latex:
No  Annotations
\mforall{}m,i,j:\mBbbZ{}.    ((i  \mequiv{}  j  mod  m)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (i\^{}n  \mequiv{}  j\^{}n  mod  m)))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))  THEN  TACTIC:InductionOnNat)

---

Home Index