dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 22889

Description: Lemma for dchrisum0flb 22891. 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 9511	. . . . 5 $/\$ $/\$
2		0red 9497	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3928	. . . 4 $/\$
4		1red 9511	. . . 4 $/\$
5		fzfid 11911	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10746	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2454	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 18104	. . . . . . . . . 10
13		fof 5727	. . . . . . . . . 10
14	8, 12, 13	3syl 20	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 13884	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	14, 17	ffvelrnd 5952	. . . . . . . 8
19	6, 18	ffvelrnd 5952	. . . . . . 7
20		elfznn0 11597	. . . . . . 7
21		reexpcl 11998	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 477	. . . . . 6 $/\$
23	5, 22	fsumrecl 13328	. . . . 5
24	23	adantr 465	. . . 4 $/\$
25		breq1 4402	. . . . . 6
26		breq1 4402	. . . . . 6
27		1le1 10074	. . . . . 6
28		0le1 9973	. . . . . 6
29	25, 26, 27, 28	keephyp 3961	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 11005	. . . . . . . . . 10
33	31, 32	syl6eleq 2552	. . . . . . . . 9
34		fzn0 11580	. . . . . . . . 9
35	33, 34	sylibr 212	. . . . . . . 8
36		hashnncl 12250	. . . . . . . . 9
37	5, 36	syl 16	. . . . . . . 8
38	35, 37	mpbird 232	. . . . . . 7
39	38	adantr 465	. . . . . 6 $/\$
40	39	nnge1d 10474	. . . . 5 $/\$
41		simpr 461	. . . . . . . . 9 $/\$
42	41	oveq1d 6214	. . . . . . . 8 $/\$
43		elfzelz 11569	. . . . . . . . 9
44		1exp 12009	. . . . . . . . 9
45	43, 44	syl 16	. . . . . . . 8
46	42, 45	sylan9eq 2515	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13297	. . . . . 6 $/\$
48		fzfid 11911	. . . . . . 7 $/\$
49		ax-1cn 9450	. . . . . . 7
50		fsumconst 13374	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 662	. . . . . 6 $/\$
52	39	nncnd 10448	. . . . . . 7 $/\$
53	52	mulid1d 9513	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2499	. . . . 5 $/\$
55	40, 54	breqtrrd 4425	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9638	. . 3 $/\$
57		oveq1 6206	. . . . . . 7
58	57	breq1d 4409	. . . . . 6
59		oveq1 6206	. . . . . . 7
60	59	breq1d 4409	. . . . . 6
61		1re 9495	. . . . . . . . . 10
62	19	adantr 465	. . . . . . . . . 10 $/\$
63		resubcl 9783	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 663	. . . . . . . . 9 $/\$
65	64	adantr 465	. . . . . . . 8 $/\$ $/\$
66	65	leidd 10016	. . . . . . 7 $/\$ $/\$
67	64	recnd 9522	. . . . . . . . 9 $/\$
68	67	adantr 465	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9514	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10729	. . . . . . . . . . . . 13
71	31, 70	syl 16	. . . . . . . . . . . 12
72	71	ad3antrrr 729	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12140	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6214	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2505	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10535	. . . . . . . . . . . . 13
78	31	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 11988	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 13883	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12145	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10448	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrd 13042	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6215	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 11076	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10464	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10788	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 14043	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 10855	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 14056	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2504	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6215	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 14034	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10706	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 12127	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 12077	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6209	. . . . . . . . . . . . . . . 16
110	104	nn0zd 10855	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 12009	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2507	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2499	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6214	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9499	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2511	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2495	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9522	. . . . . . . . . . . . . . 15
121	120	adantr 465	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9820	. . . . . . . . . . . 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 2454	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 22721	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 484	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 22731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2458	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 13019	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2497	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9714	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2497	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6214	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2505	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2769	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6215	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4429	. . . . . 6 $/\$ $/\$
151	67	mul02d 9677	. . . . . . . 8 $/\$
152		peano2nn0 10730	. . . . . . . . . . . . 13
153	31, 152	syl 16	. . . . . . . . . . . 12
154	19, 153	reexpcld 12141	. . . . . . . . . . 11
155	154	adantr 465	. . . . . . . . . 10 $/\$
156	155	recnd 9522	. . . . . . . . . . 11 $/\$
157	156	abscld 13039	. . . . . . . . . 10 $/\$
158		1red 9511	. . . . . . . . . 10 $/\$
159	155	leabsd 13018	. . . . . . . . . 10 $/\$
160	153	adantr 465	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 13055	. . . . . . . . . . 11 $/\$
162	121	abscld 13039	. . . . . . . . . . . 12 $/\$
163	121	absge0d 13047	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 22733	. . . . . . . . . . . . 13
165	164	adantr 465	. . . . . . . . . . . 12 $/\$
166		exple1 12039	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1222	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4419	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9638	. . . . . . . . 9 $/\$
170		subge0 9962	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 663	. . . . . . . . 9 $/\$
172	169, 171	mpbird 232	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4419	. . . . . . 7 $/\$
174	173	adantr 465	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3931	. . . . 5 $/\$
176		0re 9496	. . . . . . . 8
177	61, 176	keepel 3964	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9783	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 663	. . . . . 6 $/\$
181	124	necomd 2722	. . . . . . . 8 $/\$
182	62	leabsd 13018	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9638	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9635	. . . . . . . 8 $/\$
185	181, 184	mpbird 232	. . . . . . 7 $/\$
186		posdif 9942	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 662	. . . . . . 7 $/\$
188	185, 187	mpbid 210	. . . . . 6 $/\$
189		lemuldiv 10321	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1223	. . . . 5 $/\$
191	175, 190	mpbid 210	. . . 4 $/\$
192	31	nn0zd 10855	. . . . . . . 8
193		fzval3 11721	. . . . . . . 8 ..^
194	192, 193	syl 16	. . . . . . 7 ..^
195	194	adantr 465	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13295	. . . . 5 $/\$ ..^
197		0nn0 10704	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2552	. . . . . . 7
200	199	adantr 465	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 13445	. . . . 5 $/\$ ..^
202	121	exp0d 12118	. . . . . . 7 $/\$
203	202	oveq1d 6214	. . . . . 6 $/\$
204	203	oveq1d 6214	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2499	. . . 4 $/\$
206	191, 205	breqtrrd 4425	. . 3 $/\$
207	56, 206	pm2.61dane 2769	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 22886	. . . 4
211	83, 210	syl 16	. . 3
212		fveq2 5798	. . . . 5
213	212	fveq2d 5802	. . . 4
214		eqid 2454	. . . . . 6
215	214	dvdsppwf1o 22658	. . . . 5 $/\$
216	15, 31, 215	syl2anc 661	. . . 4
217		oveq2 6207	. . . . . 6
218		ovex 6224	. . . . . 6
219	217, 214, 218	fvmpt3i 5886	. . . . 5
220	219	adantl 466	. . . 4 $/\$
221	6	adantr 465	. . . . . 6 $/\$
222		elrabi 3219	. . . . . . . 8
223	222	nnzd 10856	. . . . . . 7
224		ffvelrn 5949	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 477	. . . . . 6 $/\$
226	221, 225	ffvelrnd 5952	. . . . 5 $/\$
227	226	recnd 9522	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13317	. . 3
229		zsubrg 17990	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2454	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 17000	. . . . . . . . . . 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 2454	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 18040	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2467	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2454	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 15780	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1219	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10448	. . . . . . . . . 10
242		cnfldexp 17973	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 477	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2497	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5802	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 18101	. . . . . . . . . . 11
247		crngrng 16777	. . . . . . . . . . 11
248	8, 246, 247	3syl 20	. . . . . . . . . 10
249	11	zrhrhm 18067	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2454	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2454	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 16934	. . . . . . . . . 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 18013	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 16718	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2454	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 15777	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1219	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2497	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5802	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 22712	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3461	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 465	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 465	. . . . . 6 $/\$
266	251, 10	mgpbas 16718	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 15777	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1219	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 17973	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 477	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2499	. . . 4 $/\$
272	271	sumeq2dv 13297	. . 3
273	211, 228, 272	3eqtrd 2499	. 2
274	207, 273	breqtrrd 4425	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1370

wcel 1758

wne 2647

crab 2802

c0 3744

cif 3898 class class class wbr 4399

cmpt 4457

wf 5521

wfo 5523

wf1o 5524

cfv 5525 (class class class)co 6199

cfn 7419

cc 9390

cr 9391

cc0 9392

c1 9393

caddc 9395

cmul 9397

clt 9528

cle 9529

cmin 9705

cneg 9706

cdiv 10103

cn 10432

c2 10481

cn0 10689

cz 10756

cuz 10971

cq 11063

cfz 11553 ..^cfzo 11664

cexp 11981

chash 12219

csqr 12839

cabs 12840

csu 13280

cdivides 13652

cprime 13880

cpc 14020

cbs 14291 ↾_s cress 14292

c0g 14496 ._gcmg 15532 MndHom cmhm 15580 SubMndcsubmnd 15581 mulGrpcmgp 16712

crg 16767

ccrg 16768 Unitcui 16853 RingHom crh 16926 SubRingcsubrg 16983 ℂ_fldccnfld 17942 ℤ_ringzring 18007

RHomczrh 18055 ℤ/nℤczn 18058 DChrcdchr 22703

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-inf2 7957 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 ax-pre-sup 9470 ax-addf 9471 ax-mulf 9472

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-iin 4281 df-disj 4370 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-se 4787 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-of 6429 df-om 6586 df-1st 6686 df-2nd 6687 df-supp 6800 df-tpos 6854 df-recs 6941 df-rdg 6975 df-1o 7029 df-2o 7030 df-oadd 7033 df-omul 7034 df-er 7210 df-ec 7212 df-qs 7216 df-map 7325 df-pm 7326 df-ixp 7373 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-fsupp 7731 df-fi 7771 df-sup 7801 df-oi 7834 df-card 8219 df-acn 8222 df-cda 8447 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-div 10104 df-nn 10433 df-2 10490 df-3 10491 df-4 10492 df-5 10493 df-6 10494 df-7 10495 df-8 10496 df-9 10497 df-10 10498 df-n0 10690 df-z 10757 df-dec 10866 df-uz 10972 df-q 11064 df-rp 11102 df-xneg 11199 df-xadd 11200 df-xmul 11201 df-ioo 11414 df-ioc 11415 df-ico 11416 df-icc 11417 df-fz 11554 df-fzo 11665 df-fl 11758 df-mod 11825 df-seq 11923 df-exp 11982 df-fac 12168 df-bc 12195 df-hash 12220 df-shft 12673 df-cj 12705 df-re 12706 df-im 12707 df-sqr 12841 df-abs 12842 df-limsup 13066 df-clim 13083 df-rlim 13084 df-sum 13281 df-ef 13470 df-sin 13472 df-cos 13473 df-pi 13475 df-dvds 13653 df-gcd 13808 df-prm 13881 df-pc 14021 df-struct 14293 df-ndx 14294 df-slot 14295 df-base 14296 df-sets 14297 df-ress 14298 df-plusg 14369 df-mulr 14370 df-starv 14371 df-sca 14372 df-vsca 14373 df-ip 14374 df-tset 14375 df-ple 14376 df-ds 14378 df-unif 14379 df-hom 14380 df-cco 14381 df-rest 14479 df-topn 14480 df-0g 14498 df-gsum 14499 df-topgen 14500 df-pt 14501 df-prds 14504 df-xrs 14558 df-qtop 14563 df-imas 14564 df-divs 14565 df-xps 14566 df-mre 14642 df-mrc 14643 df-acs 14645 df-mnd 15533 df-mhm 15582 df-submnd 15583 df-grp 15663 df-minusg 15664 df-sbg 15665 df-mulg 15666 df-subg 15796 df-nsg 15797 df-eqg 15798 df-ghm 15863 df-cntz 15953 df-od 16152 df-cmn 16399 df-abl 16400 df-mgp 16713 df-ur 16725 df-rng 16769 df-cring 16770 df-oppr 16837 df-dvdsr 16855 df-unit 16856 df-invr 16886 df-dvr 16897 df-rnghom 16928 df-drng 16956 df-subrg 16985 df-lmod 17072 df-lss 17136 df-lsp 17175 df-sra 17375 df-rgmod 17376 df-lidl 17377 df-rsp 17378 df-2idl 17436 df-psmet 17933 df-xmet 17934 df-met 17935 df-bl 17936 df-mopn 17937 df-fbas 17938 df-fg 17939 df-cnfld 17943 df-zring 18008 df-zrh 18059 df-zn 18062 df-top 18634 df-bases 18636 df-topon 18637 df-topsp 18638 df-cld 18754 df-ntr 18755 df-cls 18756 df-nei 18833 df-lp 18871 df-perf 18872 df-cn 18962 df-cnp 18963 df-haus 19050 df-tx 19266 df-hmeo 19459 df-fil 19550 df-fm 19642 df-flim 19643 df-flf 19644 df-xms 20026 df-ms 20027 df-tms 20028 df-cncf 20585 df-limc 21473 df-dv 21474 df-log 22140 df-cxp 22141 df-dchr 22704

This theorem is referenced by: dchrisum0flblem2 22890 dchrisum0flb 22891

W3C validator