---

Step * 1 1 1 1 1 2 of Lemma fermat-little


1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. a1 : ℕp ⟶ ℕx
6. a2 : ℕp ⟶ ℕx
7. (a1 o rot(p)) = (a2 o rot(p)) ∈ (ℕp ⟶ ℕx)
8. x1 : ℤ
9. 0 ≤ x1
10. x1 < p
11. ¬(x1 = 0 ∈ ℤ)
⊢ (a1 x1) = (a2 x1) ∈ ℤ
BY
{ TACTIC:((ApFunToHypEquands `Z' ⌜Z (x1 - 1)⌝ ⌜ℕx⌝ (-5)⋅ THENA Auto)
          THEN (RepUR ``rotate`` -1 THEN SplitOnHypITE -1 )
          THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  prime(p)
3.  x  :  \mBbbN{}
4.  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x  \msim{}  \mBbbN{}x\^{}p
5.  a1  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x
6.  a2  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x
7.  (a1  o  rot(p))  =  (a2  o  rot(p))
8.  x1  :  \mBbbZ{}
9.  0  \mleq{}  x1
10.  x1  <  p
11.  \mneg{}(x1  =  0)
\mvdash{}  (a1  x1)  =  (a2  x1)


By

---

Latex:
TACTIC:((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  (x1  -  1)\mkleeneclose{}  \mkleeneopen{}\mBbbN{}x\mkleeneclose{}  (-5)\mcdot{}  THENA  Auto)
                THEN  (RepUR  ``rotate``  -1  THEN  SplitOnHypITE  -1  )
                THEN  Auto)

---

Home Index