znfermltl

Description: Fermat's little theorem in Z/nZ . (Contributed by Thierry Arnoux, 24-Jul-2024)

	Ref	Expression
Hypotheses	znfermltl.z	$⊢ Z = ℤ / P ℤ$
	znfermltl.b	$⊢ B = {Base}_{Z}$
	znfermltl.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Z}}$
Assertion	znfermltl	$⊢ (P \in ℙ \land A \in B) \to P \underset{˙}{\times} A = A$

Proof

Step	Hyp	Ref	Expression
1		znfermltl.z	$⊢ Z = ℤ / P ℤ$
2		znfermltl.b	$⊢ B = {Base}_{Z}$
3		znfermltl.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Z}}$
4		prmnn	$⊢ P \in ℙ \to P \in ℕ$
5	4	nnnn0d	$⊢ P \in ℙ \to P \in ℕ_{0}$
6	5	ad3antrrr	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \in ℕ_{0}$
7		simplr	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to a \in ℤ$
8		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ$
9		zsscn	$⊢ ℤ \subseteq ℂ$
10		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
11		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
12	10 11	mgpbas	$⊢ ℂ = {Base}_{{mulGrp}_{ℂ_{fld}}}$
13	9 12	sseqtri	$⊢ ℤ \subseteq {Base}_{{mulGrp}_{ℂ_{fld}}}$
14		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
15		eqid	$⊢ {inv}_{g} ({mulGrp}_{ℂ_{fld}}) = {inv}_{g} ({mulGrp}_{ℂ_{fld}})$
16		cnring	$⊢ ℂ_{fld} \in Ring$
17	10	ringmgp	$⊢ ℂ_{fld} \in Ring \to {mulGrp}_{ℂ_{fld}} \in Mnd$
18	16 17	ax-mp	$⊢ {mulGrp}_{ℂ_{fld}} \in Mnd$
19		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
20	10 19	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
21		1z	$⊢ 1 \in ℤ$
22	20 21	eqeltrri	$⊢ 0_{{mulGrp}_{ℂ_{fld}}} \in ℤ$
23		eqid	$⊢ 0_{{mulGrp}_{ℂ_{fld}}} = 0_{{mulGrp}_{ℂ_{fld}}}$
24	8 12 23	ress0g	$⊢ ({mulGrp}_{ℂ_{fld}} \in Mnd \land 0_{{mulGrp}_{ℂ_{fld}}} \in ℤ \land ℤ \subseteq ℂ) \to 0_{{mulGrp}_{ℂ_{fld}}} = 0_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
25	18 22 9 24	mp3an	$⊢ 0_{{mulGrp}_{ℂ_{fld}}} = 0_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
26	8 13 14 15 25	ressmulgnn0	$⊢ (P \in ℕ_{0} \land a \in ℤ) \to P \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} a = P \cdot_{{mulGrp}_{ℂ_{fld}}} a$
27	6 7 26	syl2anc	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} a = P \cdot_{{mulGrp}_{ℂ_{fld}}} a$
28	7	zcnd	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to a \in ℂ$
29		cnfldexp	$⊢ (a \in ℂ \land P \in ℕ_{0}) \to P \cdot_{{mulGrp}_{ℂ_{fld}}} a = a^{P}$
30	28 6 29	syl2anc	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \cdot_{{mulGrp}_{ℂ_{fld}}} a = a^{P}$
31	27 30	eqtrd	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} a = a^{P}$
32	31	fveq2d	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to ℤRHom (Z) (P \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} a) = ℤRHom (Z) (a^{P})$
33		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
34	1	zncrng	$⊢ P \in ℕ_{0} \to Z \in CRing$
35	34	crngringd	$⊢ P \in ℕ_{0} \to Z \in Ring$
36		eqid	$⊢ ℤRHom (Z) = ℤRHom (Z)$
37	36	zrhrhm	$⊢ Z \in Ring \to ℤRHom (Z) \in (ℤ_{ring} RingHom Z)$
38	35 37	syl	$⊢ P \in ℕ_{0} \to ℤRHom (Z) \in (ℤ_{ring} RingHom Z)$
39		zringmpg	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ = {mulGrp}_{ℤ_{ring}}$
40		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
41	39 40	rhmmhm	$⊢ ℤRHom (Z) \in (ℤ_{ring} RingHom Z) \to ℤRHom (Z) \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom {mulGrp}_{Z})$
42	4 33 38 41	4syl	$⊢ P \in ℙ \to ℤRHom (Z) \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom {mulGrp}_{Z})$
43	42	ad3antrrr	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to ℤRHom (Z) \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom {mulGrp}_{Z})$
44	8 12	ressbas2	$⊢ ℤ \subseteq ℂ \to ℤ = {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
45	9 44	ax-mp	$⊢ ℤ = {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
46		eqid	$⊢ \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} = \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
47	45 46 3	mhmmulg	$⊢ (ℤRHom (Z) \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom {mulGrp}_{Z}) \land P \in ℕ_{0} \land a \in ℤ) \to ℤRHom (Z) (P \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} a) = P \underset{˙}{\times} ℤRHom (Z) (a)$
48	43 6 7 47	syl3anc	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to ℤRHom (Z) (P \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} a) = P \underset{˙}{\times} ℤRHom (Z) (a)$
49		simpr	$⊢ (P \in ℙ \land a \in ℤ) \to a \in ℤ$
50	4	adantr	$⊢ (P \in ℙ \land a \in ℤ) \to P \in ℕ$
51	50	nnnn0d	$⊢ (P \in ℙ \land a \in ℤ) \to P \in ℕ_{0}$
52		zexpcl	$⊢ (a \in ℤ \land P \in ℕ_{0}) \to a^{P} \in ℤ$
53	49 51 52	syl2anc	$⊢ (P \in ℙ \land a \in ℤ) \to a^{P} \in ℤ$
54		eqid	$⊢ -_{ℤ_{ring}} = -_{ℤ_{ring}}$
55	54	zringsubgval	$⊢ (a^{P} \in ℤ \land a \in ℤ) \to a^{P} - a = a^{P} -_{ℤ_{ring}} a$
56	53 49 55	syl2anc	$⊢ (P \in ℙ \land a \in ℤ) \to a^{P} - a = a^{P} -_{ℤ_{ring}} a$
57	56	fveq2d	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a^{P} - a) = ℤRHom (Z) (a^{P} -_{ℤ_{ring}} a)$
58	53	zred	$⊢ (P \in ℙ \land a \in ℤ) \to a^{P} \in ℝ$
59		zre	$⊢ a \in ℤ \to a \in ℝ$
60	59	adantl	$⊢ (P \in ℙ \land a \in ℤ) \to a \in ℝ$
61	50	nnrpd	$⊢ (P \in ℙ \land a \in ℤ) \to P \in ℝ^{+}$
62		fermltl	$⊢ (P \in ℙ \land a \in ℤ) \to a^{P} \mod P = a \mod P$
63		eqidd	$⊢ (P \in ℙ \land a \in ℤ) \to a \mod P = a \mod P$
64	58 60 60 60 61 62 63	modsub12d	$⊢ (P \in ℙ \land a \in ℤ) \to (a^{P} - a) \mod P = (a - a) \mod P$
65		zcn	$⊢ a \in ℤ \to a \in ℂ$
66	65	subidd	$⊢ a \in ℤ \to a - a = 0$
67	66	adantl	$⊢ (P \in ℙ \land a \in ℤ) \to a - a = 0$
68	67	oveq1d	$⊢ (P \in ℙ \land a \in ℤ) \to (a - a) \mod P = 0 \mod P$
69		0mod	$⊢ P \in ℝ^{+} \to 0 \mod P = 0$
70	61 69	syl	$⊢ (P \in ℙ \land a \in ℤ) \to 0 \mod P = 0$
71	64 68 70	3eqtrd	$⊢ (P \in ℙ \land a \in ℤ) \to (a^{P} - a) \mod P = 0$
72	53 49	zsubcld	$⊢ (P \in ℙ \land a \in ℤ) \to a^{P} - a \in ℤ$
73		dvdsval3	$⊢ (P \in ℕ \land a^{P} - a \in ℤ) \to (P ∥ (a^{P} - a) \leftrightarrow (a^{P} - a) \mod P = 0)$
74	50 72 73	syl2anc	$⊢ (P \in ℙ \land a \in ℤ) \to (P ∥ (a^{P} - a) \leftrightarrow (a^{P} - a) \mod P = 0)$
75	71 74	mpbird	$⊢ (P \in ℙ \land a \in ℤ) \to P ∥ (a^{P} - a)$
76		eqid	$⊢ 0_{Z} = 0_{Z}$
77	1 36 76	zndvds0	$⊢ (P \in ℕ_{0} \land a^{P} - a \in ℤ) \to (ℤRHom (Z) (a^{P} - a) = 0_{Z} \leftrightarrow P ∥ (a^{P} - a))$
78	51 72 77	syl2anc	$⊢ (P \in ℙ \land a \in ℤ) \to (ℤRHom (Z) (a^{P} - a) = 0_{Z} \leftrightarrow P ∥ (a^{P} - a))$
79	75 78	mpbird	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a^{P} - a) = 0_{Z}$
80		rhmghm	$⊢ ℤRHom (Z) \in (ℤ_{ring} RingHom Z) \to ℤRHom (Z) \in (ℤ_{ring} GrpHom Z)$
81	51 38 80	3syl	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) \in (ℤ_{ring} GrpHom Z)$
82		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
83		eqid	$⊢ -_{Z} = -_{Z}$
84	82 54 83	ghmsub	$⊢ (ℤRHom (Z) \in (ℤ_{ring} GrpHom Z) \land a^{P} \in ℤ \land a \in ℤ) \to ℤRHom (Z) (a^{P} -_{ℤ_{ring}} a) = ℤRHom (Z) (a^{P}) -_{Z} ℤRHom (Z) (a)$
85	81 53 49 84	syl3anc	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a^{P} -_{ℤ_{ring}} a) = ℤRHom (Z) (a^{P}) -_{Z} ℤRHom (Z) (a)$
86	57 79 85	3eqtr3rd	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a^{P}) -_{Z} ℤRHom (Z) (a) = 0_{Z}$
87	4 33 35	3syl	$⊢ P \in ℙ \to Z \in Ring$
88	87	ringgrpd	$⊢ P \in ℙ \to Z \in Grp$
89	88	adantr	$⊢ (P \in ℙ \land a \in ℤ) \to Z \in Grp$
90		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
91	82 90	rhmf	$⊢ ℤRHom (Z) \in (ℤ_{ring} RingHom Z) \to ℤRHom (Z) : ℤ ⟶ {Base}_{Z}$
92	51 38 91	3syl	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) : ℤ ⟶ {Base}_{Z}$
93	92 53	ffvelrnd	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a^{P}) \in {Base}_{Z}$
94	92 49	ffvelrnd	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a) \in {Base}_{Z}$
95	90 76 83	grpsubeq0	$⊢ (Z \in Grp \land ℤRHom (Z) (a^{P}) \in {Base}_{Z} \land ℤRHom (Z) (a) \in {Base}_{Z}) \to (ℤRHom (Z) (a^{P}) -_{Z} ℤRHom (Z) (a) = 0_{Z} \leftrightarrow ℤRHom (Z) (a^{P}) = ℤRHom (Z) (a))$
96	89 93 94 95	syl3anc	$⊢ (P \in ℙ \land a \in ℤ) \to (ℤRHom (Z) (a^{P}) -_{Z} ℤRHom (Z) (a) = 0_{Z} \leftrightarrow ℤRHom (Z) (a^{P}) = ℤRHom (Z) (a))$
97	86 96	mpbid	$⊢ (P \in ℙ \land a \in ℤ) \to ℤRHom (Z) (a^{P}) = ℤRHom (Z) (a)$
98	97	ad4ant13	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to ℤRHom (Z) (a^{P}) = ℤRHom (Z) (a)$
99	32 48 98	3eqtr3d	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \underset{˙}{\times} ℤRHom (Z) (a) = ℤRHom (Z) (a)$
100		oveq2	$⊢ A = ℤRHom (Z) (a) \to P \underset{˙}{\times} A = P \underset{˙}{\times} ℤRHom (Z) (a)$
101	100	adantl	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \underset{˙}{\times} A = P \underset{˙}{\times} ℤRHom (Z) (a)$
102		simpr	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to A = ℤRHom (Z) (a)$
103	99 101 102	3eqtr4d	$⊢ (((P \in ℙ \land A \in B) \land a \in ℤ) \land A = ℤRHom (Z) (a)) \to P \underset{˙}{\times} A = A$
104	1 2 36	znzrhfo	$⊢ P \in ℕ_{0} \to ℤRHom (Z) : ℤ \underset{onto}{⟶} B$
105	4 33 104	3syl	$⊢ P \in ℙ \to ℤRHom (Z) : ℤ \underset{onto}{⟶} B$
106		foelrn	$⊢ (ℤRHom (Z) : ℤ \underset{onto}{⟶} B \land A \in B) \to \exists a \in ℤ A = ℤRHom (Z) (a)$
107	105 106	sylan	$⊢ (P \in ℙ \land A \in B) \to \exists a \in ℤ A = ℤRHom (Z) (a)$
108	103 107	r19.29a	$⊢ (P \in ℙ \land A \in B) \to P \underset{˙}{\times} A = A$

Metamath Proof Explorer

Theorem znfermltl

Proof