dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 24425

Description: Lemma for dchrisum0flb 24427. 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		1red 9676	. . . . 5 $/\$ $/\$
2		0red 9662	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3904	. . . 4 $/\$
4		1red 9676	. . . 4 $/\$
5		fzfid 12224	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10949	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2471	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 19195	. . . . . . . . . 10
13		fof 5806	. . . . . . . . . 10
14	8, 12, 13	3syl 18	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 14705	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	14, 17	ffvelrnd 6038	. . . . . . . 8
19	6, 18	ffvelrnd 6038	. . . . . . 7
20		elfznn0 11913	. . . . . . 7
21		reexpcl 12327	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 485	. . . . . 6 $/\$
23	5, 22	fsumrecl 13877	. . . . 5
24	23	adantr 472	. . . 4 $/\$
25		breq1 4398	. . . . . 6
26		breq1 4398	. . . . . 6
27		1le1 10262	. . . . . 6
28		0le1 10158	. . . . . 6
29	25, 26, 27, 28	keephyp 3936	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 11217	. . . . . . . . . 10
33	31, 32	syl6eleq 2559	. . . . . . . . 9
34		fzn0 11839	. . . . . . . . 9
35	33, 34	sylibr 217	. . . . . . . 8
36		hashnncl 12585	. . . . . . . . 9
37	5, 36	syl 17	. . . . . . . 8
38	35, 37	mpbird 240	. . . . . . 7
39	38	adantr 472	. . . . . 6 $/\$
40	39	nnge1d 10674	. . . . 5 $/\$
41		simpr 468	. . . . . . . . 9 $/\$
42	41	oveq1d 6323	. . . . . . . 8 $/\$
43		elfzelz 11826	. . . . . . . . 9
44		1exp 12339	. . . . . . . . 9
45	43, 44	syl 17	. . . . . . . 8
46	42, 45	sylan9eq 2525	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13846	. . . . . 6 $/\$
48		fzfid 12224	. . . . . . 7 $/\$
49		ax-1cn 9615	. . . . . . 7
50		fsumconst 13928	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 675	. . . . . 6 $/\$
52	39	nncnd 10647	. . . . . . 7 $/\$
53	52	mulid1d 9678	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2509	. . . . 5 $/\$
55	40, 54	breqtrrd 4422	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9809	. . 3 $/\$
57		oveq1 6315	. . . . . . 7
58	57	breq1d 4405	. . . . . 6
59		oveq1 6315	. . . . . . 7
60	59	breq1d 4405	. . . . . 6
61		1re 9660	. . . . . . . . . 10
62	19	adantr 472	. . . . . . . . . 10 $/\$
63		resubcl 9958	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 676	. . . . . . . . 9 $/\$
65	64	adantr 472	. . . . . . . 8 $/\$ $/\$
66	65	leidd 10201	. . . . . . 7 $/\$ $/\$
67	64	recnd 9687	. . . . . . . . 9 $/\$
68	67	adantr 472	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9679	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10933	. . . . . . . . . . . . 13
71	31, 70	syl 17	. . . . . . . . . . . 12
72	71	ad3antrrr 744	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12470	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6323	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2515	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10735	. . . . . . . . . . . . 13
78	31	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 12317	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 676	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 14704	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12475	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10647	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 740	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrtd 13578	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 11300	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10664	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10993	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 14888	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1297	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 11061	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 14901	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2514	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 14879	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10910	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 12457	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 12408	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6318	. . . . . . . . . . . . . . . 16
110	104	nn0zd 11061	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 12339	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2517	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2509	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9664	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2521	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2505	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 472	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9687	. . . . . . . . . . . . . . 15
121	120	adantr 472	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9996	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		simpr 468	. . . . . . . . . . . . . . . . 17 $/\$
125	124	ad2antrr 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126		rpvmasum2.g	. . . . . . . . . . . . . . . . . . 19 DChr
127		rpvmasum2.d	. . . . . . . . . . . . . . . . . . 19
128		dchrisum0f.x	. . . . . . . . . . . . . . . . . . . 20
129	128	ad3antrrr 744	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130		eqid 2471	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 24257	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 740	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 24267	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2475	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 228	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 13554	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 384	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2507	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9889	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2507	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6323	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2515	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2730	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6324	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4426	. . . . . 6 $/\$ $/\$
151	67	mul02d 9849	. . . . . . . 8 $/\$
152		peano2nn0 10934	. . . . . . . . . . . . 13
153	31, 152	syl 17	. . . . . . . . . . . 12
154	19, 153	reexpcld 12471	. . . . . . . . . . 11
155	154	adantr 472	. . . . . . . . . 10 $/\$
156	155	recnd 9687	. . . . . . . . . . 11 $/\$
157	156	abscld 13575	. . . . . . . . . 10 $/\$
158		1red 9676	. . . . . . . . . 10 $/\$
159	155	leabsd 13553	. . . . . . . . . 10 $/\$
160	153	adantr 472	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 13591	. . . . . . . . . . 11 $/\$
162	121	abscld 13575	. . . . . . . . . . . 12 $/\$
163	121	absge0d 13583	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 24269	. . . . . . . . . . . . 13
165	164	adantr 472	. . . . . . . . . . . 12 $/\$
166		exple1 12370	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1295	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4416	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9809	. . . . . . . . 9 $/\$
170		subge0 10148	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 676	. . . . . . . . 9 $/\$
172	169, 171	mpbird 240	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4416	. . . . . . 7 $/\$
174	173	adantr 472	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3907	. . . . 5 $/\$
176		0re 9661	. . . . . . . 8
177	61, 176	keepel 3939	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9958	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 676	. . . . . 6 $/\$
181	124	necomd 2698	. . . . . . . 8 $/\$
182	62	leabsd 13553	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9809	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9805	. . . . . . . 8 $/\$
185	181, 184	mpbird 240	. . . . . . 7 $/\$
186		posdif 10128	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 675	. . . . . . 7 $/\$
188	185, 187	mpbid 215	. . . . . 6 $/\$
189		lemuldiv 10508	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1296	. . . . 5 $/\$
191	175, 190	mpbid 215	. . . 4 $/\$
192	31	nn0zd 11061	. . . . . . . 8
193		fzval3 12012	. . . . . . . 8 ..^
194	192, 193	syl 17	. . . . . . 7 ..^
195	194	adantr 472	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13844	. . . . 5 $/\$ ..^
197		0nn0 10908	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2559	. . . . . . 7
200	199	adantr 472	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 14001	. . . . 5 $/\$ ..^
202	121	exp0d 12448	. . . . . . 7 $/\$
203	202	oveq1d 6323	. . . . . 6 $/\$
204	203	oveq1d 6323	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2509	. . . 4 $/\$
206	191, 205	breqtrrd 4422	. . 3 $/\$
207	56, 206	pm2.61dane 2730	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 24422	. . . 4
211	83, 210	syl 17	. . 3
212		fveq2 5879	. . . . 5
213	212	fveq2d 5883	. . . 4
214		eqid 2471	. . . . . 6
215	214	dvdsppwf1o 24194	. . . . 5 $/\$
216	15, 31, 215	syl2anc 673	. . . 4
217		oveq2 6316	. . . . . 6
218		ovex 6336	. . . . . 6
219	217, 214, 218	fvmpt3i 5968	. . . . 5
220	219	adantl 473	. . . 4 $/\$
221	6	adantr 472	. . . . . 6 $/\$
222		elrabi 3181	. . . . . . . 8
223	222	nnzd 11062	. . . . . . 7
224		ffvelrn 6035	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 485	. . . . . 6 $/\$
226	221, 225	ffvelrnd 6038	. . . . 5 $/\$
227	226	recnd 9687	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13866	. . 3
229		zsubrg 19098	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2471	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 18099	. . . . . . . . . . 11 SubRingℂ_fld SubMndmulGrpℂ_fld
232	229, 231	mp1i 13	. . . . . . . . . 10 $/\$ SubMndmulGrpℂ_fld
233	20	adantl 473	. . . . . . . . . 10 $/\$
234	17	adantr 472	. . . . . . . . . 10 $/\$
235		eqid 2471	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 19140	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2480	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2471	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 16871	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1292	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10647	. . . . . . . . . 10
242		cnfldexp 19078	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 485	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2507	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5883	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 19192	. . . . . . . . . . 11
247		crngring 17869	. . . . . . . . . . 11
248	8, 246, 247	3syl 18	. . . . . . . . . 10
249	11	zrhrhm 19160	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2471	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2471	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 18028	. . . . . . . . . 10 ℤ_ring RingHom mulGrpℤ_ring MndHom mulGrp
253	248, 249, 252	3syl 18	. . . . . . . . 9 mulGrpℤ_ring MndHom mulGrp
254	253	adantr 472	. . . . . . . 8 $/\$ mulGrpℤ_ring MndHom mulGrp
255		zringbas 19122	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 17807	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2471	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 16868	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1292	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2507	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5883	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 24248	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3416	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 472	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 472	. . . . . 6 $/\$
266	251, 10	mgpbas 17807	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 16868	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1292	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 19078	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 485	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2509	. . . 4 $/\$
272	271	sumeq2dv 13846	. . 3
273	211, 228, 272	3eqtrd 2509	. 2
274	207, 273	breqtrrd 4422	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641

crab 2760

c0 3722

cif 3872 class class class wbr 4395

cmpt 4454

wf 5585

wfo 5587

wf1o 5588

cfv 5589 (class class class)co 6308

cfn 7587

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cneg 9881

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

cuz 11182

cq 11287

cfz 11810 ..^cfzo 11942

cexp 12310

chash 12553

csqrt 13373

cabs 13374

csu 13829

cdvds 14382

cprime 14701

cpc 14865

cbs 15199 ↾_s cress 15200

c0g 15416 MndHom cmhm 16658 SubMndcsubmnd 16659 ._gcmg 16750 mulGrpcmgp 17801

crg 17858

ccrg 17859 Unitcui 17945 RingHom crh 18018 SubRingcsubrg 18082 ℂ_fldccnfld 19047 ℤ_ringzring 19116

RHomczrh 19148 ℤ/nℤczn 19151 DChrcdchr 24239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-tpos 6991 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-omul 7205 df-er 7381 df-ec 7383 df-qs 7387 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-acn 8394 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-qus 15487 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-mhm 16660 df-submnd 16661 df-grp 16751 df-minusg 16752 df-sbg 16753 df-mulg 16754 df-subg 16892 df-nsg 16893 df-eqg 16894 df-ghm 16959 df-cntz 17049 df-od 17250 df-cmn 17510 df-abl 17511 df-mgp 17802 df-ur 17814 df-ring 17860 df-cring 17861 df-oppr 17929 df-dvdsr 17947 df-unit 17948 df-invr 17978 df-dvr 17989 df-rnghom 18021 df-drng 18055 df-subrg 18084 df-lmod 18171 df-lss 18234 df-lsp 18273 df-sra 18473 df-rgmod 18474 df-lidl 18475 df-rsp 18476 df-2idl 18533 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-zring 19117 df-zrh 19152 df-zn 19155 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cxp 23586 df-dchr 24240

This theorem is referenced by: dchrisum0flblem2 24426 dchrisum0flb 24427

W3C validator