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	$$⊢P=\mathrm{chr}\left(F\right)$$
	fermltlchr.b	$$⊢B={\mathrm{Base}}_F$$
	fermltlchr.p	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_F}$$
	fermltlchr.1	$$⊢A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
	fermltlchr.2	$$⊢\phi \to P\in \mathbb{P}$$
	fermltlchr.3	$$⊢\phi \to E\in \mathbb{Z}$$
	fermltlchr.4	$$⊢\phi \to F\in \mathrm{CRing}$$
Assertion	fermltlchr	$$⊢\phi \to P\underset{\dot{}}{\times }A=A$$

Proof

Step	Hyp	Ref	Expression
1		fermltlchr.z	$$⊢P=\mathrm{chr}\left(F\right)$$
2		fermltlchr.b	$$⊢B={\mathrm{Base}}_F$$
3		fermltlchr.p	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_F}$$
4		fermltlchr.1	$$⊢A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
5		fermltlchr.2	$$⊢\phi \to P\in \mathbb{P}$$
6		fermltlchr.3	$$⊢\phi \to E\in \mathbb{Z}$$
7		fermltlchr.4	$$⊢\phi \to F\in \mathrm{CRing}$$
8		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
9	8	nnnn0d	$$⊢P\in \mathbb{P}\to P\in {\mathbb{N}}_0$$
10	5 9	syl	$$⊢\phi \to P\in {\mathbb{N}}_0$$
11	10	adantr	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P\in {\mathbb{N}}_0$$
12	6	adantr	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to E\in \mathbb{Z}$$
13		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
14		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
15		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
16		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
17	15 16	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
18	14 17	sseqtri	$$⊢\mathbb{Z}\subseteq {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
19		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}={\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
20		eqid	$$⊢{inv}_g\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)={inv}_g\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
21		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
22	15	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
23	21 22	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
24		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
25	15 24	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
26		1z	$$⊢1\in \mathbb{Z}$$
27	25 26	eqeltrri	$$⊢0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\in \mathbb{Z}$$
28		eqid	$$⊢0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
29	13 17 28	ress0g	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge 0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\in \mathbb{Z}\wedge \mathbb{Z}\subseteq ℂ\right)\to 0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}=0_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
30	23 27 14 29	mp3an	$$⊢0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}=0_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
31	13 18 19 20 30	ressmulgnn0	$$⊢\left(P\in {\mathbb{N}}_0\wedge E\in \mathbb{Z}\right)\to P{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}E=P{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}E$$
32	11 12 31	syl2anc	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}E=P{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}E$$
33	12	zcnd	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to E\in ℂ$$
34		cnfldexp	$$⊢\left(E\in ℂ\wedge P\in {\mathbb{N}}_0\right)\to P{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}E=E^P$$
35	33 11 34	syl2anc	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}E=E^P$$
36	32 35	eqtrd	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}E=E^P$$
37	36	fveq2d	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(P{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)$$
38	7	crngringd	$$⊢\phi \to F\in \mathrm{Ring}$$
39		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)$$
40	39	zrhrhm	$$⊢F\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)$$
41	38 40	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)$$
42		zringmpg	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
43		eqid	$$⊢{\mathrm{mulGrp}}_F={\mathrm{mulGrp}}_F$$
44	42 43	rhmmhm	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_F\right)$$
45	41 44	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_F\right)$$
46	45	adantr	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_F\right)$$
47	13 17	ressbas2	$$⊢\mathbb{Z}\subseteq ℂ\to \mathbb{Z}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
48	14 47	ax-mp	$$⊢\mathbb{Z}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
49		eqid	$$⊢{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}={\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}$$
50	48 49 3	mhmmulg	$$⊢\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_F\right)\wedge P\in {\mathbb{N}}_0\wedge E\in \mathbb{Z}\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(P{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}E\right)=P\underset{\dot{}}{\times }\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
51	46 11 12 50	syl3anc	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(P{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right)}E\right)=P\underset{\dot{}}{\times }\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
52	6 10	zexpcld	$$⊢\phi \to E^P\in \mathbb{Z}$$
53		eqid	$$⊢{-}_{{\mathbb{Z}}_{\mathrm{ring}}}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
54	53	zringsubgval	$$⊢\left(E^P\in \mathbb{Z}\wedge E\in \mathbb{Z}\right)\to E^P-E=E^P{-}_{{\mathbb{Z}}_{\mathrm{ring}}}E$$
55	52 6 54	syl2anc	$$⊢\phi \to E^P-E=E^P{-}_{{\mathbb{Z}}_{\mathrm{ring}}}E$$
56	55	fveq2d	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P-E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P{-}_{{\mathbb{Z}}_{\mathrm{ring}}}E\right)$$
57	52	zred	$$⊢\phi \to E^P\in ℝ$$
58	6	zred	$$⊢\phi \to E\in ℝ$$
59	5 8	syl	$$⊢\phi \to P\in \mathbb{N}$$
60	59	nnrpd	$$⊢\phi \to P\in {ℝ}^{+}$$
61		fermltl	$$⊢\left(P\in \mathbb{P}\wedge E\in \mathbb{Z}\right)\to E^P\mathrm{mod}P=E\mathrm{mod}P$$
62	5 6 61	syl2anc	$$⊢\phi \to E^P\mathrm{mod}P=E\mathrm{mod}P$$
63		eqidd	$$⊢\phi \to E\mathrm{mod}P=E\mathrm{mod}P$$
64	57 58 58 58 60 62 63	modsub12d	$$⊢\phi \to \left(E^P-E\right)\mathrm{mod}P=\left(E-E\right)\mathrm{mod}P$$
65		zcn	$$⊢E\in \mathbb{Z}\to E\in ℂ$$
66	65	subidd	$$⊢E\in \mathbb{Z}\to E-E=0$$
67	6 66	syl	$$⊢\phi \to E-E=0$$
68	67	oveq1d	$$⊢\phi \to \left(E-E\right)\mathrm{mod}P=0\mathrm{mod}P$$
69		0mod	$$⊢P\in {ℝ}^{+}\to 0\mathrm{mod}P=0$$
70	60 69	syl	$$⊢\phi \to 0\mathrm{mod}P=0$$
71	64 68 70	3eqtrd	$$⊢\phi \to \left(E^P-E\right)\mathrm{mod}P=0$$
72	52 6	zsubcld	$$⊢\phi \to E^P-E\in \mathbb{Z}$$
73		dvdsval3	$$⊢\left(P\in \mathbb{N}\wedge E^P-E\in \mathbb{Z}\right)\to \left(P\parallel \left(E^P-E\right)\leftrightarrow \left(E^P-E\right)\mathrm{mod}P=0\right)$$
74	59 72 73	syl2anc	$$⊢\phi \to \left(P\parallel \left(E^P-E\right)\leftrightarrow \left(E^P-E\right)\mathrm{mod}P=0\right)$$
75	71 74	mpbird	$$⊢\phi \to P\parallel \left(E^P-E\right)$$
76		eqid	$$⊢0_F=0_F$$
77	1 39 76	chrdvds	$$⊢\left(F\in \mathrm{Ring}\wedge E^P-E\in \mathbb{Z}\right)\to \left(P\parallel \left(E^P-E\right)\leftrightarrow \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P-E\right)=0_F\right)$$
78	38 72 77	syl2anc	$$⊢\phi \to \left(P\parallel \left(E^P-E\right)\leftrightarrow \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P-E\right)=0_F\right)$$
79	75 78	mpbid	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P-E\right)=0_F$$
80		rhmghm	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}F\right)$$
81	41 80	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}F\right)$$
82		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
83		eqid	$$⊢{-}_F={-}_F$$
84	82 53 83	ghmsub	$$⊢\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}F\right)\wedge E^P\in \mathbb{Z}\wedge E\in \mathbb{Z}\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P{-}_{{\mathbb{Z}}_{\mathrm{ring}}}E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right){-}_F\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
85	81 52 6 84	syl3anc	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P{-}_{{\mathbb{Z}}_{\mathrm{ring}}}E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right){-}_F\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
86	56 79 85	3eqtr3rd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right){-}_F\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)=0_F$$
87	7	crnggrpd	$$⊢\phi \to F\in \mathrm{Grp}$$
88		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
89	82 88	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right):\mathbb{Z}⟶{\mathrm{Base}}_F$$
90	41 89	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right):\mathbb{Z}⟶{\mathrm{Base}}_F$$
91	90 52	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)\in {\mathrm{Base}}_F$$
92	90 6	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\in {\mathrm{Base}}_F$$
93	88 76 83	grpsubeq0	$$⊢\left(F\in \mathrm{Grp}\wedge \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)\in {\mathrm{Base}}_F\wedge \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\in {\mathrm{Base}}_F\right)\to \left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right){-}_F\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)=0_F\leftrightarrow \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
94	87 91 92 93	syl3anc	$$⊢\phi \to \left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right){-}_F\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)=0_F\leftrightarrow \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
95	86 94	mpbid	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
96	95	adantr	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E^P\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
97	37 51 96	3eqtr3d	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P\underset{\dot{}}{\times }\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
98		oveq2	$$⊢A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\to P\underset{\dot{}}{\times }A=P\underset{\dot{}}{\times }\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
99	98	adantl	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P\underset{\dot{}}{\times }A=P\underset{\dot{}}{\times }\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
100		simpr	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
101	97 99 100	3eqtr4d	$$⊢\left(\phi \wedge A=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\to P\underset{\dot{}}{\times }A=A$$
102	4 101	mpan2	$$⊢\phi \to P\underset{\dot{}}{\times }A=A$$