Step
*
1
2
2
1
1
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. a1 : ℕp ⟶ ℕx
9. (a1 o rot(p)) = a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 o rot(p)) = a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) = (a2 0) ∈ ℕx
13. a1 = (λi.(a1 0)) ∈ (ℕp ⟶ ℕx)
⊢ a2 = (λi.(a2 0)) ∈ (ℕp ⟶ ℕx)
BY
{ TACTIC:(Assert ∀n:ℕ. (n < p 
⇒ ((a2 n) = (a2 0) ∈ ℕx)) BY
                (InductionOnNat THEN Auto THEN D -2 THEN Auto THEN Assert ⌜(a2 (n - 1)) = (a2 n) ∈ ℕx⌝⋅ THEN Auto)) }
1
.....aux..... 
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 : ℕp ⟶ ℕx
9. (a1 o rot(p)) = a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 o rot(p)) = a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) = (a2 0) ∈ ℕx
13. a1 = (λi.(a1 0)) ∈ (ℕp ⟶ ℕx)
14. n : ℤ
15. 0 < n
16. n < p
17. (a2 (n - 1)) = (a2 0) ∈ ℕx
⊢ (a2 (n - 1)) = (a2 n) ∈ ℕ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. a1 : ℕp ⟶ ℕx
9. (a1 o rot(p)) = a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 o rot(p)) = a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) = (a2 0) ∈ ℕx
13. a1 = (λi.(a1 0)) ∈ (ℕp ⟶ ℕx)
14. ∀n:ℕ. (n < p 
⇒ ((a2 n) = (a2 0) ∈ ℕx))
⊢ a2 = (λi.(a2 0)) ∈ (ℕp ⟶ ℕx)
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.  a1  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x
9.  (a1  o  rot(p))  =  a1
10.  a2  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x
11.  (a2  o  rot(p))  =  a2
12.  (a1  0)  =  (a2  0)
13.  a1  =  (\mlambda{}i.(a1  0))
\mvdash{}  a2  =  (\mlambda{}i.(a2  0))
By
Latex:
TACTIC:(Assert  \mforall{}n:\mBbbN{}.  (n  <  p  {}\mRightarrow{}  ((a2  n)  =  (a2  0)))  BY
                            (InductionOnNat
                              THEN  Auto
                              THEN  D  -2
                              THEN  Auto
                              THEN  Assert  \mkleeneopen{}(a2  (n  -  1))  =  (a2  n)\mkleeneclose{}\mcdot{}
                              THEN  Auto))
Home
Index