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