---

Step * 1 2 of Lemma fermat-little


1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
⊢ {x@0:ℕp ⟶ ℕx| ((λg.(g o rot(p))) x@0) = x@0 ∈ (ℕp ⟶ ℕx)}  ~ ℕx
BY
{ TACTIC:(With ⌜λg.(g 0)⌝ (D 0)⋅ THEN Auto) }

1
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
6. ∀x@0:ℕp ⟶ ℕx. (((λg.(g o rot(p))) x@0) = x@0 ∈ (ℕp ⟶ ℕx) ∈ 𝕌{[1 | i 0]})
7. g : ℕp ⟶ ℕx
8. ((λg.(g o rot(p))) g) = g ∈ (ℕp ⟶ ℕx)
⊢ 0 ∈ ℕp

2
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
⊢ Bij({x@0:ℕp ⟶ ℕx| ((λg.(g o rot(p))) x@0) = x@0 ∈ (ℕp ⟶ ℕx)} ;ℕx;λg.(g 0))

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  prime(p)
3.  x  :  \mBbbN{}
4.  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x  \msim{}  \mBbbN{}x\^{}p
5.  Inj(\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x;\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x;\mlambda{}g.(g  o  rot(p)))
\mvdash{}  \{x@0:\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x|  ((\mlambda{}g.(g  o  rot(p)))  x@0)  =  x@0\}    \msim{}  \mBbbN{}x


By

---

Latex:
TACTIC:(With  \mkleeneopen{}\mlambda{}g.(g  0)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index