---

Step * of Lemma exp-rem-property

∀[m:ℕ+]. ∀[n,i:ℕ].  (exp-rem(i;n;m) ~ i^n rem m)
BY
{ ((D 0 THENA Auto)
   THEN CompleteInductionOnNat
   THEN RecUnfold `exp-rem` 0
   THEN Reduce 0
   THEN CaseNat 0 `n'
   THEN Reduce 0
   THEN Try (Trivial)
   THEN (CaseNat 1 `n'
         THEN Reduce 0
         THEN Try ((RepUR ``exp`` 0 THEN Complete (Auto)))
         THEN (InstHyp [⌜n ÷ 2⌝] 3⋅ THENA (Auto THEN (MemTypeCD THEN Auto) THEN BLemma `div_mono1`  THEN Auto))
         THEN (D 0 THENA Auto)
         THEN Assert ⌜i^n = (i^n rem 2 * i^n ÷ 2 * i^n ÷ 2) ∈ ℤ⌝⋅)) }

1
.....assertion..... 
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 : ℕ
⊢ i^n = (i^n rem 2 * i^n ÷ 2 * i^n ÷ 2) ∈ ℤ

2
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

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[n,i:\mBbbN{}].    (exp-rem(i;n;m)  \msim{}  i\^{}n  rem  m)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  CompleteInductionOnNat
  THEN  RecUnfold  `exp-rem`  0
  THEN  Reduce  0
  THEN  CaseNat  0  `n'
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  (CaseNat  1  `n'
              THEN  Reduce  0
              THEN  Try  ((RepUR  ``exp``  0  THEN  Complete  (Auto)))
              THEN  (InstHyp  [\mkleeneopen{}n  \mdiv{}  2\mkleeneclose{}]  3\mcdot{}
                          THENA  (Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  BLemma  `div\_mono1`    THEN  Auto)
                          )
              THEN  (D  0  THENA  Auto)
              THEN  Assert  \mkleeneopen{}i\^{}n  =  (i\^{}n  rem  2  *  i\^{}n  \mdiv{}  2  *  i\^{}n  \mdiv{}  2)\mkleeneclose{}\mcdot{}))

---

Home Index