---

Step * 1 2 2 2 of Lemma fermat-little


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)
BY
{ (InstConcl [⌜λi.b⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  \mneg{}(p  =  0)
3.  \mneg{}(p  \msim{}  1)
4.  \mforall{}b,c:\mBbbZ{}.    ((p  |  (b  *  c))  {}\mRightarrow{}  ((p  |  b)  \mvee{}  (p  |  c)))
5.  x  :  \mBbbN{}
6.  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x  \msim{}  \mBbbN{}x\^{}p
7.  Inj(\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x;\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x;\mlambda{}g.(g  o  rot(p)))
8.  b  :  \mBbbN{}x
\mvdash{}  \mexists{}a:\{x@0:\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x|  (x@0  o  rot(p))  =  x@0\}  .  ((a  0)  =  b)


By

---

Latex:
(InstConcl  [\mkleeneopen{}\mlambda{}i.b\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index