---

Step * 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)
⊢ a1 = a2 ∈ (ℕp ⟶ ℕx)
BY
{ TACTIC:(Ext THEN 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 : ℕp
⊢ (a1 x1) = (a2 x1) ∈ ℕx

---

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))
\mvdash{}  a1  =  a2


By

---

Latex:
TACTIC:(Ext  THEN  Auto)

---

Home Index