---

Step * 2 of Lemma exp-rem-property


1. m : ℕ+
2. n : ℕ
3. ∀n:ℕn. ∀[i:ℕ]. (exp-rem(i;n;m) ~ i^n rem m)
4. ¬(n = 0 ∈ ℤ)
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) ∈ ℤ
⊢ eval n' = n ÷ 2 in
  eval x = exp-rem(i;n';m) in
    if n rem 2=0  then x * x rem m  else (i * x * x rem m) ~ i^n rem m
BY
{ (HypSubst' (-1) 0⋅
   THEN ((RWO "int_eq-as-ifthenelse" 0 THENA Auto) THEN AutoSplit THEN Try ((HypSubst' (-1) 0 THEN Reduce 0)))
   THEN (RepeatFor 2 ((CallByValueReduce 0 THENA Auto)⋅)
         THEN (RWO "-3 -4" 0⋅ THEN Auto⋅ THEN RWW "rem_mul<" 0 THEN Auto)⋅
         )⋅) }

1
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) ∈ ℤ

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n.  \mforall{}[i:\mBbbN{}].  (exp-rem(i;n;m)  \msim{}  i\^{}n  rem  m)
4.  \mneg{}(n  =  0)
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{}  eval  n'  =  n  \mdiv{}  2  in
    eval  x  =  exp-rem(i;n';m)  in
        if  n  rem  2=0    then  x  *  x  rem  m    else  (i  *  x  *  x  rem  m)  \msim{}  i\^{}n  rem  m


By

---

Latex:
(HypSubst'  (-1)  0\mcdot{}
  THEN  ((RWO  "int\_eq-as-ifthenelse"  0  THENA  Auto)
              THEN  AutoSplit
              THEN  Try  ((HypSubst'  (-1)  0  THEN  Reduce  0)))
  THEN  (RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)\mcdot{})
              THEN  (RWO  "-3  -4"  0\mcdot{}  THEN  Auto\mcdot{}  THEN  RWW  "rem\_mul<"  0  THEN  Auto)\mcdot{}
              )\mcdot{})

---

Home Index