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


1. : ℕ
2. ¬(p 0 ∈ ℤ)
3. ¬(p 1)
4. ∀b,c:ℤ.  ((p (b c))  ((p b) ∨ (p c)))
5. : ℕ
6. ℕp ⟶ ℕ~ ℕx^p
7. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g rot(p)))
8. a1 : ℕp ⟶ ℕx
9. (a1 rot(p)) a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 rot(p)) a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) (a2 0) ∈ ℕx
⊢ a1 a2 ∈ {x@0:ℕp ⟶ ℕx| (x@0 rot(p)) x@0 ∈ (ℕp ⟶ ℕx)} 
BY
TACTIC:(Assert ⌜(a1 i.(a1 0)) ∈ (ℕp ⟶ ℕx)) ∧ (a2 i.(a2 0)) ∈ (ℕp ⟶ ℕx))⌝⋅ THEN Auto) }

1
1. : ℕ
2. ¬(p 0 ∈ ℤ)
3. ¬(p 1)
4. ∀b,c:ℤ.  ((p (b c))  ((p b) ∨ (p c)))
5. : ℕ
6. ℕp ⟶ ℕ~ ℕx^p
7. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g rot(p)))
8. a1 : ℕp ⟶ ℕx
9. (a1 rot(p)) a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 rot(p)) a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) (a2 0) ∈ ℕx
⊢ a1 i.(a1 0)) ∈ (ℕp ⟶ ℕx)

2
1. : ℕ
2. ¬(p 0 ∈ ℤ)
3. ¬(p 1)
4. ∀b,c:ℤ.  ((p (b c))  ((p b) ∨ (p c)))
5. : ℕ
6. ℕp ⟶ ℕ~ ℕx^p
7. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g rot(p)))
8. a1 : ℕp ⟶ ℕx
9. (a1 rot(p)) a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 rot(p)) a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) (a2 0) ∈ ℕx
13. a1 i.(a1 0)) ∈ (ℕp ⟶ ℕx)
⊢ a2 i.(a2 0)) ∈ (ℕp ⟶ ℕx)

3
1. : ℕ
2. ¬(p 0 ∈ ℤ)
3. ¬(p 1)
4. ∀b,c:ℤ.  ((p (b c))  ((p b) ∨ (p c)))
5. : ℕ
6. ℕp ⟶ ℕ~ ℕx^p
7. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g rot(p)))
8. a1 : ℕp ⟶ ℕx
9. (a1 rot(p)) a1 ∈ (ℕp ⟶ ℕx)
10. a2 : ℕp ⟶ ℕx
11. (a2 rot(p)) a2 ∈ (ℕp ⟶ ℕx)
12. (a1 0) (a2 0) ∈ ℕx
13. a1 i.(a1 0)) ∈ (ℕp ⟶ ℕx)
14. a2 i.(a2 0)) ∈ (ℕp ⟶ ℕx)
⊢ a1 a2 ∈ {x@0:ℕp ⟶ ℕx| (x@0 rot(p)) x@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)
\mvdash{}  a1  =  a2


By


Latex:
TACTIC:(Assert  \mkleeneopen{}(a1  =  (\mlambda{}i.(a1  0)))  \mwedge{}  (a2  =  (\mlambda{}i.(a2  0)))\mkleeneclose{}\mcdot{}  THEN  Auto)




Home Index