---

Step * 2 1 1 of Lemma exp-rem-property

.....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
BY
{ (InstLemma `rem_bounds_1` [⌜n⌝;⌜2⌝]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
.....equality..... 
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{}  n  rem  2  \msim{}  1


By

---

Latex:
(InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index