dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 23810

Description: Lemma for dchrisum0flb 23812. 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 9522	. . . . 5 $/\$ $/\$
2		0red 9508	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3889	. . . 4 $/\$
4		1red 9522	. . . 4 $/\$
5		fzfid 11986	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10769	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2382	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 18677	. . . . . . . . . 10
13		fof 5703	. . . . . . . . . 10
14	8, 12, 13	3syl 20	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 14223	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	14, 17	ffvelrnd 5934	. . . . . . . 8
19	6, 18	ffvelrnd 5934	. . . . . . 7
20		elfznn0 11693	. . . . . . 7
21		reexpcl 12086	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 475	. . . . . 6 $/\$
23	5, 22	fsumrecl 13558	. . . . 5
24	23	adantr 463	. . . 4 $/\$
25		breq1 4370	. . . . . 6
26		breq1 4370	. . . . . 6
27		1le1 10094	. . . . . 6
28		0le1 9993	. . . . . 6
29	25, 26, 27, 28	keephyp 3921	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 11035	. . . . . . . . . 10
33	31, 32	syl6eleq 2480	. . . . . . . . 9
34		fzn0 11621	. . . . . . . . 9
35	33, 34	sylibr 212	. . . . . . . 8
36		hashnncl 12339	. . . . . . . . 9
37	5, 36	syl 16	. . . . . . . 8
38	35, 37	mpbird 232	. . . . . . 7
39	38	adantr 463	. . . . . 6 $/\$
40	39	nnge1d 10495	. . . . 5 $/\$
41		simpr 459	. . . . . . . . 9 $/\$
42	41	oveq1d 6211	. . . . . . . 8 $/\$
43		elfzelz 11609	. . . . . . . . 9
44		1exp 12098	. . . . . . . . 9
45	43, 44	syl 16	. . . . . . . 8
46	42, 45	sylan9eq 2443	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13527	. . . . . 6 $/\$
48		fzfid 11986	. . . . . . 7 $/\$
49		ax-1cn 9461	. . . . . . 7
50		fsumconst 13607	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 660	. . . . . 6 $/\$
52	39	nncnd 10468	. . . . . . 7 $/\$
53	52	mulid1d 9524	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2427	. . . . 5 $/\$
55	40, 54	breqtrrd 4393	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9650	. . 3 $/\$
57		oveq1 6203	. . . . . . 7
58	57	breq1d 4377	. . . . . 6
59		oveq1 6203	. . . . . . 7
60	59	breq1d 4377	. . . . . 6
61		1re 9506	. . . . . . . . . 10
62	19	adantr 463	. . . . . . . . . 10 $/\$
63		resubcl 9796	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 661	. . . . . . . . 9 $/\$
65	64	adantr 463	. . . . . . . 8 $/\$ $/\$
66	65	leidd 10036	. . . . . . 7 $/\$ $/\$
67	64	recnd 9533	. . . . . . . . 9 $/\$
68	67	adantr 463	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9525	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10752	. . . . . . . . . . . . 13
71	31, 70	syl 16	. . . . . . . . . . . 12
72	71	ad3antrrr 727	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12228	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 459	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6211	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2433	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10556	. . . . . . . . . . . . 13
78	31	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 12076	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 661	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 14222	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12233	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10468	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrtd 13272	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 11114	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 464	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10485	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 464	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10813	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 14385	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1231	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 10882	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 14398	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2432	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6212	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 459	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 14376	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10729	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 12215	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 12166	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6206	. . . . . . . . . . . . . . . 16
110	104	nn0zd 10882	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 12098	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2435	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2427	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6211	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9510	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2439	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2423	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 463	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9533	. . . . . . . . . . . . . . 15
121	120	adantr 463	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9835	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		simpr 459	. . . . . . . . . . . . . . . . 17 $/\$
125	124	ad2antrr 723	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126		rpvmasum2.g	. . . . . . . . . . . . . . . . . . 19 DChr
127		rpvmasum2.d	. . . . . . . . . . . . . . . . . . 19
128		dchrisum0f.x	. . . . . . . . . . . . . . . . . . . 20
129	128	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130		eqid 2382	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 23642	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 23652	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2386	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2592	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 723	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 13249	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 375	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2425	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2425	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6211	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2433	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2700	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6212	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4397	. . . . . 6 $/\$ $/\$
151	67	mul02d 9689	. . . . . . . 8 $/\$
152		peano2nn0 10753	. . . . . . . . . . . . 13
153	31, 152	syl 16	. . . . . . . . . . . 12
154	19, 153	reexpcld 12229	. . . . . . . . . . 11
155	154	adantr 463	. . . . . . . . . 10 $/\$
156	155	recnd 9533	. . . . . . . . . . 11 $/\$
157	156	abscld 13269	. . . . . . . . . 10 $/\$
158		1red 9522	. . . . . . . . . 10 $/\$
159	155	leabsd 13248	. . . . . . . . . 10 $/\$
160	153	adantr 463	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 13285	. . . . . . . . . . 11 $/\$
162	121	abscld 13269	. . . . . . . . . . . 12 $/\$
163	121	absge0d 13277	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 23654	. . . . . . . . . . . . 13
165	164	adantr 463	. . . . . . . . . . . 12 $/\$
166		exple1 12128	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1229	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4387	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9650	. . . . . . . . 9 $/\$
170		subge0 9983	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 661	. . . . . . . . 9 $/\$
172	169, 171	mpbird 232	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4387	. . . . . . 7 $/\$
174	173	adantr 463	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3892	. . . . 5 $/\$
176		0re 9507	. . . . . . . 8
177	61, 176	keepel 3924	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9796	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 661	. . . . . 6 $/\$
181	124	necomd 2653	. . . . . . . 8 $/\$
182	62	leabsd 13248	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9650	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9647	. . . . . . . 8 $/\$
185	181, 184	mpbird 232	. . . . . . 7 $/\$
186		posdif 9963	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 660	. . . . . . 7 $/\$
188	185, 187	mpbid 210	. . . . . 6 $/\$
189		lemuldiv 10340	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1230	. . . . 5 $/\$
191	175, 190	mpbid 210	. . . 4 $/\$
192	31	nn0zd 10882	. . . . . . . 8
193		fzval3 11784	. . . . . . . 8 ..^
194	192, 193	syl 16	. . . . . . 7 ..^
195	194	adantr 463	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13525	. . . . 5 $/\$ ..^
197		0nn0 10727	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2480	. . . . . . 7
200	199	adantr 463	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 13679	. . . . 5 $/\$ ..^
202	121	exp0d 12206	. . . . . . 7 $/\$
203	202	oveq1d 6211	. . . . . 6 $/\$
204	203	oveq1d 6211	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2427	. . . 4 $/\$
206	191, 205	breqtrrd 4393	. . 3 $/\$
207	56, 206	pm2.61dane 2700	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 23807	. . . 4
211	83, 210	syl 16	. . 3
212		fveq2 5774	. . . . 5
213	212	fveq2d 5778	. . . 4
214		eqid 2382	. . . . . 6
215	214	dvdsppwf1o 23579	. . . . 5 $/\$
216	15, 31, 215	syl2anc 659	. . . 4
217		oveq2 6204	. . . . . 6
218		ovex 6224	. . . . . 6
219	217, 214, 218	fvmpt3i 5861	. . . . 5
220	219	adantl 464	. . . 4 $/\$
221	6	adantr 463	. . . . . 6 $/\$
222		elrabi 3179	. . . . . . . 8
223	222	nnzd 10883	. . . . . . 7
224		ffvelrn 5931	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 475	. . . . . 6 $/\$
226	221, 225	ffvelrnd 5934	. . . . 5 $/\$
227	226	recnd 9533	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13547	. . 3
229		zsubrg 18584	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2382	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 17555	. . . . . . . . . . 11 SubRingℂ_fld SubMndmulGrpℂ_fld
232	229, 231	mp1i 12	. . . . . . . . . 10 $/\$ SubMndmulGrpℂ_fld
233	20	adantl 464	. . . . . . . . . 10 $/\$
234	17	adantr 463	. . . . . . . . . 10 $/\$
235		eqid 2382	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 18622	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2395	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2382	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 16294	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1226	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10468	. . . . . . . . . 10
242		cnfldexp 18564	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 475	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2425	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5778	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 18674	. . . . . . . . . . 11
247		crngring 17322	. . . . . . . . . . 11
248	8, 246, 247	3syl 20	. . . . . . . . . 10
249	11	zrhrhm 18642	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2382	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2382	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 17484	. . . . . . . . . 10 ℤ_ring RingHom mulGrpℤ_ring MndHom mulGrp
253	248, 249, 252	3syl 20	. . . . . . . . 9 mulGrpℤ_ring MndHom mulGrp
254	253	adantr 463	. . . . . . . 8 $/\$ mulGrpℤ_ring MndHom mulGrp
255		zringbas 18607	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 17260	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2382	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 16291	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1226	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2425	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5778	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 23633	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3415	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 463	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 463	. . . . . 6 $/\$
266	251, 10	mgpbas 17260	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 16291	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1226	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 18564	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 475	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2427	. . . 4 $/\$
272	271	sumeq2dv 13527	. . 3
273	211, 228, 272	3eqtrd 2427	. 2
274	207, 273	breqtrrd 4393	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wceq 1399

wcel 1826

wne 2577

crab 2736

c0 3711

cif 3857 class class class wbr 4367

cmpt 4425

wf 5492

wfo 5494

wf1o 5495

cfv 5496 (class class class)co 6196

cfn 7435

cc 9401

cr 9402

cc0 9403

c1 9404

caddc 9406

cmul 9408

clt 9539

cle 9540

cmin 9718

cneg 9719

cdiv 10123

cn 10452

c2 10502

cn0 10712

cz 10781

cuz 11001

cq 11101

cfz 11593 ..^cfzo 11717

cexp 12069

chash 12307

csqrt 13068

cabs 13069

csu 13510

cdvds 13988

cprime 14219

cpc 14362

cbs 14634 ↾_s cress 14635

c0g 14847 MndHom cmhm 16081 SubMndcsubmnd 16082 ._gcmg 16173 mulGrpcmgp 17254

crg 17311

ccrg 17312 Unitcui 17401 RingHom crh 17474 SubRingcsubrg 17538 ℂ_fldccnfld 18533 ℤ_ringzring 18601

RHomczrh 18630 ℤ/nℤczn 18633 DChrcdchr 23624

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481 ax-addf 9482 ax-mulf 9483

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-iin 4246 df-disj 4339 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-of 6439 df-om 6600 df-1st 6699 df-2nd 6700 df-supp 6818 df-tpos 6873 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-omul 7053 df-er 7229 df-ec 7231 df-qs 7235 df-map 7340 df-pm 7341 df-ixp 7389 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-fsupp 7745 df-fi 7786 df-sup 7816 df-oi 7850 df-card 8233 df-acn 8236 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-5 10514 df-6 10515 df-7 10516 df-8 10517 df-9 10518 df-10 10519 df-n0 10713 df-z 10782 df-dec 10896 df-uz 11002 df-q 11102 df-rp 11140 df-xneg 11239 df-xadd 11240 df-xmul 11241 df-ioo 11454 df-ioc 11455 df-ico 11456 df-icc 11457 df-fz 11594 df-fzo 11718 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-fac 12256 df-bc 12283 df-hash 12308 df-shft 12902 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-limsup 13296 df-clim 13313 df-rlim 13314 df-sum 13511 df-ef 13805 df-sin 13807 df-cos 13808 df-pi 13810 df-dvds 13989 df-gcd 14147 df-prm 14220 df-pc 14363 df-struct 14636 df-ndx 14637 df-slot 14638 df-base 14639 df-sets 14640 df-ress 14641 df-plusg 14715 df-mulr 14716 df-starv 14717 df-sca 14718 df-vsca 14719 df-ip 14720 df-tset 14721 df-ple 14722 df-ds 14724 df-unif 14725 df-hom 14726 df-cco 14727 df-rest 14830 df-topn 14831 df-0g 14849 df-gsum 14850 df-topgen 14851 df-pt 14852 df-prds 14855 df-xrs 14909 df-qtop 14914 df-imas 14915 df-qus 14916 df-xps 14917 df-mre 14993 df-mrc 14994 df-acs 14996 df-mgm 15989 df-sgrp 16028 df-mnd 16038 df-mhm 16083 df-submnd 16084 df-grp 16174 df-minusg 16175 df-sbg 16176 df-mulg 16177 df-subg 16315 df-nsg 16316 df-eqg 16317 df-ghm 16382 df-cntz 16472 df-od 16670 df-cmn 16917 df-abl 16918 df-mgp 17255 df-ur 17267 df-ring 17313 df-cring 17314 df-oppr 17385 df-dvdsr 17403 df-unit 17404 df-invr 17434 df-dvr 17445 df-rnghom 17477 df-drng 17511 df-subrg 17540 df-lmod 17627 df-lss 17692 df-lsp 17731 df-sra 17931 df-rgmod 17932 df-lidl 17933 df-rsp 17934 df-2idl 17993 df-psmet 18524 df-xmet 18525 df-met 18526 df-bl 18527 df-mopn 18528 df-fbas 18529 df-fg 18530 df-cnfld 18534 df-zring 18602 df-zrh 18634 df-zn 18637 df-top 19484 df-bases 19486 df-topon 19487 df-topsp 19488 df-cld 19605 df-ntr 19606 df-cls 19607 df-nei 19685 df-lp 19723 df-perf 19724 df-cn 19814 df-cnp 19815 df-haus 19902 df-tx 20148 df-hmeo 20341 df-fil 20432 df-fm 20524 df-flim 20525 df-flf 20526 df-xms 20908 df-ms 20909 df-tms 20910 df-cncf 21467 df-limc 22355 df-dv 22356 df-log 23029 df-cxp 23030 df-dchr 23625

This theorem is referenced by: dchrisum0flblem2 23811 dchrisum0flb 23812

W3C validator