dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 24288

Description: Lemma for dchrisum0flb 24290. 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 9609	. . . . 5 $/\$ $/\$
2		0red 9595	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3886	. . . 4 $/\$
4		1red 9609	. . . 4 $/\$
5		fzfid 12136	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10876	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2428	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 19060	. . . . . . . . . 10
13		fof 5753	. . . . . . . . . 10
14	8, 12, 13	3syl 18	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 14569	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	14, 17	ffvelrnd 5982	. . . . . . . 8
19	6, 18	ffvelrnd 5982	. . . . . . 7
20		elfznn0 11838	. . . . . . 7
21		reexpcl 12239	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 479	. . . . . 6 $/\$
23	5, 22	fsumrecl 13743	. . . . 5
24	23	adantr 466	. . . 4 $/\$
25		breq1 4369	. . . . . 6
26		breq1 4369	. . . . . 6
27		1le1 10191	. . . . . 6
28		0le1 10088	. . . . . 6
29	25, 26, 27, 28	keephyp 3918	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 11144	. . . . . . . . . 10
33	31, 32	syl6eleq 2516	. . . . . . . . 9
34		fzn0 11764	. . . . . . . . 9
35	33, 34	sylibr 215	. . . . . . . 8
36		hashnncl 12497	. . . . . . . . 9
37	5, 36	syl 17	. . . . . . . 8
38	35, 37	mpbird 235	. . . . . . 7
39	38	adantr 466	. . . . . 6 $/\$
40	39	nnge1d 10603	. . . . 5 $/\$
41		simpr 462	. . . . . . . . 9 $/\$
42	41	oveq1d 6264	. . . . . . . 8 $/\$
43		elfzelz 11751	. . . . . . . . 9
44		1exp 12251	. . . . . . . . 9
45	43, 44	syl 17	. . . . . . . 8
46	42, 45	sylan9eq 2482	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13712	. . . . . 6 $/\$
48		fzfid 12136	. . . . . . 7 $/\$
49		ax-1cn 9548	. . . . . . 7
50		fsumconst 13794	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 666	. . . . . 6 $/\$
52	39	nncnd 10576	. . . . . . 7 $/\$
53	52	mulid1d 9611	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2466	. . . . 5 $/\$
55	40, 54	breqtrrd 4393	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9743	. . 3 $/\$
57		oveq1 6256	. . . . . . 7
58	57	breq1d 4376	. . . . . 6
59		oveq1 6256	. . . . . . 7
60	59	breq1d 4376	. . . . . 6
61		1re 9593	. . . . . . . . . 10
62	19	adantr 466	. . . . . . . . . 10 $/\$
63		resubcl 9889	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 667	. . . . . . . . 9 $/\$
65	64	adantr 466	. . . . . . . 8 $/\$ $/\$
66	65	leidd 10131	. . . . . . 7 $/\$ $/\$
67	64	recnd 9620	. . . . . . . . 9 $/\$
68	67	adantr 466	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9612	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10860	. . . . . . . . . . . . 13
71	31, 70	syl 17	. . . . . . . . . . . 12
72	71	ad3antrrr 734	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12382	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6264	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2472	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10664	. . . . . . . . . . . . 13
78	31	ad2antrr 730	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 12229	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 667	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 14568	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12387	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10576	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrtd 13444	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6265	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 11228	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10593	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10920	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 14752	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1269	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 10989	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 14765	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2471	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6265	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 14743	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10837	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 12369	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 12320	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6259	. . . . . . . . . . . . . . . 16
110	104	nn0zd 10989	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 12251	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2474	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2466	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6264	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9597	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2478	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2462	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9620	. . . . . . . . . . . . . . 15
121	120	adantr 466	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 730	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9928	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		simpr 462	. . . . . . . . . . . . . . . . 17 $/\$
125	124	ad2antrr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126		rpvmasum2.g	. . . . . . . . . . . . . . . . . . 19 DChr
127		rpvmasum2.d	. . . . . . . . . . . . . . . . . . 19
128		dchrisum0f.x	. . . . . . . . . . . . . . . . . . . 20
129	128	ad3antrrr 734	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130		eqid 2428	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 24120	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 730	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 486	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 24130	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2432	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 223	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2614	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 730	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 13421	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 378	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9820	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2464	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6264	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2472	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2688	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6265	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4397	. . . . . 6 $/\$ $/\$
151	67	mul02d 9782	. . . . . . . 8 $/\$
152		peano2nn0 10861	. . . . . . . . . . . . 13
153	31, 152	syl 17	. . . . . . . . . . . 12
154	19, 153	reexpcld 12383	. . . . . . . . . . 11
155	154	adantr 466	. . . . . . . . . 10 $/\$
156	155	recnd 9620	. . . . . . . . . . 11 $/\$
157	156	abscld 13441	. . . . . . . . . 10 $/\$
158		1red 9609	. . . . . . . . . 10 $/\$
159	155	leabsd 13420	. . . . . . . . . 10 $/\$
160	153	adantr 466	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 13457	. . . . . . . . . . 11 $/\$
162	121	abscld 13441	. . . . . . . . . . . 12 $/\$
163	121	absge0d 13449	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 24132	. . . . . . . . . . . . 13
165	164	adantr 466	. . . . . . . . . . . 12 $/\$
166		exple1 12282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1267	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4387	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9743	. . . . . . . . 9 $/\$
170		subge0 10078	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 667	. . . . . . . . 9 $/\$
172	169, 171	mpbird 235	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4387	. . . . . . 7 $/\$
174	173	adantr 466	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3889	. . . . 5 $/\$
176		0re 9594	. . . . . . . 8
177	61, 176	keepel 3921	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9889	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 667	. . . . . 6 $/\$
181	124	necomd 2656	. . . . . . . 8 $/\$
182	62	leabsd 13420	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9743	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9739	. . . . . . . 8 $/\$
185	181, 184	mpbird 235	. . . . . . 7 $/\$
186		posdif 10058	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 666	. . . . . . 7 $/\$
188	185, 187	mpbid 213	. . . . . 6 $/\$
189		lemuldiv 10437	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1268	. . . . 5 $/\$
191	175, 190	mpbid 213	. . . 4 $/\$
192	31	nn0zd 10989	. . . . . . . 8
193		fzval3 11933	. . . . . . . 8 ..^
194	192, 193	syl 17	. . . . . . 7 ..^
195	194	adantr 466	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13710	. . . . 5 $/\$ ..^
197		0nn0 10835	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2516	. . . . . . 7
200	199	adantr 466	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 13867	. . . . 5 $/\$ ..^
202	121	exp0d 12360	. . . . . . 7 $/\$
203	202	oveq1d 6264	. . . . . 6 $/\$
204	203	oveq1d 6264	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2466	. . . 4 $/\$
206	191, 205	breqtrrd 4393	. . 3 $/\$
207	56, 206	pm2.61dane 2688	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 24285	. . . 4
211	83, 210	syl 17	. . 3
212		fveq2 5825	. . . . 5
213	212	fveq2d 5829	. . . 4
214		eqid 2428	. . . . . 6
215	214	dvdsppwf1o 24057	. . . . 5 $/\$
216	15, 31, 215	syl2anc 665	. . . 4
217		oveq2 6257	. . . . . 6
218		ovex 6277	. . . . . 6
219	217, 214, 218	fvmpt3i 5913	. . . . 5
220	219	adantl 467	. . . 4 $/\$
221	6	adantr 466	. . . . . 6 $/\$
222		elrabi 3168	. . . . . . . 8
223	222	nnzd 10990	. . . . . . 7
224		ffvelrn 5979	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 479	. . . . . 6 $/\$
226	221, 225	ffvelrnd 5982	. . . . 5 $/\$
227	226	recnd 9620	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13732	. . 3
229		zsubrg 18964	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2428	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 17964	. . . . . . . . . . 11 SubRingℂ_fld SubMndmulGrpℂ_fld
232	229, 231	mp1i 13	. . . . . . . . . 10 $/\$ SubMndmulGrpℂ_fld
233	20	adantl 467	. . . . . . . . . 10 $/\$
234	17	adantr 466	. . . . . . . . . 10 $/\$
235		eqid 2428	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 19005	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2437	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2428	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 16736	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1264	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10576	. . . . . . . . . 10
242		cnfldexp 18944	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 479	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2464	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5829	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 19057	. . . . . . . . . . 11
247		crngring 17734	. . . . . . . . . . 11
248	8, 246, 247	3syl 18	. . . . . . . . . 10
249	11	zrhrhm 19025	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2428	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2428	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 17893	. . . . . . . . . 10 ℤ_ring RingHom mulGrpℤ_ring MndHom mulGrp
253	248, 249, 252	3syl 18	. . . . . . . . 9 mulGrpℤ_ring MndHom mulGrp
254	253	adantr 466	. . . . . . . 8 $/\$ mulGrpℤ_ring MndHom mulGrp
255		zringbas 18987	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 17672	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2428	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 16733	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1264	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2464	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5829	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 24111	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3405	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 466	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 466	. . . . . 6 $/\$
266	251, 10	mgpbas 17672	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 16733	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1264	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 18944	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 479	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2466	. . . 4 $/\$
272	271	sumeq2dv 13712	. . 3
273	211, 228, 272	3eqtrd 2466	. 2
274	207, 273	breqtrrd 4393	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370

wceq 1437

wcel 1872

wne 2599

crab 2718

c0 3704

cif 3854 class class class wbr 4366

cmpt 4425

wf 5540

wfo 5542

wf1o 5543

cfv 5544 (class class class)co 6249

cfn 7524

cc 9488

cr 9489

cc0 9490

c1 9491

caddc 9493

cmul 9495

clt 9626

cle 9627

cmin 9811

cneg 9812

cdiv 10220

cn 10560

c2 10610

cn0 10820

cz 10888

cuz 11110

cq 11215

cfz 11735 ..^cfzo 11866

cexp 12222

chash 12465

csqrt 13240

cabs 13241

csu 13695

cdvds 14248

cprime 14565

cpc 14729

cbs 15064 ↾_s cress 15065

c0g 15281 MndHom cmhm 16523 SubMndcsubmnd 16524 ._gcmg 16615 mulGrpcmgp 17666

crg 17723

ccrg 17724 Unitcui 17810 RingHom crh 17883 SubRingcsubrg 17947 ℂ_fldccnfld 18913 ℤ_ringzring 18981

RHomczrh 19013 ℤ/nℤczn 19016 DChrcdchr 24102

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-rep 4479 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541 ax-inf2 8099 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568 ax-addf 9569 ax-mulf 9570

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-nel 2602 df-ral 2719 df-rex 2720 df-reu 2721 df-rmo 2722 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-pss 3395 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-tp 3946 df-op 3948 df-uni 4163 df-int 4199 df-iun 4244 df-iin 4245 df-disj 4338 df-br 4367 df-opab 4426 df-mpt 4427 df-tr 4462 df-eprel 4707 df-id 4711 df-po 4717 df-so 4718 df-fr 4755 df-se 4756 df-we 4757 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-pred 5342 df-ord 5388 df-on 5389 df-lim 5390 df-suc 5391 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-isom 5553 df-riota 6211 df-ov 6252 df-oprab 6253 df-mpt2 6254 df-of 6489 df-om 6651 df-1st 6751 df-2nd 6752 df-supp 6870 df-tpos 6928 df-wrecs 6983 df-recs 7045 df-rdg 7083 df-1o 7137 df-2o 7138 df-oadd 7141 df-omul 7142 df-er 7318 df-ec 7320 df-qs 7324 df-map 7429 df-pm 7430 df-ixp 7478 df-en 7525 df-dom 7526 df-sdom 7527 df-fin 7528 df-fsupp 7837 df-fi 7878 df-sup 7909 df-inf 7910 df-oi 7978 df-card 8325 df-acn 8328 df-cda 8549 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9813 df-neg 9814 df-div 10221 df-nn 10561 df-2 10619 df-3 10620 df-4 10621 df-5 10622 df-6 10623 df-7 10624 df-8 10625 df-9 10626 df-10 10627 df-n0 10821 df-z 10889 df-dec 11003 df-uz 11111 df-q 11216 df-rp 11254 df-xneg 11360 df-xadd 11361 df-xmul 11362 df-ioo 11590 df-ioc 11591 df-ico 11592 df-icc 11593 df-fz 11736 df-fzo 11867 df-fl 11978 df-mod 12047 df-seq 12164 df-exp 12223 df-fac 12410 df-bc 12438 df-hash 12466 df-shft 13074 df-cj 13106 df-re 13107 df-im 13108 df-sqrt 13242 df-abs 13243 df-limsup 13469 df-clim 13495 df-rlim 13496 df-sum 13696 df-ef 14064 df-sin 14066 df-cos 14067 df-pi 14069 df-dvds 14249 df-gcd 14412 df-prm 14566 df-pc 14730 df-struct 15066 df-ndx 15067 df-slot 15068 df-base 15069 df-sets 15070 df-ress 15071 df-plusg 15146 df-mulr 15147 df-starv 15148 df-sca 15149 df-vsca 15150 df-ip 15151 df-tset 15152 df-ple 15153 df-ds 15155 df-unif 15156 df-hom 15157 df-cco 15158 df-rest 15264 df-topn 15265 df-0g 15283 df-gsum 15284 df-topgen 15285 df-pt 15286 df-prds 15289 df-xrs 15343 df-qtop 15349 df-imas 15350 df-qus 15352 df-xps 15353 df-mre 15435 df-mrc 15436 df-acs 15438 df-mgm 16431 df-sgrp 16470 df-mnd 16480 df-mhm 16525 df-submnd 16526 df-grp 16616 df-minusg 16617 df-sbg 16618 df-mulg 16619 df-subg 16757 df-nsg 16758 df-eqg 16759 df-ghm 16824 df-cntz 16914 df-od 17115 df-cmn 17375 df-abl 17376 df-mgp 17667 df-ur 17679 df-ring 17725 df-cring 17726 df-oppr 17794 df-dvdsr 17812 df-unit 17813 df-invr 17843 df-dvr 17854 df-rnghom 17886 df-drng 17920 df-subrg 17949 df-lmod 18036 df-lss 18099 df-lsp 18138 df-sra 18338 df-rgmod 18339 df-lidl 18340 df-rsp 18341 df-2idl 18399 df-psmet 18905 df-xmet 18906 df-met 18907 df-bl 18908 df-mopn 18909 df-fbas 18910 df-fg 18911 df-cnfld 18914 df-zring 18982 df-zrh 19017 df-zn 19020 df-top 19863 df-bases 19864 df-topon 19865 df-topsp 19866 df-cld 19976 df-ntr 19977 df-cls 19978 df-nei 20056 df-lp 20094 df-perf 20095 df-cn 20185 df-cnp 20186 df-haus 20273 df-tx 20519 df-hmeo 20712 df-fil 20803 df-fm 20895 df-flim 20896 df-flf 20897 df-xms 21277 df-ms 21278 df-tms 21279 df-cncf 21852 df-limc 22763 df-dv 22764 df-log 23448 df-cxp 23449 df-dchr 24103

This theorem is referenced by: dchrisum0flblem2 24289 dchrisum0flb 24290

W3C validator