dchrisum0flblem1 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dchrisum0flblem1		Unicode version

Theorem dchrisum0flblem1 21155

Description: Lemma for dchrisum0flb 21157. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.)

**Hypotheses**
Ref	Expression
rpvmasum.z	ℤ/nℤ
rpvmasum.l	RHom
rpvmasum.a
rpvmasum2.g	DChr
rpvmasum2.d
rpvmasum2.1
dchrisum0f.f
dchrisum0f.x
dchrisum0flb.r
dchrisum0flblem1.1
dchrisum0flblem1.2

**Assertion**
Ref	Expression
dchrisum0flblem1

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem dchrisum0flblem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1re 9046	. . . . . 6
2	1	a1i 11	. . . . 5 $/\$ $/\$
3		0re 9047	. . . . . 6
4	3	a1i 11	. . . . 5 $/\$ $/\$
5	2, 4	ifclda 3726	. . . 4 $/\$
6	1	a1i 11	. . . 4 $/\$
7		fzfid 11267	. . . . . 6
8		dchrisum0flb.r	. . . . . . . 8
9		rpvmasum.a	. . . . . . . . . . 11
10	9	nnnn0d 10230	. . . . . . . . . 10
11		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
12		eqid 2404	. . . . . . . . . . 11
13		rpvmasum.l	. . . . . . . . . . 11 RHom
14	11, 12, 13	znzrhfo 16783	. . . . . . . . . 10
15		fof 5612	. . . . . . . . . 10
16	10, 14, 15	3syl 19	. . . . . . . . 9
17		dchrisum0flblem1.1	. . . . . . . . . 10
18		prmz 13038	. . . . . . . . . 10
19	17, 18	syl 16	. . . . . . . . 9
20	16, 19	ffvelrnd 5830	. . . . . . . 8
21	8, 20	ffvelrnd 5830	. . . . . . 7
22		elfznn0 11039	. . . . . . 7
23		reexpcl 11353	. . . . . . 7 $/\$
24	21, 22, 23	syl2an 464	. . . . . 6 $/\$
25	7, 24	fsumrecl 12483	. . . . 5
26	25	adantr 452	. . . 4 $/\$
27		breq1 4175	. . . . . 6
28		breq1 4175	. . . . . 6
29		1le1 9606	. . . . . 6
30		0le1 9507	. . . . . 6
31	27, 28, 29, 30	keephyp 3753	. . . . 5
32	31	a1i 11	. . . 4 $/\$
33		dchrisum0flblem1.2	. . . . . . . . . 10
34		nn0uz 10476	. . . . . . . . . 10
35	33, 34	syl6eleq 2494	. . . . . . . . 9
36		fzn0 11026	. . . . . . . . 9
37	35, 36	sylibr 204	. . . . . . . 8
38		hashnncl 11600	. . . . . . . . 9
39	7, 38	syl 16	. . . . . . . 8
40	37, 39	mpbird 224	. . . . . . 7
41	40	adantr 452	. . . . . 6 $/\$
42	41	nnge1d 9998	. . . . 5 $/\$
43		simpr 448	. . . . . . . . 9 $/\$
44	43	oveq1d 6055	. . . . . . . 8 $/\$
45		elfzelz 11015	. . . . . . . . 9
46		1exp 11364	. . . . . . . . 9
47	45, 46	syl 16	. . . . . . . 8
48	44, 47	sylan9eq 2456	. . . . . . 7 $/\$ $/\$
49	48	sumeq2dv 12452	. . . . . 6 $/\$
50		fzfid 11267	. . . . . . 7 $/\$
51		ax-1cn 9004	. . . . . . 7
52		fsumconst 12528	. . . . . . 7 $/\$
53	50, 51, 52	sylancl 644	. . . . . 6 $/\$
54	41	nncnd 9972	. . . . . . 7 $/\$
55	54	mulid1d 9061	. . . . . 6 $/\$
56	49, 53, 55	3eqtrd 2440	. . . . 5 $/\$
57	42, 56	breqtrrd 4198	. . . 4 $/\$
58	5, 6, 26, 32, 57	letrd 9183	. . 3 $/\$
59		oveq1 6047	. . . . . . 7
60	59	breq1d 4182	. . . . . 6
61		oveq1 6047	. . . . . . 7
62	61	breq1d 4182	. . . . . 6
63	21	adantr 452	. . . . . . . . . 10 $/\$
64		resubcl 9321	. . . . . . . . . 10 $/\$
65	1, 63, 64	sylancr 645	. . . . . . . . 9 $/\$
66	65	adantr 452	. . . . . . . 8 $/\$ $/\$
67	66	leidd 9549	. . . . . . 7 $/\$ $/\$
68	65	recnd 9070	. . . . . . . . 9 $/\$
69	68	adantr 452	. . . . . . . 8 $/\$ $/\$
70	69	mulid2d 9062	. . . . . . 7 $/\$ $/\$
71		nn0p1nn 10215	. . . . . . . . . . . . 13
72	33, 71	syl 16	. . . . . . . . . . . 12
73	72	ad3antrrr 711	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74	73	0expd 11494	. . . . . . . . . 10 $/\$ $/\$ $/\$
75		simpr 448	. . . . . . . . . . 11 $/\$ $/\$ $/\$
76	75	oveq1d 6055	. . . . . . . . . 10 $/\$ $/\$ $/\$
77	74, 76, 75	3eqtr4d 2446	. . . . . . . . 9 $/\$ $/\$ $/\$
78		neg1cn 10023	. . . . . . . . . . . . 13
79	33	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$
80		expp1 11343	. . . . . . . . . . . . 13 $/\$
81	78, 79, 80	sylancr 645	. . . . . . . . . . . 12 $/\$ $/\$
82		prmnn 13037	. . . . . . . . . . . . . . . . . . . . . . 23
83	17, 82	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
84	83, 33	nnexpcld 11499	. . . . . . . . . . . . . . . . . . . . 21
85	84	nncnd 9972	. . . . . . . . . . . . . . . . . . . 20
86	85	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
87	86	sqsqrd 12196	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
88	87	oveq2d 6056	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
89	17	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
90		nnq 10543	. . . . . . . . . . . . . . . . . . 19
91	90	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92		nnne0 9988	. . . . . . . . . . . . . . . . . . 19
93	92	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
94		2z 10268	. . . . . . . . . . . . . . . . . . 19
95	94	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
96		pcexp 13188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
97	89, 91, 93, 95, 96	syl121anc 1189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
98	79	nn0zd 10329	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
99		pcid 13201	. . . . . . . . . . . . . . . . . 18 $/\$
100	89, 98, 99	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
101	88, 97, 100	3eqtr3rd 2445	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102	101	oveq2d 6056	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	78	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104		simpr 448	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
105	89, 104	pccld 13179	. . . . . . . . . . . . . . . 16 $/\$ $/\$
106		2nn0 10194	. . . . . . . . . . . . . . . . 17
107	106	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
108	103, 105, 107	expmuld 11481	. . . . . . . . . . . . . . 15 $/\$ $/\$
109		sqneg 11397	. . . . . . . . . . . . . . . . . . 19
110	51, 109	ax-mp 8	. . . . . . . . . . . . . . . . . 18
111		sq1 11431	. . . . . . . . . . . . . . . . . 18
112	110, 111	eqtri 2424	. . . . . . . . . . . . . . . . 17
113	112	oveq1i 6050	. . . . . . . . . . . . . . . 16
114	105	nn0zd 10329	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
115		1exp 11364	. . . . . . . . . . . . . . . . 17
116	114, 115	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	113, 116	syl5eq 2448	. . . . . . . . . . . . . . 15 $/\$ $/\$
118	102, 108, 117	3eqtrd 2440	. . . . . . . . . . . . . 14 $/\$ $/\$
119	118	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ $/\$
120	78	mulid2i 9049	. . . . . . . . . . . . 13
121	119, 120	syl6eq 2452	. . . . . . . . . . . 12 $/\$ $/\$
122	81, 121	eqtrd 2436	. . . . . . . . . . 11 $/\$ $/\$
123	122	adantr 452	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	21	recnd 9070	. . . . . . . . . . . . . . 15
125	124	adantr 452	. . . . . . . . . . . . . 14 $/\$
126	125	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
127	126	negnegd 9358	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
128		simpr 448	. . . . . . . . . . . . . . . . 17 $/\$
129	128	ad2antrr 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
130		rpvmasum2.g	. . . . . . . . . . . . . . . . . . 19 DChr
131		rpvmasum2.d	. . . . . . . . . . . . . . . . . . 19
132		dchrisum0f.x	. . . . . . . . . . . . . . . . . . . 20
133	132	ad3antrrr 711	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
134		eqid 2404	. . . . . . . . . . . . . . . . . . 19 Unit Unit
135	130, 11, 131, 12, 134, 132, 20	dchrn0 20987	. . . . . . . . . . . . . . . . . . . . 21 Unit
136	135	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
137	136	biimpa 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
138	130, 131, 133, 11, 134, 137	dchrabs 20997	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
139		eqeq1 2410	. . . . . . . . . . . . . . . . . 18
140	138, 139	syl5ibcom 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
141	140	necon3ad 2603	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
142	129, 141	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	63	ad2antrr 707	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
144	143	absord 12173	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
145	144	ord 367	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	142, 145	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147	146, 138	eqtr3d 2438	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
148	147	negeqd 9256	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
149	127, 148	eqtr3d 2438	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150	149	oveq1d 6055	. . . . . . . . . 10 $/\$ $/\$ $/\$
151	123, 150, 149	3eqtr4d 2446	. . . . . . . . 9 $/\$ $/\$ $/\$
152	77, 151	pm2.61dane 2645	. . . . . . . 8 $/\$ $/\$
153	152	oveq2d 6056	. . . . . . 7 $/\$ $/\$
154	67, 70, 153	3brtr4d 4202	. . . . . 6 $/\$ $/\$
155	68	mul02d 9220	. . . . . . . 8 $/\$
156		peano2nn0 10216	. . . . . . . . . . . . 13
157	33, 156	syl 16	. . . . . . . . . . . 12
158	21, 157	reexpcld 11495	. . . . . . . . . . 11
159	158	adantr 452	. . . . . . . . . 10 $/\$
160	159	recnd 9070	. . . . . . . . . . 11 $/\$
161	160	abscld 12193	. . . . . . . . . 10 $/\$
162	1	a1i 11	. . . . . . . . . 10 $/\$
163	159	leabsd 12172	. . . . . . . . . 10 $/\$
164	157	adantr 452	. . . . . . . . . . . 12 $/\$
165	125, 164	absexpd 12209	. . . . . . . . . . 11 $/\$
166	125	abscld 12193	. . . . . . . . . . . 12 $/\$
167	125	absge0d 12201	. . . . . . . . . . . 12 $/\$
168	130, 131, 11, 12, 132, 20	dchrabs2 20999	. . . . . . . . . . . . 13
169	168	adantr 452	. . . . . . . . . . . 12 $/\$
170		exple1 11394	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
171	166, 167, 169, 164, 170	syl31anc 1187	. . . . . . . . . . 11 $/\$
172	165, 171	eqbrtrd 4192	. . . . . . . . . 10 $/\$
173	159, 161, 162, 163, 172	letrd 9183	. . . . . . . . 9 $/\$
174		subge0 9497	. . . . . . . . . 10 $/\$
175	1, 159, 174	sylancr 645	. . . . . . . . 9 $/\$
176	173, 175	mpbird 224	. . . . . . . 8 $/\$
177	155, 176	eqbrtrd 4192	. . . . . . 7 $/\$
178	177	adantr 452	. . . . . 6 $/\$ $/\$
179	60, 62, 154, 178	ifbothda 3729	. . . . 5 $/\$
180	1, 3	keepel 3756	. . . . . . 7
181	180	a1i 11	. . . . . 6 $/\$
182		resubcl 9321	. . . . . . 7 $/\$
183	1, 159, 182	sylancr 645	. . . . . 6 $/\$
184	128	necomd 2650	. . . . . . . 8 $/\$
185	63	leabsd 12172	. . . . . . . . . 10 $/\$
186	63, 166, 162, 185, 169	letrd 9183	. . . . . . . . 9 $/\$
187	63, 162, 186	leltned 9180	. . . . . . . 8 $/\$
188	184, 187	mpbird 224	. . . . . . 7 $/\$
189		posdif 9477	. . . . . . . 8 $/\$
190	63, 1, 189	sylancl 644	. . . . . . 7 $/\$
191	188, 190	mpbid 202	. . . . . 6 $/\$
192		lemuldiv 9845	. . . . . 6 $/\$ $/\$ $/\$
193	181, 183, 65, 191, 192	syl112anc 1188	. . . . 5 $/\$
194	179, 193	mpbid 202	. . . 4 $/\$
195	33	nn0zd 10329	. . . . . . . 8
196		fzval3 11135	. . . . . . . 8 ..^
197	195, 196	syl 16	. . . . . . 7 ..^
198	197	adantr 452	. . . . . 6 $/\$ ..^
199	198	sumeq1d 12450	. . . . 5 $/\$ ..^
200		0nn0 10192	. . . . . . 7
201	200	a1i 11	. . . . . 6 $/\$
202	157, 34	syl6eleq 2494	. . . . . . 7
203	202	adantr 452	. . . . . 6 $/\$
204	125, 128, 201, 203	geoserg 12600	. . . . 5 $/\$ ..^
205	125	exp0d 11472	. . . . . . 7 $/\$
206	205	oveq1d 6055	. . . . . 6 $/\$
207	206	oveq1d 6055	. . . . 5 $/\$
208	199, 204, 207	3eqtrd 2440	. . . 4 $/\$
209	194, 208	breqtrrd 4198	. . 3 $/\$
210	58, 209	pm2.61dane 2645	. 2
211		rpvmasum2.1	. . . . 5
212		dchrisum0f.f	. . . . 5
213	11, 13, 9, 130, 131, 211, 212	dchrisum0fval 21152	. . . 4
214	84, 213	syl 16	. . 3
215		fveq2 5687	. . . . 5
216	215	fveq2d 5691	. . . 4
217		eqid 2404	. . . . . 6
218	217	dvdsppwf1o 20924	. . . . 5 $/\$
219	17, 33, 218	syl2anc 643	. . . 4
220		oveq2 6048	. . . . . 6
221		ovex 6065	. . . . . 6
222	220, 217, 221	fvmpt3i 5768	. . . . 5
223	222	adantl 453	. . . 4 $/\$
224	8	adantr 452	. . . . . 6 $/\$
225		elrabi 3050	. . . . . . . 8
226	225	nnzd 10330	. . . . . . 7
227		ffvelrn 5827	. . . . . . 7 $/\$
228	16, 226, 227	syl2an 464	. . . . . 6 $/\$
229	224, 228	ffvelrnd 5830	. . . . 5 $/\$
230	229	recnd 9070	. . . 4 $/\$
231	216, 7, 219, 223, 230	fsumf1o 12472	. . 3
232		zsubrg 16707	. . . . . . . . . . 11 SubRingℂ_fld
233		eqid 2404	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
234	233	subrgsubm 15836	. . . . . . . . . . 11 SubRingℂ_fld SubMndmulGrpℂ_fld
235	232, 234	mp1i 12	. . . . . . . . . 10 $/\$ SubMndmulGrpℂ_fld
236	22	adantl 453	. . . . . . . . . 10 $/\$
237	19	adantr 452	. . . . . . . . . 10 $/\$
238		eqid 2404	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
239		cnfldex 16661	. . . . . . . . . . . . 13 ℂ_fld
240		zex 10247	. . . . . . . . . . . . 13
241		eqid 2404	. . . . . . . . . . . . . 14 ℂ_fld ↾_s ℂ_fld ↾_s
242	241, 233	mgpress 15614	. . . . . . . . . . . . 13 ℂ_fld $/\$ mulGrpℂ_fld ↾_s mulGrpℂ_fld ↾_s
243	239, 240, 242	mp2an 654	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℂ_fld ↾_s
244	243	eqcomi 2408	. . . . . . . . . . 11 mulGrpℂ_fld ↾_s mulGrpℂ_fld ↾_s
245		eqid 2404	. . . . . . . . . . 11 ._gmulGrpℂ_fld ↾_s ._gmulGrpℂ_fld ↾_s
246	238, 244, 245	submmulg 14880	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℂ_fld ↾_s
247	235, 236, 237, 246	syl3anc 1184	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℂ_fld ↾_s
248	83	nncnd 9972	. . . . . . . . . 10
249		cnfldexp 16689	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
250	248, 22, 249	syl2an 464	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
251	247, 250	eqtr3d 2438	. . . . . . . 8 $/\$ ._gmulGrpℂ_fld ↾_s
252	251	fveq2d 5691	. . . . . . 7 $/\$ ._gmulGrpℂ_fld ↾_s
253	11	zncrng 16780	. . . . . . . . . . 11
254		crngrng 15629	. . . . . . . . . . 11
255	10, 253, 254	3syl 19	. . . . . . . . . 10
256	241, 13	zrhrhm 16748	. . . . . . . . . 10 ℂ_fld ↾_s RingHom
257		eqid 2404	. . . . . . . . . . 11 mulGrpℂ_fld ↾_s mulGrpℂ_fld ↾_s
258		eqid 2404	. . . . . . . . . . 11 mulGrp mulGrp
259	257, 258	rhmmhm 15780	. . . . . . . . . 10 ℂ_fld ↾_s RingHom mulGrpℂ_fld ↾_s MndHom mulGrp
260	255, 256, 259	3syl 19	. . . . . . . . 9 mulGrpℂ_fld ↾_s MndHom mulGrp
261	260	adantr 452	. . . . . . . 8 $/\$ mulGrpℂ_fld ↾_s MndHom mulGrp
262		subrgsubg 15829	. . . . . . . . . . 11 SubRingℂ_fld SubGrpℂ_fld
263	241	subgbas 14903	. . . . . . . . . . 11 SubGrpℂ_fld ℂ_fld ↾_s
264	232, 262, 263	mp2b 10	. . . . . . . . . 10 ℂ_fld ↾_s
265	257, 264	mgpbas 15609	. . . . . . . . 9 mulGrpℂ_fld ↾_s
266		eqid 2404	. . . . . . . . 9 ._gmulGrp ._gmulGrp
267	265, 245, 266	mhmmulg 14877	. . . . . . . 8 mulGrpℂ_fld ↾_s MndHom mulGrp $/\$ $/\$ ._gmulGrpℂ_fld ↾_s ._gmulGrp
268	261, 236, 237, 267	syl3anc 1184	. . . . . . 7 $/\$ ._gmulGrpℂ_fld ↾_s ._gmulGrp
269	252, 268	eqtr3d 2438	. . . . . 6 $/\$ ._gmulGrp
270	269	fveq2d 5691	. . . . 5 $/\$ ._gmulGrp
271	130, 11, 131	dchrmhm 20978	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
272	271, 132	sseldi 3306	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
273	272	adantr 452	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
274	20	adantr 452	. . . . . 6 $/\$
275	258, 12	mgpbas 15609	. . . . . . 7 mulGrp
276	275, 266, 238	mhmmulg 14877	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
277	273, 236, 274, 276	syl3anc 1184	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
278		cnfldexp 16689	. . . . . 6 $/\$ ._gmulGrpℂ_fld
279	124, 22, 278	syl2an 464	. . . . 5 $/\$ ._gmulGrpℂ_fld
280	270, 277, 279	3eqtrd 2440	. . . 4 $/\$
281	280	sumeq2dv 12452	. . 3
282	214, 231, 281	3eqtrd 2440	. 2
283	210, 282	breqtrrd 4198	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721

wne 2567

crab 2670

cvv 2916

c0 3588

cif 3699 class class class wbr 4172

cmpt 4226

wf 5409

wfo 5411

wf1o 5412

cfv 5413 (class class class)co 6040

cfn 7068

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cmin 9247

cneg 9248

cdiv 9633

cn 9956

c2 10005

cn0 10177

cz 10238

cuz 10444

cq 10530

cfz 10999 ..^cfzo 11090

cexp 11337

chash 11573

csqr 11993

cabs 11994

csu 12434

cdivides 12807

cprime 13034

cpc 13165

cbs 13424 ↾_s cress 13425

c0g 13678 ._gcmg 14644 MndHom cmhm 14691 SubMndcsubmnd 14692 SubGrpcsubg 14893 mulGrpcmgp 15603

crg 15615

ccrg 15616 Unitcui 15699 RingHom crh 15772 SubRingcsubrg 15819 ℂ_fldccnfld 16658

RHomczrh 16733 ℤ/nℤczn 16736 DChrcdchr 20969

This theorem is referenced by: dchrisum0flblem2 21156 dchrisum0flb 21157

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-disj 4143 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-tpos 6438 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-omul 6688 df-er 6864 df-ec 6866 df-qs 6870 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-acn 7785 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-dvds 12808 df-gcd 12962 df-prm 13035 df-pc 13166 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-divs 13690 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-mhm 14693 df-submnd 14694 df-grp 14767 df-minusg 14768 df-sbg 14769 df-mulg 14770 df-subg 14896 df-nsg 14897 df-eqg 14898 df-ghm 14959 df-cntz 15071 df-od 15122 df-cmn 15369 df-abl 15370 df-mgp 15604 df-rng 15618 df-cring 15619 df-ur 15620 df-oppr 15683 df-dvdsr 15701 df-unit 15702 df-invr 15732 df-dvr 15743 df-rnghom 15774 df-drng 15792 df-subrg 15821 df-lmod 15907 df-lss 15964 df-lsp 16003 df-sra 16199 df-rgmod 16200 df-lidl 16201 df-rsp 16202 df-2idl 16258 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-zrh 16737 df-zn 16740 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407 df-cxp 20408 df-dchr 20970

W3C validator