---

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


1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. a1 : ℕp ⟶ ℕx
6. a2 : ℕp ⟶ ℕx
7. (a1 o rot(p)) = (a2 o rot(p)) ∈ (ℕp ⟶ ℕx)
8. x1 : ℤ
9. 0 ≤ x1
10. x1 < p
⊢ (a1 x1) = (a2 x1) ∈ ℤ
BY
{ TACTIC:(Decide x1 = 0 ∈ ℤ THENA Auto) }

1
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. a1 : ℕp ⟶ ℕx
6. a2 : ℕp ⟶ ℕx
7. (a1 o rot(p)) = (a2 o rot(p)) ∈ (ℕp ⟶ ℕx)
8. x1 : ℤ
9. 0 ≤ x1
10. x1 < p
11. x1 = 0 ∈ ℤ
⊢ (a1 x1) = (a2 x1) ∈ ℤ

2
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. a1 : ℕp ⟶ ℕx
6. a2 : ℕp ⟶ ℕx
7. (a1 o rot(p)) = (a2 o rot(p)) ∈ (ℕp ⟶ ℕx)
8. x1 : ℤ
9. 0 ≤ x1
10. x1 < p
11. ¬(x1 = 0 ∈ ℤ)
⊢ (a1 x1) = (a2 x1) ∈ ℤ

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  prime(p)
3.  x  :  \mBbbN{}
4.  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x  \msim{}  \mBbbN{}x\^{}p
5.  a1  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x
6.  a2  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x
7.  (a1  o  rot(p))  =  (a2  o  rot(p))
8.  x1  :  \mBbbZ{}
9.  0  \mleq{}  x1
10.  x1  <  p
\mvdash{}  (a1  x1)  =  (a2  x1)


By

---

Latex:
TACTIC:(Decide  x1  =  0  THENA  Auto)

---

Home Index