Step |
Hyp |
Ref |
Expression |
1 |
|
ply1fermltl.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑃 ) |
2 |
|
ply1fermltl.w |
⊢ 𝑊 = ( Poly1 ‘ 𝑍 ) |
3 |
|
ply1fermltl.x |
⊢ 𝑋 = ( var1 ‘ 𝑍 ) |
4 |
|
ply1fermltl.l |
⊢ + = ( +g ‘ 𝑊 ) |
5 |
|
ply1fermltl.n |
⊢ 𝑁 = ( mulGrp ‘ 𝑊 ) |
6 |
|
ply1fermltl.t |
⊢ ↑ = ( .g ‘ 𝑁 ) |
7 |
|
ply1fermltl.c |
⊢ 𝐶 = ( algSc ‘ 𝑊 ) |
8 |
|
ply1fermltl.a |
⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝐸 ) ) |
9 |
|
ply1fermltl.p |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
10 |
|
ply1fermltl.1 |
⊢ ( 𝜑 → 𝐸 ∈ ℤ ) |
11 |
|
eqid |
⊢ ( chr ‘ 𝑍 ) = ( chr ‘ 𝑍 ) |
12 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
13 |
|
nnnn0 |
⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 ) |
14 |
1
|
zncrng |
⊢ ( 𝑃 ∈ ℕ0 → 𝑍 ∈ CRing ) |
15 |
9 12 13 14
|
4syl |
⊢ ( 𝜑 → 𝑍 ∈ CRing ) |
16 |
1
|
znchr |
⊢ ( 𝑃 ∈ ℕ0 → ( chr ‘ 𝑍 ) = 𝑃 ) |
17 |
9 12 13 16
|
4syl |
⊢ ( 𝜑 → ( chr ‘ 𝑍 ) = 𝑃 ) |
18 |
17 9
|
eqeltrd |
⊢ ( 𝜑 → ( chr ‘ 𝑍 ) ∈ ℙ ) |
19 |
2 3 4 5 6 7 8 11 15 18 10
|
ply1fermltlchr |
⊢ ( 𝜑 → ( ( chr ‘ 𝑍 ) ↑ ( 𝑋 + 𝐴 ) ) = ( ( ( chr ‘ 𝑍 ) ↑ 𝑋 ) + 𝐴 ) ) |
20 |
17
|
oveq1d |
⊢ ( 𝜑 → ( ( chr ‘ 𝑍 ) ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) ) |
21 |
17
|
oveq1d |
⊢ ( 𝜑 → ( ( chr ‘ 𝑍 ) ↑ 𝑋 ) = ( 𝑃 ↑ 𝑋 ) ) |
22 |
21
|
oveq1d |
⊢ ( 𝜑 → ( ( ( chr ‘ 𝑍 ) ↑ 𝑋 ) + 𝐴 ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) ) |
23 |
19 20 22
|
3eqtr3d |
⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) ) |