dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 22737

Description: Lemma for dchrisum0flb 22739. 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 9393	. . . . 5 $/\$ $/\$
2		0red 9379	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3816	. . . 4 $/\$
4		1red 9393	. . . 4 $/\$
5		fzfid 11787	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10628	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2438	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 17960	. . . . . . . . . 10
13		fof 5615	. . . . . . . . . 10
14	8, 12, 13	3syl 20	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 13759	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	14, 17	ffvelrnd 5839	. . . . . . . 8
19	6, 18	ffvelrnd 5839	. . . . . . 7
20		elfznn0 11473	. . . . . . 7
21		reexpcl 11874	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 477	. . . . . 6 $/\$
23	5, 22	fsumrecl 13203	. . . . 5
24	23	adantr 465	. . . 4 $/\$
25		breq1 4290	. . . . . 6
26		breq1 4290	. . . . . 6
27		1le1 9956	. . . . . 6
28		0le1 9855	. . . . . 6
29	25, 26, 27, 28	keephyp 3849	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 10887	. . . . . . . . . 10
33	31, 32	syl6eleq 2528	. . . . . . . . 9
34		fzn0 11456	. . . . . . . . 9
35	33, 34	sylibr 212	. . . . . . . 8
36		hashnncl 12126	. . . . . . . . 9
37	5, 36	syl 16	. . . . . . . 8
38	35, 37	mpbird 232	. . . . . . 7
39	38	adantr 465	. . . . . 6 $/\$
40	39	nnge1d 10356	. . . . 5 $/\$
41		simpr 461	. . . . . . . . 9 $/\$
42	41	oveq1d 6101	. . . . . . . 8 $/\$
43		elfzelz 11445	. . . . . . . . 9
44		1exp 11885	. . . . . . . . 9
45	43, 44	syl 16	. . . . . . . 8
46	42, 45	sylan9eq 2490	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13172	. . . . . 6 $/\$
48		fzfid 11787	. . . . . . 7 $/\$
49		ax-1cn 9332	. . . . . . 7
50		fsumconst 13249	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 662	. . . . . 6 $/\$
52	39	nncnd 10330	. . . . . . 7 $/\$
53	52	mulid1d 9395	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2474	. . . . 5 $/\$
55	40, 54	breqtrrd 4313	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9520	. . 3 $/\$
57		oveq1 6093	. . . . . . 7
58	57	breq1d 4297	. . . . . 6
59		oveq1 6093	. . . . . . 7
60	59	breq1d 4297	. . . . . 6
61		1re 9377	. . . . . . . . . 10
62	19	adantr 465	. . . . . . . . . 10 $/\$
63		resubcl 9665	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 663	. . . . . . . . 9 $/\$
65	64	adantr 465	. . . . . . . 8 $/\$ $/\$
66	65	leidd 9898	. . . . . . 7 $/\$ $/\$
67	64	recnd 9404	. . . . . . . . 9 $/\$
68	67	adantr 465	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9396	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10611	. . . . . . . . . . . . 13
71	31, 70	syl 16	. . . . . . . . . . . 12
72	71	ad3antrrr 729	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12016	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6101	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2480	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10417	. . . . . . . . . . . . 13
78	31	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 11864	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 13758	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12021	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10330	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrd 12917	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6102	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 10958	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10346	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10670	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 13918	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1223	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 10737	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 13931	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2479	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6102	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 13909	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10588	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 12003	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 11953	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6096	. . . . . . . . . . . . . . . 16
110	104	nn0zd 10737	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 11885	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2482	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2474	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6101	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9381	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2486	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2470	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9404	. . . . . . . . . . . . . . 15
121	120	adantr 465	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9702	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$
125	124	ad2antrr 725	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126		rpvmasum2.g	. . . . . . . . . . . . . . . . . . 19 DChr
127		rpvmasum2.d	. . . . . . . . . . . . . . . . . . 19
128		dchrisum0f.x	. . . . . . . . . . . . . . . . . . . 20
129	128	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130		eqid 2438	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 22569	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 484	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 22579	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2444	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2639	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 12894	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9596	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2472	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6101	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2480	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2684	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6102	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4317	. . . . . 6 $/\$ $/\$
151	67	mul02d 9559	. . . . . . . 8 $/\$
152		peano2nn0 10612	. . . . . . . . . . . . 13
153	31, 152	syl 16	. . . . . . . . . . . 12
154	19, 153	reexpcld 12017	. . . . . . . . . . 11
155	154	adantr 465	. . . . . . . . . 10 $/\$
156	155	recnd 9404	. . . . . . . . . . 11 $/\$
157	156	abscld 12914	. . . . . . . . . 10 $/\$
158		1red 9393	. . . . . . . . . 10 $/\$
159	155	leabsd 12893	. . . . . . . . . 10 $/\$
160	153	adantr 465	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 12930	. . . . . . . . . . 11 $/\$
162	121	abscld 12914	. . . . . . . . . . . 12 $/\$
163	121	absge0d 12922	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 22581	. . . . . . . . . . . . 13
165	164	adantr 465	. . . . . . . . . . . 12 $/\$
166		exple1 11915	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1221	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4307	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9520	. . . . . . . . 9 $/\$
170		subge0 9844	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 663	. . . . . . . . 9 $/\$
172	169, 171	mpbird 232	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4307	. . . . . . 7 $/\$
174	173	adantr 465	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3819	. . . . 5 $/\$
176		0re 9378	. . . . . . . 8
177	61, 176	keepel 3852	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9665	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 663	. . . . . 6 $/\$
181	124	necomd 2690	. . . . . . . 8 $/\$
182	62	leabsd 12893	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9520	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9517	. . . . . . . 8 $/\$
185	181, 184	mpbird 232	. . . . . . 7 $/\$
186		posdif 9824	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 662	. . . . . . 7 $/\$
188	185, 187	mpbid 210	. . . . . 6 $/\$
189		lemuldiv 10203	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1222	. . . . 5 $/\$
191	175, 190	mpbid 210	. . . 4 $/\$
192	31	nn0zd 10737	. . . . . . . 8
193		fzval3 11597	. . . . . . . 8 ..^
194	192, 193	syl 16	. . . . . . 7 ..^
195	194	adantr 465	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13170	. . . . 5 $/\$ ..^
197		0nn0 10586	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2528	. . . . . . 7
200	199	adantr 465	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 13320	. . . . 5 $/\$ ..^
202	121	exp0d 11994	. . . . . . 7 $/\$
203	202	oveq1d 6101	. . . . . 6 $/\$
204	203	oveq1d 6101	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2474	. . . 4 $/\$
206	191, 205	breqtrrd 4313	. . 3 $/\$
207	56, 206	pm2.61dane 2684	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 22734	. . . 4
211	83, 210	syl 16	. . 3
212		fveq2 5686	. . . . 5
213	212	fveq2d 5690	. . . 4
214		eqid 2438	. . . . . 6
215	214	dvdsppwf1o 22506	. . . . 5 $/\$
216	15, 31, 215	syl2anc 661	. . . 4
217		oveq2 6094	. . . . . 6
218		ovex 6111	. . . . . 6
219	217, 214, 218	fvmpt3i 5773	. . . . 5
220	219	adantl 466	. . . 4 $/\$
221	6	adantr 465	. . . . . 6 $/\$
222		elrabi 3109	. . . . . . . 8
223	222	nnzd 10738	. . . . . . 7
224		ffvelrn 5836	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 477	. . . . . 6 $/\$
226	221, 225	ffvelrnd 5839	. . . . 5 $/\$
227	226	recnd 9404	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13192	. . 3
229		zsubrg 17846	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2438	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 16858	. . . . . . . . . . 11 SubRingℂ_fld SubMndmulGrpℂ_fld
232	229, 231	mp1i 12	. . . . . . . . . 10 $/\$ SubMndmulGrpℂ_fld
233	20	adantl 466	. . . . . . . . . 10 $/\$
234	17	adantr 465	. . . . . . . . . 10 $/\$
235		eqid 2438	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 17896	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2442	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2438	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 15653	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1218	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10330	. . . . . . . . . 10
242		cnfldexp 17829	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 477	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2472	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5690	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 17957	. . . . . . . . . . 11
247		crngrng 16645	. . . . . . . . . . 11
248	8, 246, 247	3syl 20	. . . . . . . . . 10
249	11	zrhrhm 17923	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2438	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2438	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 16802	. . . . . . . . . 10 ℤ_ring RingHom mulGrpℤ_ring MndHom mulGrp
253	248, 249, 252	3syl 20	. . . . . . . . 9 mulGrpℤ_ring MndHom mulGrp
254	253	adantr 465	. . . . . . . 8 $/\$ mulGrpℤ_ring MndHom mulGrp
255		zringbas 17869	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 16587	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2438	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 15650	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1218	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2472	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5690	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 22560	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3349	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 465	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 465	. . . . . 6 $/\$
266	251, 10	mgpbas 16587	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 15650	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1218	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 17829	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 477	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2474	. . . 4 $/\$
272	271	sumeq2dv 13172	. . 3
273	211, 228, 272	3eqtrd 2474	. 2
274	207, 273	breqtrrd 4313	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wne 2601

crab 2714

c0 3632

cif 3786 class class class wbr 4287

cmpt 4345

wf 5409

wfo 5411

wf1o 5412

cfv 5413 (class class class)co 6086

cfn 7302

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

clt 9410

cle 9411

cmin 9587

cneg 9588

cdiv 9985

cn 10314

c2 10363

cn0 10571

cz 10638

cuz 10853

cq 10945

cfz 11429 ..^cfzo 11540

cexp 11857

chash 12095

csqr 12714

cabs 12715

csu 13155

cdivides 13527

cprime 13755

cpc 13895

cbs 14166 ↾_s cress 14167

c0g 14370 ._gcmg 15406 MndHom cmhm 15454 SubMndcsubmnd 15455 mulGrpcmgp 16581

crg 16635

ccrg 16636 Unitcui 16721 RingHom crh 16794 SubRingcsubrg 16841 ℂ_fldccnfld 17798 ℤ_ringzring 17863

RHomczrh 17911 ℤ/nℤczn 17914 DChrcdchr 22551

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-disj 4258 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 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-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-tpos 6740 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-omul 6917 df-er 7093 df-ec 7095 df-qs 7099 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-acn 8104 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-fac 12044 df-bc 12071 df-hash 12096 df-shft 12548 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-sum 13156 df-ef 13345 df-sin 13347 df-cos 13348 df-pi 13350 df-dvds 13528 df-gcd 13683 df-prm 13756 df-pc 13896 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-divs 14439 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-mhm 15456 df-submnd 15457 df-grp 15536 df-minusg 15537 df-sbg 15538 df-mulg 15539 df-subg 15669 df-nsg 15670 df-eqg 15671 df-ghm 15736 df-cntz 15826 df-od 16023 df-cmn 16270 df-abl 16271 df-mgp 16582 df-ur 16594 df-rng 16637 df-cring 16638 df-oppr 16705 df-dvdsr 16723 df-unit 16724 df-invr 16754 df-dvr 16765 df-rnghom 16796 df-drng 16814 df-subrg 16843 df-lmod 16930 df-lss 16994 df-lsp 17033 df-sra 17233 df-rgmod 17234 df-lidl 17235 df-rsp 17236 df-2idl 17294 df-psmet 17789 df-xmet 17790 df-met 17791 df-bl 17792 df-mopn 17793 df-fbas 17794 df-fg 17795 df-cnfld 17799 df-zring 17864 df-zrh 17915 df-zn 17918 df-top 18483 df-bases 18485 df-topon 18486 df-topsp 18487 df-cld 18603 df-ntr 18604 df-cls 18605 df-nei 18682 df-lp 18720 df-perf 18721 df-cn 18811 df-cnp 18812 df-haus 18899 df-tx 19115 df-hmeo 19308 df-fil 19399 df-fm 19491 df-flim 19492 df-flf 19493 df-xms 19875 df-ms 19876 df-tms 19877 df-cncf 20434 df-limc 21321 df-dv 21322 df-log 21988 df-cxp 21989 df-dchr 22552

This theorem is referenced by: dchrisum0flblem2 22738 dchrisum0flb 22739

W3C validator