---

Step * of Lemma Euler-Fermat

No Annotations
∀n:{2...}. ∀a:ℕ+.  (CoPrime(n,a) ⇒ (a^totient(n) ≡ 1 mod n))
BY
{ (Auto
   THEN (Assert Πx ∈ map(λi.(ai mod n);residues-mod(n)). x = Πx ∈ residues-mod(n). x ∈ ℤ BY
               (Using [`T',⌜ℤ⌝] EqCD⋅
                THEN Auto
                THEN Try (((InstLemma `residues-equal-bags` [⌜n⌝;⌜a⌝]⋅ THENA Auto)
                           THEN HypSubst' (-1) 0
                           THEN Complete (Auto)))
                THEN D 0
                THEN Reduce 0
                THEN Auto))
   THEN (Assert Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ BY
               ((Unfold `bag-product` (-1) THEN Unfold `bag-product` 0)
                THEN Fold `bag-map` (-1)
                THEN RWO "bag-summation-map" (-1)
                THEN Auto
                THEN Reduce (-1)))) }

1
1. n : {2...}
2. a : ℕ+
3. CoPrime(n,a)
4. Πx ∈ map(λi.(ai mod n);residues-mod(n)). x = Πx ∈ residues-mod(n). x ∈ ℤ
5. Πx ∈ residues-mod(n). (ax mod n) = Πx ∈ residues-mod(n). x ∈ ℤ
⊢ a^totient(n) ≡ 1 mod n

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\{2...\}.  \mforall{}a:\mBbbN{}\msupplus{}.    (CoPrime(n,a)  {}\mRightarrow{}  (a\^{}totient(n)  \mequiv{}  1  mod  n))


By

---

Latex:
(Auto
  THEN  (Assert  \mPi{}x  \mmember{}  map(\mlambda{}i.(ai  mod  n);residues-mod(n)).  x  =  \mPi{}x  \mmember{}  residues-mod(n).  x  BY
                          (Using  [`T',\mkleeneopen{}\mBbbZ{}\mkleeneclose{}]  EqCD\mcdot{}
                            THEN  Auto
                            THEN  Try  (((InstLemma  `residues-equal-bags`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                  THEN  HypSubst'  (-1)  0
                                                  THEN  Complete  (Auto)))
                            THEN  D  0
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (Assert  \mPi{}x  \mmember{}  residues-mod(n).  (ax  mod  n)  =  \mPi{}x  \mmember{}  residues-mod(n).  x  BY
                          ((Unfold  `bag-product`  (-1)  THEN  Unfold  `bag-product`  0)
                            THEN  Fold  `bag-map`  (-1)
                            THEN  RWO  "bag-summation-map"  (-1)
                            THEN  Auto
                            THEN  Reduce  (-1))))

---

Home Index