---

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