---

Step * 2 1 of Lemma exp-rem-property


1. m : ℕ+
2. n : {1...}
3. n rem 2 ≠ 0
4. ∀n:ℕn. ∀[i:ℕ]. (exp-rem(i;n;m) ~ i^n rem m)
5. ¬(n = 1 ∈ ℤ)
6. ∀[i:ℕ]. (exp-rem(i;n ÷ 2;m) ~ i^(n ÷ 2) rem m)
7. i : ℕ
8. i^n = (i^(n rem 2) * i^(n ÷ 2) * i^(n ÷ 2)) ∈ ℤ
⊢ (i * (i^(n ÷ 2) rem m) * (i^(n ÷ 2) rem m) rem m) = (i^(n rem 2) * i^(n ÷ 2) * i^(n ÷ 2) rem m) ∈ ℤ
BY
{ Subst' n rem 2 ~ 1 0⋅ }

1
.....equality..... 
1. m : ℕ+
2. n : {1...}
3. n rem 2 ≠ 0
4. ∀n:ℕn. ∀[i:ℕ]. (exp-rem(i;n;m) ~ i^n rem m)
5. ¬(n = 1 ∈ ℤ)
6. ∀[i:ℕ]. (exp-rem(i;n ÷ 2;m) ~ i^(n ÷ 2) rem m)
7. i : ℕ
8. i^n = (i^(n rem 2) * i^(n ÷ 2) * i^(n ÷ 2)) ∈ ℤ
⊢ n rem 2 ~ 1

2
1. m : ℕ+
2. n : {1...}
3. n rem 2 ≠ 0
4. ∀n:ℕn. ∀[i:ℕ]. (exp-rem(i;n;m) ~ i^n rem m)
5. ¬(n = 1 ∈ ℤ)
6. ∀[i:ℕ]. (exp-rem(i;n ÷ 2;m) ~ i^(n ÷ 2) rem m)
7. i : ℕ
8. i^n = (i^(n rem 2) * i^(n ÷ 2) * i^(n ÷ 2)) ∈ ℤ
⊢ (i * (i^(n ÷ 2) rem m) * (i^(n ÷ 2) rem m) rem m) = (i^1 * i^(n ÷ 2) * i^(n ÷ 2) rem m) ∈ ℤ

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  n  :  \{1...\}
3.  n  rem  2  \mneq{}  0
4.  \mforall{}n:\mBbbN{}n.  \mforall{}[i:\mBbbN{}].  (exp-rem(i;n;m)  \msim{}  i\^{}n  rem  m)
5.  \mneg{}(n  =  1)
6.  \mforall{}[i:\mBbbN{}].  (exp-rem(i;n  \mdiv{}  2;m)  \msim{}  i\^{}(n  \mdiv{}  2)  rem  m)
7.  i  :  \mBbbN{}
8.  i\^{}n  =  (i\^{}(n  rem  2)  *  i\^{}(n  \mdiv{}  2)  *  i\^{}(n  \mdiv{}  2))
\mvdash{}  (i  *  (i\^{}(n  \mdiv{}  2)  rem  m)  *  (i\^{}(n  \mdiv{}  2)  rem  m)  rem  m)  =  (i\^{}(n  rem  2)  *  i\^{}(n  \mdiv{}  2)  *  i\^{}(n  \mdiv{}  2)  rem  m)


By

---

Latex:
Subst'  n  rem  2  \msim{}  1  0\mcdot{}

---

Home Index