---

Step * 1 2 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)))
⊢ Bij({x@0:ℕp ⟶ ℕx| ((λg.(g o rot(p))) x@0) = x@0 ∈ (ℕp ⟶ ℕx)} ;ℕx;λg.(g 0))
BY
{ TACTIC:(D 2 THEN RepeatFor 2 (D 0) THEN All Reduce THEN Auto) }

1
1. p : ℕ
2. ¬(p = 0 ∈ ℤ)
3. ¬(p ~ 1)
4. ∀b,c:ℤ.  ((p | (b * c)) ⇒ ((p | b) ∨ (p | c)))
5. x : ℕ
6. ℕp ⟶ ℕx ~ ℕx^p
7. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
8. a1 : {x@0:ℕp ⟶ ℕx| (x@0 o rot(p)) = x@0 ∈ (ℕp ⟶ ℕx)} 
9. a2 : {x@0:ℕp ⟶ ℕx| (x@0 o rot(p)) = x@0 ∈ (ℕp ⟶ ℕx)} 
10. (a1 0) = (a2 0) ∈ ℕx
⊢ a1 = a2 ∈ {x@0:ℕp ⟶ ℕx| (x@0 o rot(p)) = x@0 ∈ (ℕp ⟶ ℕx)} 

2
1. p : ℕ
2. ¬(p = 0 ∈ ℤ)
3. ¬(p ~ 1)
4. ∀b,c:ℤ.  ((p | (b * c)) ⇒ ((p | b) ∨ (p | c)))
5. x : ℕ
6. ℕp ⟶ ℕx ~ ℕx^p
7. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
8. b : ℕx
⊢ ∃a:{x@0:ℕp ⟶ ℕx| (x@0 o rot(p)) = x@0 ∈ (ℕp ⟶ ℕx)} . ((a 0) = b ∈ ℕx)

---

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{}  Bij(\{x@0:\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x|  ((\mlambda{}g.(g  o  rot(p)))  x@0)  =  x@0\}  ;\mBbbN{}x;\mlambda{}g.(g  0))


By

---

Latex:
TACTIC:(D  2  THEN  RepeatFor  2  (D  0)  THEN  All  Reduce  THEN  Auto)

---

Home Index