dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 22642

Description: Lemma for dchrisum0flb 22644. 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 9389	. . . . 5 $/\$ $/\$
2		0red 9375	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3809	. . . 4 $/\$
4		1red 9389	. . . 4 $/\$
5		fzfid 11779	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10624	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2433	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 17822	. . . . . . . . . 10
13		fof 5608	. . . . . . . . . 10
14	8, 12, 13	3syl 20	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 13750	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	14, 17	ffvelrnd 5832	. . . . . . . 8
19	6, 18	ffvelrnd 5832	. . . . . . 7
20		elfznn0 11468	. . . . . . 7
21		reexpcl 11866	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 474	. . . . . 6 $/\$
23	5, 22	fsumrecl 13195	. . . . 5
24	23	adantr 462	. . . 4 $/\$
25		breq1 4283	. . . . . 6
26		breq1 4283	. . . . . 6
27		1le1 9952	. . . . . 6
28		0le1 9851	. . . . . 6
29	25, 26, 27, 28	keephyp 3842	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 10883	. . . . . . . . . 10
33	31, 32	syl6eleq 2523	. . . . . . . . 9
34		fzn0 11451	. . . . . . . . 9
35	33, 34	sylibr 212	. . . . . . . 8
36		hashnncl 12118	. . . . . . . . 9
37	5, 36	syl 16	. . . . . . . 8
38	35, 37	mpbird 232	. . . . . . 7
39	38	adantr 462	. . . . . 6 $/\$
40	39	nnge1d 10352	. . . . 5 $/\$
41		simpr 458	. . . . . . . . 9 $/\$
42	41	oveq1d 6095	. . . . . . . 8 $/\$
43		elfzelz 11440	. . . . . . . . 9
44		1exp 11877	. . . . . . . . 9
45	43, 44	syl 16	. . . . . . . 8
46	42, 45	sylan9eq 2485	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13164	. . . . . 6 $/\$
48		fzfid 11779	. . . . . . 7 $/\$
49		ax-1cn 9328	. . . . . . 7
50		fsumconst 13240	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 655	. . . . . 6 $/\$
52	39	nncnd 10326	. . . . . . 7 $/\$
53	52	mulid1d 9391	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2469	. . . . 5 $/\$
55	40, 54	breqtrrd 4306	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9516	. . 3 $/\$
57		oveq1 6087	. . . . . . 7
58	57	breq1d 4290	. . . . . 6
59		oveq1 6087	. . . . . . 7
60	59	breq1d 4290	. . . . . 6
61		1re 9373	. . . . . . . . . 10
62	19	adantr 462	. . . . . . . . . 10 $/\$
63		resubcl 9661	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 656	. . . . . . . . 9 $/\$
65	64	adantr 462	. . . . . . . 8 $/\$ $/\$
66	65	leidd 9894	. . . . . . 7 $/\$ $/\$
67	64	recnd 9400	. . . . . . . . 9 $/\$
68	67	adantr 462	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9392	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10607	. . . . . . . . . . . . 13
71	31, 70	syl 16	. . . . . . . . . . . 12
72	71	ad3antrrr 722	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12008	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 458	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6095	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2475	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10413	. . . . . . . . . . . . 13
78	31	ad2antrr 718	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 11856	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 656	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 13749	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12013	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10326	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 718	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrd 12909	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6096	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 718	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 10954	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10342	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10666	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 13909	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1216	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 10733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 13922	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 654	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2474	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6096	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 458	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 13900	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10584	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 11995	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 11945	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6090	. . . . . . . . . . . . . . . 16
110	104	nn0zd 10733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 11877	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2477	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2469	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6095	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9377	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2481	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2465	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 462	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9400	. . . . . . . . . . . . . . 15
121	120	adantr 462	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 718	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		simpr 458	. . . . . . . . . . . . . . . . 17 $/\$
125	124	ad2antrr 718	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126		rpvmasum2.g	. . . . . . . . . . . . . . . . . . 19 DChr
127		rpvmasum2.d	. . . . . . . . . . . . . . . . . . 19
128		dchrisum0f.x	. . . . . . . . . . . . . . . . . . . 20
129	128	ad3antrrr 722	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130		eqid 2433	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 22474	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 718	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 22484	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2439	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2634	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 718	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 12886	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9592	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6095	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2475	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2679	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6096	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4310	. . . . . 6 $/\$ $/\$
151	67	mul02d 9555	. . . . . . . 8 $/\$
152		peano2nn0 10608	. . . . . . . . . . . . 13
153	31, 152	syl 16	. . . . . . . . . . . 12
154	19, 153	reexpcld 12009	. . . . . . . . . . 11
155	154	adantr 462	. . . . . . . . . 10 $/\$
156	155	recnd 9400	. . . . . . . . . . 11 $/\$
157	156	abscld 12906	. . . . . . . . . 10 $/\$
158		1red 9389	. . . . . . . . . 10 $/\$
159	155	leabsd 12885	. . . . . . . . . 10 $/\$
160	153	adantr 462	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 12922	. . . . . . . . . . 11 $/\$
162	121	abscld 12906	. . . . . . . . . . . 12 $/\$
163	121	absge0d 12914	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 22486	. . . . . . . . . . . . 13
165	164	adantr 462	. . . . . . . . . . . 12 $/\$
166		exple1 11907	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1214	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4300	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9516	. . . . . . . . 9 $/\$
170		subge0 9840	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 656	. . . . . . . . 9 $/\$
172	169, 171	mpbird 232	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4300	. . . . . . 7 $/\$
174	173	adantr 462	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3812	. . . . 5 $/\$
176		0re 9374	. . . . . . . 8
177	61, 176	keepel 3845	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9661	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 656	. . . . . 6 $/\$
181	124	necomd 2685	. . . . . . . 8 $/\$
182	62	leabsd 12885	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9516	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9513	. . . . . . . 8 $/\$
185	181, 184	mpbird 232	. . . . . . 7 $/\$
186		posdif 9820	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 655	. . . . . . 7 $/\$
188	185, 187	mpbid 210	. . . . . 6 $/\$
189		lemuldiv 10199	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1215	. . . . 5 $/\$
191	175, 190	mpbid 210	. . . 4 $/\$
192	31	nn0zd 10733	. . . . . . . 8
193		fzval3 11589	. . . . . . . 8 ..^
194	192, 193	syl 16	. . . . . . 7 ..^
195	194	adantr 462	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13162	. . . . 5 $/\$ ..^
197		0nn0 10582	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2523	. . . . . . 7
200	199	adantr 462	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 13311	. . . . 5 $/\$ ..^
202	121	exp0d 11986	. . . . . . 7 $/\$
203	202	oveq1d 6095	. . . . . 6 $/\$
204	203	oveq1d 6095	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2469	. . . 4 $/\$
206	191, 205	breqtrrd 4306	. . 3 $/\$
207	56, 206	pm2.61dane 2679	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 22639	. . . 4
211	83, 210	syl 16	. . 3
212		fveq2 5679	. . . . 5
213	212	fveq2d 5683	. . . 4
214		eqid 2433	. . . . . 6
215	214	dvdsppwf1o 22411	. . . . 5 $/\$
216	15, 31, 215	syl2anc 654	. . . 4
217		oveq2 6088	. . . . . 6
218		ovex 6105	. . . . . 6
219	217, 214, 218	fvmpt3i 5766	. . . . 5
220	219	adantl 463	. . . 4 $/\$
221	6	adantr 462	. . . . . 6 $/\$
222		elrabi 3103	. . . . . . . 8
223	222	nnzd 10734	. . . . . . 7
224		ffvelrn 5829	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 474	. . . . . 6 $/\$
226	221, 225	ffvelrnd 5832	. . . . 5 $/\$
227	226	recnd 9400	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13184	. . 3
229		zsubrg 17710	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2433	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 16802	. . . . . . . . . . 11 SubRingℂ_fld SubMndmulGrpℂ_fld
232	229, 231	mp1i 12	. . . . . . . . . 10 $/\$ SubMndmulGrpℂ_fld
233	20	adantl 463	. . . . . . . . . 10 $/\$
234	17	adantr 462	. . . . . . . . . 10 $/\$
235		eqid 2433	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 17758	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2437	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2433	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 15642	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1211	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10326	. . . . . . . . . 10
242		cnfldexp 17693	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 474	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2467	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5683	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 17819	. . . . . . . . . . 11
247		crngrng 16591	. . . . . . . . . . 11
248	8, 246, 247	3syl 20	. . . . . . . . . 10
249	11	zrhrhm 17785	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2433	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2433	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 16746	. . . . . . . . . 10 ℤ_ring RingHom mulGrpℤ_ring MndHom mulGrp
253	248, 249, 252	3syl 20	. . . . . . . . 9 mulGrpℤ_ring MndHom mulGrp
254	253	adantr 462	. . . . . . . 8 $/\$ mulGrpℤ_ring MndHom mulGrp
255		zringbas 17731	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 16571	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2433	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 15639	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1211	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2467	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5683	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 22465	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3342	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 462	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 462	. . . . . 6 $/\$
266	251, 10	mgpbas 16571	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 15639	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1211	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 17693	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 474	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2469	. . . 4 $/\$
272	271	sumeq2dv 13164	. . 3
273	211, 228, 272	3eqtrd 2469	. 2
274	207, 273	breqtrrd 4306	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1362

wcel 1755

wne 2596

crab 2709

c0 3625

cif 3779 class class class wbr 4280

cmpt 4338

wf 5402

wfo 5404

wf1o 5405

cfv 5406 (class class class)co 6080

cfn 7298

cc 9268

cr 9269

cc0 9270

c1 9271

caddc 9273

cmul 9275

clt 9406

cle 9407

cmin 9583

cneg 9584

cdiv 9981

cn 10310

c2 10359

cn0 10567

cz 10634

cuz 10849

cq 10941

cfz 11424 ..^cfzo 11532

cexp 11849

chash 12087

csqr 12706

cabs 12707

csu 13147

cdivides 13518

cprime 13746

cpc 13886

cbs 14157 ↾_s cress 14158

c0g 14361 ._gcmg 15397 MndHom cmhm 15445 SubMndcsubmnd 15446 mulGrpcmgp 16565

crg 16577

ccrg 16578 Unitcui 16665 RingHom crh 16738 SubRingcsubrg 16785 ℂ_fldccnfld 17662 ℤ_ringzring 17725

RHomczrh 17773 ℤ/nℤczn 17776 DChrcdchr 22456

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-disj 4251 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-tpos 6734 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-omul 6913 df-er 7089 df-ec 7091 df-qs 7095 df-map 7204 df-pm 7205 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-acn 8100 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-5 10371 df-6 10372 df-7 10373 df-8 10374 df-9 10375 df-10 10376 df-n0 10568 df-z 10635 df-dec 10744 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-ioc 11293 df-ico 11294 df-icc 11295 df-fz 11425 df-fzo 11533 df-fl 11626 df-mod 11693 df-seq 11791 df-exp 11850 df-fac 12036 df-bc 12063 df-hash 12088 df-shft 12540 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-limsup 12933 df-clim 12950 df-rlim 12951 df-sum 13148 df-ef 13336 df-sin 13338 df-cos 13339 df-pi 13341 df-dvds 13519 df-gcd 13674 df-prm 13747 df-pc 13887 df-struct 14159 df-ndx 14160 df-slot 14161 df-base 14162 df-sets 14163 df-ress 14164 df-plusg 14234 df-mulr 14235 df-starv 14236 df-sca 14237 df-vsca 14238 df-ip 14239 df-tset 14240 df-ple 14241 df-ds 14243 df-unif 14244 df-hom 14245 df-cco 14246 df-rest 14344 df-topn 14345 df-0g 14363 df-gsum 14364 df-topgen 14365 df-pt 14366 df-prds 14369 df-xrs 14423 df-qtop 14428 df-imas 14429 df-divs 14430 df-xps 14431 df-mre 14507 df-mrc 14508 df-acs 14510 df-mnd 15398 df-mhm 15447 df-submnd 15448 df-grp 15525 df-minusg 15526 df-sbg 15527 df-mulg 15528 df-subg 15658 df-nsg 15659 df-eqg 15660 df-ghm 15725 df-cntz 15815 df-od 16012 df-cmn 16259 df-abl 16260 df-mgp 16566 df-rng 16580 df-cring 16581 df-ur 16582 df-oppr 16649 df-dvdsr 16667 df-unit 16668 df-invr 16698 df-dvr 16709 df-rnghom 16740 df-drng 16758 df-subrg 16787 df-lmod 16874 df-lss 16936 df-lsp 16975 df-sra 17175 df-rgmod 17176 df-lidl 17177 df-rsp 17178 df-2idl 17236 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-fbas 17658 df-fg 17659 df-cnfld 17663 df-zring 17726 df-zrh 17777 df-zn 17780 df-top 18345 df-bases 18347 df-topon 18348 df-topsp 18349 df-cld 18465 df-ntr 18466 df-cls 18467 df-nei 18544 df-lp 18582 df-perf 18583 df-cn 18673 df-cnp 18674 df-haus 18761 df-tx 18977 df-hmeo 19170 df-fil 19261 df-fm 19353 df-flim 19354 df-flf 19355 df-xms 19737 df-ms 19738 df-tms 19739 df-cncf 20296 df-limc 21183 df-dv 21184 df-log 21893 df-cxp 21894 df-dchr 22457

This theorem is referenced by: dchrisum0flblem2 22643 dchrisum0flb 22644

W3C validator