dchrisum0flblem1 - Metamath Proof Explorer

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

Theorem dchrisum0flblem1 23449

Description: Lemma for dchrisum0flb 23451. 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 9611	. . . . 5 $/\$ $/\$
2		0red 9597	. . . . 5 $/\$ $/\$
3	1, 2	ifclda 3971	. . . 4 $/\$
4		1red 9611	. . . 4 $/\$
5		fzfid 12051	. . . . . 6
6		dchrisum0flb.r	. . . . . . . 8
7		rpvmasum.a	. . . . . . . . . . 11
8	7	nnnn0d 10852	. . . . . . . . . 10
9		rpvmasum.z	. . . . . . . . . . 11 ℤ/nℤ
10		eqid 2467	. . . . . . . . . . 11
11		rpvmasum.l	. . . . . . . . . . 11 RHom
12	9, 10, 11	znzrhfo 18381	. . . . . . . . . 10
13		fof 5795	. . . . . . . . . 10
14	8, 12, 13	3syl 20	. . . . . . . . 9
15		dchrisum0flblem1.1	. . . . . . . . . 10
16		prmz 14080	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	14, 17	ffvelrnd 6022	. . . . . . . 8
19	6, 18	ffvelrnd 6022	. . . . . . 7
20		elfznn0 11770	. . . . . . 7
21		reexpcl 12151	. . . . . . 7 $/\$
22	19, 20, 21	syl2an 477	. . . . . 6 $/\$
23	5, 22	fsumrecl 13519	. . . . 5
24	23	adantr 465	. . . 4 $/\$
25		breq1 4450	. . . . . 6
26		breq1 4450	. . . . . 6
27		1le1 10177	. . . . . 6
28		0le1 10076	. . . . . 6
29	25, 26, 27, 28	keephyp 4004	. . . . 5
30	29	a1i 11	. . . 4 $/\$
31		dchrisum0flblem1.2	. . . . . . . . . 10
32		nn0uz 11116	. . . . . . . . . 10
33	31, 32	syl6eleq 2565	. . . . . . . . 9
34		fzn0 11700	. . . . . . . . 9
35	33, 34	sylibr 212	. . . . . . . 8
36		hashnncl 12404	. . . . . . . . 9
37	5, 36	syl 16	. . . . . . . 8
38	35, 37	mpbird 232	. . . . . . 7
39	38	adantr 465	. . . . . 6 $/\$
40	39	nnge1d 10578	. . . . 5 $/\$
41		simpr 461	. . . . . . . . 9 $/\$
42	41	oveq1d 6299	. . . . . . . 8 $/\$
43		elfzelz 11688	. . . . . . . . 9
44		1exp 12163	. . . . . . . . 9
45	43, 44	syl 16	. . . . . . . 8
46	42, 45	sylan9eq 2528	. . . . . . 7 $/\$ $/\$
47	46	sumeq2dv 13488	. . . . . 6 $/\$
48		fzfid 12051	. . . . . . 7 $/\$
49		ax-1cn 9550	. . . . . . 7
50		fsumconst 13568	. . . . . . 7 $/\$
51	48, 49, 50	sylancl 662	. . . . . 6 $/\$
52	39	nncnd 10552	. . . . . . 7 $/\$
53	52	mulid1d 9613	. . . . . 6 $/\$
54	47, 51, 53	3eqtrd 2512	. . . . 5 $/\$
55	40, 54	breqtrrd 4473	. . . 4 $/\$
56	3, 4, 24, 30, 55	letrd 9738	. . 3 $/\$
57		oveq1 6291	. . . . . . 7
58	57	breq1d 4457	. . . . . 6
59		oveq1 6291	. . . . . . 7
60	59	breq1d 4457	. . . . . 6
61		1re 9595	. . . . . . . . . 10
62	19	adantr 465	. . . . . . . . . 10 $/\$
63		resubcl 9883	. . . . . . . . . 10 $/\$
64	61, 62, 63	sylancr 663	. . . . . . . . 9 $/\$
65	64	adantr 465	. . . . . . . 8 $/\$ $/\$
66	65	leidd 10119	. . . . . . 7 $/\$ $/\$
67	64	recnd 9622	. . . . . . . . 9 $/\$
68	67	adantr 465	. . . . . . . 8 $/\$ $/\$
69	68	mulid2d 9614	. . . . . . 7 $/\$ $/\$
70		nn0p1nn 10835	. . . . . . . . . . . . 13
71	31, 70	syl 16	. . . . . . . . . . . 12
72	71	ad3antrrr 729	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	72	0expd 12294	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	74	oveq1d 6299	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	73, 75, 74	3eqtr4d 2518	. . . . . . . . 9 $/\$ $/\$ $/\$
77		neg1cn 10639	. . . . . . . . . . . . 13
78	31	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
79		expp1 12141	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$
81		prmnn 14079	. . . . . . . . . . . . . . . . . . . . . . 23
82	15, 81	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
83	82, 31	nnexpcld 12299	. . . . . . . . . . . . . . . . . . . . 21
84	83	nncnd 10552	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
86	85	sqsqrtd 13233	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87	86	oveq2d 6300	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
88	15	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
89		nnq 11195	. . . . . . . . . . . . . . . . . . 19
90	89	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91		nnne0 10568	. . . . . . . . . . . . . . . . . . 19
92	91	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
93		2z 10896	. . . . . . . . . . . . . . . . . . 19
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		pcexp 14242	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
96	88, 90, 92, 94, 95	syl121anc 1233	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
97	78	nn0zd 10964	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
98		pcid 14255	. . . . . . . . . . . . . . . . . 18 $/\$
99	88, 97, 98	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	87, 96, 99	3eqtr3rd 2517	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	oveq2d 6300	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	77	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
103		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	88, 103	pccld 14233	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105		2nn0 10812	. . . . . . . . . . . . . . . . 17
106	105	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	102, 104, 106	expmuld 12281	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		neg1sqe1 12231	. . . . . . . . . . . . . . . . 17
109	108	oveq1i 6294	. . . . . . . . . . . . . . . 16
110	104	nn0zd 10964	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		1exp 12163	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113	109, 112	syl5eq 2520	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	101, 107, 113	3eqtrd 2512	. . . . . . . . . . . . . 14 $/\$ $/\$
115	114	oveq1d 6299	. . . . . . . . . . . . 13 $/\$ $/\$
116	77	mulid2i 9599	. . . . . . . . . . . . 13
117	115, 116	syl6eq 2524	. . . . . . . . . . . 12 $/\$ $/\$
118	80, 117	eqtrd 2508	. . . . . . . . . . 11 $/\$ $/\$
119	118	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	19	recnd 9622	. . . . . . . . . . . . . . 15
121	120	adantr 465	. . . . . . . . . . . . . 14 $/\$
122	121	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	122	negnegd 9921	. . . . . . . . . . . 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 2467	. . . . . . . . . . . . . . . . . . 19 Unit Unit
131	126, 9, 127, 10, 130, 128, 18	dchrn0 23281	. . . . . . . . . . . . . . . . . . . . 21 Unit
132	131	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Unit
133	132	biimpa 484	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Unit
134	126, 127, 129, 9, 130, 133	dchrabs 23291	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		eqeq1 2471	. . . . . . . . . . . . . . . . . 18
136	134, 135	syl5ibcom 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
137	136	necon3ad 2677	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
138	125, 137	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	62	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
140	139	absord 13210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
141	140	ord 377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
142	138, 141	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	142, 134	eqtr3d 2510	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
144	143	negeqd 9814	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	123, 144	eqtr3d 2510	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145	oveq1d 6299	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	119, 146, 145	3eqtr4d 2518	. . . . . . . . 9 $/\$ $/\$ $/\$
148	76, 147	pm2.61dane 2785	. . . . . . . 8 $/\$ $/\$
149	148	oveq2d 6300	. . . . . . 7 $/\$ $/\$
150	66, 69, 149	3brtr4d 4477	. . . . . 6 $/\$ $/\$
151	67	mul02d 9777	. . . . . . . 8 $/\$
152		peano2nn0 10836	. . . . . . . . . . . . 13
153	31, 152	syl 16	. . . . . . . . . . . 12
154	19, 153	reexpcld 12295	. . . . . . . . . . 11
155	154	adantr 465	. . . . . . . . . 10 $/\$
156	155	recnd 9622	. . . . . . . . . . 11 $/\$
157	156	abscld 13230	. . . . . . . . . 10 $/\$
158		1red 9611	. . . . . . . . . 10 $/\$
159	155	leabsd 13209	. . . . . . . . . 10 $/\$
160	153	adantr 465	. . . . . . . . . . . 12 $/\$
161	121, 160	absexpd 13246	. . . . . . . . . . 11 $/\$
162	121	abscld 13230	. . . . . . . . . . . 12 $/\$
163	121	absge0d 13238	. . . . . . . . . . . 12 $/\$
164	126, 127, 9, 10, 128, 18	dchrabs2 23293	. . . . . . . . . . . . 13
165	164	adantr 465	. . . . . . . . . . . 12 $/\$
166		exple1 12193	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
167	162, 163, 165, 160, 166	syl31anc 1231	. . . . . . . . . . 11 $/\$
168	161, 167	eqbrtrd 4467	. . . . . . . . . 10 $/\$
169	155, 157, 158, 159, 168	letrd 9738	. . . . . . . . 9 $/\$
170		subge0 10065	. . . . . . . . . 10 $/\$
171	61, 155, 170	sylancr 663	. . . . . . . . 9 $/\$
172	169, 171	mpbird 232	. . . . . . . 8 $/\$
173	151, 172	eqbrtrd 4467	. . . . . . 7 $/\$
174	173	adantr 465	. . . . . 6 $/\$ $/\$
175	58, 60, 150, 174	ifbothda 3974	. . . . 5 $/\$
176		0re 9596	. . . . . . . 8
177	61, 176	keepel 4007	. . . . . . 7
178	177	a1i 11	. . . . . 6 $/\$
179		resubcl 9883	. . . . . . 7 $/\$
180	61, 155, 179	sylancr 663	. . . . . 6 $/\$
181	124	necomd 2738	. . . . . . . 8 $/\$
182	62	leabsd 13209	. . . . . . . . . 10 $/\$
183	62, 162, 158, 182, 165	letrd 9738	. . . . . . . . 9 $/\$
184	62, 158, 183	leltned 9735	. . . . . . . 8 $/\$
185	181, 184	mpbird 232	. . . . . . 7 $/\$
186		posdif 10045	. . . . . . . 8 $/\$
187	62, 61, 186	sylancl 662	. . . . . . 7 $/\$
188	185, 187	mpbid 210	. . . . . 6 $/\$
189		lemuldiv 10424	. . . . . 6 $/\$ $/\$ $/\$
190	178, 180, 64, 188, 189	syl112anc 1232	. . . . 5 $/\$
191	175, 190	mpbid 210	. . . 4 $/\$
192	31	nn0zd 10964	. . . . . . . 8
193		fzval3 11853	. . . . . . . 8 ..^
194	192, 193	syl 16	. . . . . . 7 ..^
195	194	adantr 465	. . . . . 6 $/\$ ..^
196	195	sumeq1d 13486	. . . . 5 $/\$ ..^
197		0nn0 10810	. . . . . . 7
198	197	a1i 11	. . . . . 6 $/\$
199	153, 32	syl6eleq 2565	. . . . . . 7
200	199	adantr 465	. . . . . 6 $/\$
201	121, 124, 198, 200	geoserg 13640	. . . . 5 $/\$ ..^
202	121	exp0d 12272	. . . . . . 7 $/\$
203	202	oveq1d 6299	. . . . . 6 $/\$
204	203	oveq1d 6299	. . . . 5 $/\$
205	196, 201, 204	3eqtrd 2512	. . . 4 $/\$
206	191, 205	breqtrrd 4473	. . 3 $/\$
207	56, 206	pm2.61dane 2785	. 2
208		rpvmasum2.1	. . . . 5
209		dchrisum0f.f	. . . . 5
210	9, 11, 7, 126, 127, 208, 209	dchrisum0fval 23446	. . . 4
211	83, 210	syl 16	. . 3
212		fveq2 5866	. . . . 5
213	212	fveq2d 5870	. . . 4
214		eqid 2467	. . . . . 6
215	214	dvdsppwf1o 23218	. . . . 5 $/\$
216	15, 31, 215	syl2anc 661	. . . 4
217		oveq2 6292	. . . . . 6
218		ovex 6309	. . . . . 6
219	217, 214, 218	fvmpt3i 5954	. . . . 5
220	219	adantl 466	. . . 4 $/\$
221	6	adantr 465	. . . . . 6 $/\$
222		elrabi 3258	. . . . . . . 8
223	222	nnzd 10965	. . . . . . 7
224		ffvelrn 6019	. . . . . . 7 $/\$
225	14, 223, 224	syl2an 477	. . . . . 6 $/\$
226	221, 225	ffvelrnd 6022	. . . . 5 $/\$
227	226	recnd 9622	. . . 4 $/\$
228	213, 5, 216, 220, 227	fsumf1o 13508	. . 3
229		zsubrg 18267	. . . . . . . . . . 11 SubRingℂ_fld
230		eqid 2467	. . . . . . . . . . . 12 mulGrpℂ_fld mulGrpℂ_fld
231	230	subrgsubm 17242	. . . . . . . . . . 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 2467	. . . . . . . . . . 11 ._gmulGrpℂ_fld ._gmulGrpℂ_fld
236		zringmpg 18317	. . . . . . . . . . . 12 mulGrpℂ_fld ↾_s mulGrpℤ_ring
237	236	eqcomi 2480	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℂ_fld ↾_s
238		eqid 2467	. . . . . . . . . . 11 ._gmulGrpℤ_ring ._gmulGrpℤ_ring
239	235, 237, 238	submmulg 15987	. . . . . . . . . 10 SubMndmulGrpℂ_fld $/\$ $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
240	232, 233, 234, 239	syl3anc 1228	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld ._gmulGrpℤ_ring
241	82	nncnd 10552	. . . . . . . . . 10
242		cnfldexp 18250	. . . . . . . . . 10 $/\$ ._gmulGrpℂ_fld
243	241, 20, 242	syl2an 477	. . . . . . . . 9 $/\$ ._gmulGrpℂ_fld
244	240, 243	eqtr3d 2510	. . . . . . . 8 $/\$ ._gmulGrpℤ_ring
245	244	fveq2d 5870	. . . . . . 7 $/\$ ._gmulGrpℤ_ring
246	9	zncrng 18378	. . . . . . . . . . 11
247		crngrng 17010	. . . . . . . . . . 11
248	8, 246, 247	3syl 20	. . . . . . . . . 10
249	11	zrhrhm 18344	. . . . . . . . . 10 ℤ_ring RingHom
250		eqid 2467	. . . . . . . . . . 11 mulGrpℤ_ring mulGrpℤ_ring
251		eqid 2467	. . . . . . . . . . 11 mulGrp mulGrp
252	250, 251	rhmmhm 17172	. . . . . . . . . 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 18290	. . . . . . . . . 10 ℤ_ring
256	250, 255	mgpbas 16949	. . . . . . . . 9 mulGrpℤ_ring
257		eqid 2467	. . . . . . . . 9 ._gmulGrp ._gmulGrp
258	256, 238, 257	mhmmulg 15984	. . . . . . . 8 mulGrpℤ_ring MndHom mulGrp $/\$ $/\$ ._gmulGrpℤ_ring ._gmulGrp
259	254, 233, 234, 258	syl3anc 1228	. . . . . . 7 $/\$ ._gmulGrpℤ_ring ._gmulGrp
260	245, 259	eqtr3d 2510	. . . . . 6 $/\$ ._gmulGrp
261	260	fveq2d 5870	. . . . 5 $/\$ ._gmulGrp
262	126, 9, 127	dchrmhm 23272	. . . . . . . 8 mulGrp MndHom mulGrpℂ_fld
263	262, 128	sseldi 3502	. . . . . . 7 mulGrp MndHom mulGrpℂ_fld
264	263	adantr 465	. . . . . 6 $/\$ mulGrp MndHom mulGrpℂ_fld
265	18	adantr 465	. . . . . 6 $/\$
266	251, 10	mgpbas 16949	. . . . . . 7 mulGrp
267	266, 257, 235	mhmmulg 15984	. . . . . 6 mulGrp MndHom mulGrpℂ_fld $/\$ $/\$ ._gmulGrp ._gmulGrpℂ_fld
268	264, 233, 265, 267	syl3anc 1228	. . . . 5 $/\$ ._gmulGrp ._gmulGrpℂ_fld
269		cnfldexp 18250	. . . . . 6 $/\$ ._gmulGrpℂ_fld
270	120, 20, 269	syl2an 477	. . . . 5 $/\$ ._gmulGrpℂ_fld
271	261, 268, 270	3eqtrd 2512	. . . 4 $/\$
272	271	sumeq2dv 13488	. . 3
273	211, 228, 272	3eqtrd 2512	. 2
274	207, 273	breqtrrd 4473	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662

crab 2818

c0 3785

cif 3939 class class class wbr 4447

cmpt 4505

wf 5584

wfo 5586

wf1o 5587

cfv 5588 (class class class)co 6284

cfn 7516

cc 9490

cr 9491

cc0 9492

c1 9493

caddc 9495

cmul 9497

clt 9628

cle 9629

cmin 9805

cneg 9806

cdiv 10206

cn 10536

c2 10585

cn0 10795

cz 10864

cuz 11082

cq 11182

cfz 11672 ..^cfzo 11792

cexp 12134

chash 12373

csqrt 13029

cabs 13030

csu 13471

cdivides 13847

cprime 14076

cpc 14219

cbs 14490 ↾_s cress 14491

c0g 14695 ._gcmg 15731 MndHom cmhm 15784 SubMndcsubmnd 15785 mulGrpcmgp 16943

crg 17000

ccrg 17001 Unitcui 17089 RingHom crh 17162 SubRingcsubrg 17225 ℂ_fldccnfld 18219 ℤ_ringzring 18284

RHomczrh 18332 ℤ/nℤczn 18335 DChrcdchr 23263

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570 ax-addf 9571 ax-mulf 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-of 6524 df-om 6685 df-1st 6784 df-2nd 6785 df-supp 6902 df-tpos 6955 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-omul 7135 df-er 7311 df-ec 7313 df-qs 7317 df-map 7422 df-pm 7423 df-ixp 7470 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fsupp 7830 df-fi 7871 df-sup 7901 df-oi 7935 df-card 8320 df-acn 8323 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-4 10596 df-5 10597 df-6 10598 df-7 10599 df-8 10600 df-9 10601 df-10 10602 df-n0 10796 df-z 10865 df-dec 10977 df-uz 11083 df-q 11183 df-rp 11221 df-xneg 11318 df-xadd 11319 df-xmul 11320 df-ioo 11533 df-ioc 11534 df-ico 11535 df-icc 11536 df-fz 11673 df-fzo 11793 df-fl 11897 df-mod 11965 df-seq 12076 df-exp 12135 df-fac 12322 df-bc 12349 df-hash 12374 df-shft 12863 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-limsup 13257 df-clim 13274 df-rlim 13275 df-sum 13472 df-ef 13665 df-sin 13667 df-cos 13668 df-pi 13670 df-dvds 13848 df-gcd 14004 df-prm 14077 df-pc 14220 df-struct 14492 df-ndx 14493 df-slot 14494 df-base 14495 df-sets 14496 df-ress 14497 df-plusg 14568 df-mulr 14569 df-starv 14570 df-sca 14571 df-vsca 14572 df-ip 14573 df-tset 14574 df-ple 14575 df-ds 14577 df-unif 14578 df-hom 14579 df-cco 14580 df-rest 14678 df-topn 14679 df-0g 14697 df-gsum 14698 df-topgen 14699 df-pt 14700 df-prds 14703 df-xrs 14757 df-qtop 14762 df-imas 14763 df-divs 14764 df-xps 14765 df-mre 14841 df-mrc 14842 df-acs 14844 df-mnd 15732 df-mhm 15786 df-submnd 15787 df-grp 15867 df-minusg 15868 df-sbg 15869 df-mulg 15870 df-subg 16003 df-nsg 16004 df-eqg 16005 df-ghm 16070 df-cntz 16160 df-od 16359 df-cmn 16606 df-abl 16607 df-mgp 16944 df-ur 16956 df-rng 17002 df-cring 17003 df-oppr 17073 df-dvdsr 17091 df-unit 17092 df-invr 17122 df-dvr 17133 df-rnghom 17165 df-drng 17198 df-subrg 17227 df-lmod 17314 df-lss 17379 df-lsp 17418 df-sra 17618 df-rgmod 17619 df-lidl 17620 df-rsp 17621 df-2idl 17679 df-psmet 18210 df-xmet 18211 df-met 18212 df-bl 18213 df-mopn 18214 df-fbas 18215 df-fg 18216 df-cnfld 18220 df-zring 18285 df-zrh 18336 df-zn 18339 df-top 19194 df-bases 19196 df-topon 19197 df-topsp 19198 df-cld 19314 df-ntr 19315 df-cls 19316 df-nei 19393 df-lp 19431 df-perf 19432 df-cn 19522 df-cnp 19523 df-haus 19610 df-tx 19826 df-hmeo 20019 df-fil 20110 df-fm 20202 df-flim 20203 df-flf 20204 df-xms 20586 df-ms 20587 df-tms 20588 df-cncf 21145 df-limc 22033 df-dv 22034 df-log 22700 df-cxp 22701 df-dchr 23264

This theorem is referenced by: dchrisum0flblem2 23450 dchrisum0flb 23451

W3C validator