Metamath Proof Explorer

Theorem fermltlchr

Description: A generalization of Fermat's little theorem in a commutative ring F of prime characteristic. See fermltl . (Contributed by Thierry Arnoux, 9-Jan-2024)

Ref Expression
Hypotheses fermltlchr.z ⊢ 𝑃 = ( chr ‘ 𝐹 )
fermltlchr.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
fermltlchr.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐹 ) )
fermltlchr.1 ⊢ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 )
fermltlchr.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
fermltlchr.3 ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
fermltlchr.4 ⊢ ( 𝜑 → 𝐹 ∈ CRing )
Assertion fermltlchr ( 𝜑 → ( 𝑃 ↑ 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 fermltlchr.z ⊢ 𝑃 = ( chr ‘ 𝐹 )
2 fermltlchr.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 fermltlchr.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐹 ) )
4 fermltlchr.1 ⊢ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 )
5 fermltlchr.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
6 fermltlchr.3 ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
7 fermltlchr.4 ⊢ ( 𝜑 → 𝐹 ∈ CRing )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 8 nnnn0d ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ0 )
10 5 9 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → 𝑃 ∈ ℕ0 )
12 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → 𝐸 ∈ ℤ )
13 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℤ )
14 zsscn ⊢ ℤ ⊆ ℂ
15 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
16 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
17 15 16 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
18 14 17 sseqtri ⊢ ℤ ⊆ ( Base ‘ ( mulGrp ‘ ℂfld ) )
19 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
20 eqid ⊢ ( invg ‘ ( mulGrp ‘ ℂfld ) ) = ( invg ‘ ( mulGrp ‘ ℂfld ) )
21 cnring ⊢ ℂfld ∈ Ring
22 15 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
23 21 22 ax-mp ⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
24 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
25 15 24 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
26 1z ⊢ 1 ∈ ℤ
27 25 26 eqeltrri ⊢ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) ∈ ℤ
28 eqid ⊢ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
29 13 17 28 ress0g ⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) ∈ ℤ ∧ ℤ ⊆ ℂ ) → ( 0g ‘ ( mulGrp ‘ ℂfld ) ) = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) )
30 23 27 14 29 mp3an ⊢ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) )
31 13 18 19 20 30 ressmulgnn0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 𝐸 ∈ ℤ ) → ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝐸 ) = ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐸 ) )
32 11 12 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝐸 ) = ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐸 ) )
33 12 zcnd ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → 𝐸 ∈ ℂ )
34 cnfldexp ⊢ ( ( 𝐸 ∈ ℂ ∧ 𝑃 ∈ ℕ0 ) → ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐸 ) = ( 𝐸 ↑ 𝑃 ) )
35 33 11 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐸 ) = ( 𝐸 ↑ 𝑃 ) )
36 32 35 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝐸 ) = ( 𝐸 ↑ 𝑃 ) )
37 36 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝐸 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) )
38 7 crngringd ⊢ ( 𝜑 → 𝐹 ∈ Ring )
39 eqid ⊢ ( ℤRHom ‘ 𝐹 ) = ( ℤRHom ‘ 𝐹 )
40 39 zrhrhm ⊢ ( 𝐹 ∈ Ring → ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) )
41 38 40 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) )
42 zringmpg ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring )
43 eqid ⊢ ( mulGrp ‘ 𝐹 ) = ( mulGrp ‘ 𝐹 )
44 42 43 rhmmhm ⊢ ( ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) → ( ℤRHom ‘ 𝐹 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝐹 ) ) )
45 41 44 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐹 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝐹 ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( ℤRHom ‘ 𝐹 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝐹 ) ) )
47 13 17 ressbas2 ⊢ ( ℤ ⊆ ℂ → ℤ = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) )
48 14 47 ax-mp ⊢ ℤ = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) )
49 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) = ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) )
50 48 49 3 mhmmulg ⊢ ( ( ( ℤRHom ‘ 𝐹 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝐹 ) ) ∧ 𝑃 ∈ ℕ0 ∧ 𝐸 ∈ ℤ ) → ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝐸 ) ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
51 46 11 12 50 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝐸 ) ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
52 6 10 zexpcld ⊢ ( 𝜑 → ( 𝐸 ↑ 𝑃 ) ∈ ℤ )
53 eqid ⊢ ( -g ‘ ℤring ) = ( -g ‘ ℤring )
54 53 zringsubgval ⊢ ( ( ( 𝐸 ↑ 𝑃 ) ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) = ( ( 𝐸 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝐸 ) )
55 52 6 54 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) = ( ( 𝐸 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝐸 ) )
56 55 fveq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝐸 ) ) )
57 52 zred ⊢ ( 𝜑 → ( 𝐸 ↑ 𝑃 ) ∈ ℝ )
58 6 zred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
59 5 8 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
60 59 nnrpd ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
61 fermltl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐸 ∈ ℤ ) → ( ( 𝐸 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐸 mod 𝑃 ) )
62 5 6 61 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐸 mod 𝑃 ) )
63 eqidd ⊢ ( 𝜑 → ( 𝐸 mod 𝑃 ) = ( 𝐸 mod 𝑃 ) )
64 57 58 58 58 60 62 63 modsub12d ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) mod 𝑃 ) = ( ( 𝐸 − 𝐸 ) mod 𝑃 ) )
65 zcn ⊢ ( 𝐸 ∈ ℤ → 𝐸 ∈ ℂ )
66 65 subidd ⊢ ( 𝐸 ∈ ℤ → ( 𝐸 − 𝐸 ) = 0 )
67 6 66 syl ⊢ ( 𝜑 → ( 𝐸 − 𝐸 ) = 0 )
68 67 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 − 𝐸 ) mod 𝑃 ) = ( 0 mod 𝑃 ) )
69 0mod ⊢ ( 𝑃 ∈ ℝ+ → ( 0 mod 𝑃 ) = 0 )
70 60 69 syl ⊢ ( 𝜑 → ( 0 mod 𝑃 ) = 0 )
71 64 68 70 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) mod 𝑃 ) = 0 )
72 52 6 zsubcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ∈ ℤ )
73 dvdsval3 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ↔ ( ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) mod 𝑃 ) = 0 ) )
74 59 72 73 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ↔ ( ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) mod 𝑃 ) = 0 ) )
75 71 74 mpbird ⊢ ( 𝜑 → 𝑃 ∥ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) )
76 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
77 1 39 76 chrdvds ⊢ ( ( 𝐹 ∈ Ring ∧ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ↔ ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ) = ( 0g ‘ 𝐹 ) ) )
78 38 72 77 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ↔ ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ) = ( 0g ‘ 𝐹 ) ) )
79 75 78 mpbid ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) − 𝐸 ) ) = ( 0g ‘ 𝐹 ) )
80 rhmghm ⊢ ( ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) → ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring GrpHom 𝐹 ) )
81 41 80 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring GrpHom 𝐹 ) )
82 zringbas ⊢ ℤ = ( Base ‘ ℤring )
83 eqid ⊢ ( -g ‘ 𝐹 ) = ( -g ‘ 𝐹 )
84 82 53 83 ghmsub ⊢ ( ( ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring GrpHom 𝐹 ) ∧ ( 𝐸 ↑ 𝑃 ) ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝐸 ) ) = ( ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ( -g ‘ 𝐹 ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
85 81 52 6 84 syl3anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ ( ( 𝐸 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝐸 ) ) = ( ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ( -g ‘ 𝐹 ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
86 56 79 85 3eqtr3rd ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ( -g ‘ 𝐹 ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) = ( 0g ‘ 𝐹 ) )
87 7 crnggrpd ⊢ ( 𝜑 → 𝐹 ∈ Grp )
88 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
89 82 88 rhmf ⊢ ( ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) → ( ℤRHom ‘ 𝐹 ) : ℤ ⟶ ( Base ‘ 𝐹 ) )
90 41 89 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐹 ) : ℤ ⟶ ( Base ‘ 𝐹 ) )
91 90 52 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ∈ ( Base ‘ 𝐹 ) )
92 90 6 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) )
93 88 76 83 grpsubeq0 ⊢ ( ( 𝐹 ∈ Grp ∧ ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ∈ ( Base ‘ 𝐹 ) ∧ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) ) → ( ( ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ( -g ‘ 𝐹 ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) = ( 0g ‘ 𝐹 ) ↔ ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
94 87 91 92 93 syl3anc ⊢ ( 𝜑 → ( ( ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) ( -g ‘ 𝐹 ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) = ( 0g ‘ 𝐹 ) ↔ ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
95 86 94 mpbid ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( ( ℤRHom ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
97 37 51 96 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
98 oveq2 ⊢ ( 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) → ( 𝑃 ↑ 𝐴 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
99 98 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( 𝑃 ↑ 𝐴 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
100 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
101 97 99 100 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) → ( 𝑃 ↑ 𝐴 ) = 𝐴 )
102 4 101 mpan2 ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) = 𝐴 )