dvnmul - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvnmul		Structured version Visualization version Unicode version

Theorem dvnmul 40158

Description: Function-builder for the

-th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
dvnmul.s
dvnmul.x	ℂ_fld ↾_t
dvnmul.a	$/\$
dvnmul.cc	$/\$
dvnmul.n
dvnmulf
dvnmul.f
dvnmul.dvnf	$/\$
dvnmul.dvng	$/\$
dvnmul.c
dvnmul.d

**Assertion**
Ref	Expression
dvnmul

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem dvnmul Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. 2
2		dvnmul.n	. . 3
3		nn0uz 11722	. . . . 5
4	2, 3	syl6eleq 2711	. . . 4
5		eluzfz2 12349	. . . 4
6	4, 5	syl 17	. . 3
7		eleq1 2689	. . . . 5
8		fveq2 6191	. . . . . . 7
9		oveq2 6658	. . . . . . . . . 10
10	9	sumeq1d 14431	. . . . . . . . 9
11		oveq1 6657	. . . . . . . . . . 11
12		oveq1 6657	. . . . . . . . . . . . . 14
13	12	fveq2d 6195	. . . . . . . . . . . . 13
14	13	fveq1d 6193	. . . . . . . . . . . 12
15	14	oveq2d 6666	. . . . . . . . . . 11
16	11, 15	oveq12d 6668	. . . . . . . . . 10
17	16	sumeq2ad 14434	. . . . . . . . 9
18	10, 17	eqtrd 2656	. . . . . . . 8
19	18	mpteq2dv 4745	. . . . . . 7
20	8, 19	eqeq12d 2637	. . . . . 6
21	20	imbi2d 330	. . . . 5
22	7, 21	imbi12d 334	. . . 4
23		fveq2 6191	. . . . . . 7
24		simpl 473	. . . . . . . . . 10 $/\$
25	24	oveq2d 6666	. . . . . . . . 9 $/\$
26		simpll 790	. . . . . . . . . . 11 $/\$ $/\$
27	26	oveq1d 6665	. . . . . . . . . 10 $/\$ $/\$
28	26	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$
29	28	fveq2d 6195	. . . . . . . . . . . 12 $/\$ $/\$
30	29	fveq1d 6193	. . . . . . . . . . 11 $/\$ $/\$
31	30	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
32	27, 31	oveq12d 6668	. . . . . . . . 9 $/\$ $/\$
33	25, 32	sumeq12rdv 14438	. . . . . . . 8 $/\$
34	33	mpteq2dva 4744	. . . . . . 7
35	23, 34	eqeq12d 2637	. . . . . 6
36	35	imbi2d 330	. . . . 5
37		fveq2 6191	. . . . . . 7
38		simpl 473	. . . . . . . . . 10 $/\$
39	38	oveq2d 6666	. . . . . . . . 9 $/\$
40		simpll 790	. . . . . . . . . . 11 $/\$ $/\$
41	40	oveq1d 6665	. . . . . . . . . 10 $/\$ $/\$
42	40	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$
43	42	fveq2d 6195	. . . . . . . . . . . 12 $/\$ $/\$
44	43	fveq1d 6193	. . . . . . . . . . 11 $/\$ $/\$
45	44	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
46	41, 45	oveq12d 6668	. . . . . . . . 9 $/\$ $/\$
47	39, 46	sumeq12rdv 14438	. . . . . . . 8 $/\$
48	47	mpteq2dva 4744	. . . . . . 7
49	37, 48	eqeq12d 2637	. . . . . 6
50	49	imbi2d 330	. . . . 5
51		fveq2 6191	. . . . . . 7
52		simpl 473	. . . . . . . . . 10 $/\$
53	52	oveq2d 6666	. . . . . . . . 9 $/\$
54		simpll 790	. . . . . . . . . . 11 $/\$ $/\$
55	54	oveq1d 6665	. . . . . . . . . 10 $/\$ $/\$
56	54	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$
57	56	fveq2d 6195	. . . . . . . . . . . 12 $/\$ $/\$
58	57	fveq1d 6193	. . . . . . . . . . 11 $/\$ $/\$
59	58	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
60	55, 59	oveq12d 6668	. . . . . . . . 9 $/\$ $/\$
61	53, 60	sumeq12rdv 14438	. . . . . . . 8 $/\$
62	61	mpteq2dva 4744	. . . . . . 7
63	51, 62	eqeq12d 2637	. . . . . 6
64	63	imbi2d 330	. . . . 5
65		fveq2 6191	. . . . . . 7
66		simpl 473	. . . . . . . . . 10 $/\$
67	66	oveq2d 6666	. . . . . . . . 9 $/\$
68		simpll 790	. . . . . . . . . . 11 $/\$ $/\$
69	68	oveq1d 6665	. . . . . . . . . 10 $/\$ $/\$
70	68	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$
71	70	fveq2d 6195	. . . . . . . . . . . 12 $/\$ $/\$
72	71	fveq1d 6193	. . . . . . . . . . 11 $/\$ $/\$
73	72	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
74	69, 73	oveq12d 6668	. . . . . . . . 9 $/\$ $/\$
75	67, 74	sumeq12rdv 14438	. . . . . . . 8 $/\$
76	75	mpteq2dva 4744	. . . . . . 7
77	65, 76	eqeq12d 2637	. . . . . 6
78	77	imbi2d 330	. . . . 5
79		dvnmul.s	. . . . . . . . 9
80		recnprss 23668	. . . . . . . . 9
81	79, 80	syl 17	. . . . . . . 8
82		dvnmul.a	. . . . . . . . . 10 $/\$
83		dvnmul.cc	. . . . . . . . . 10 $/\$
84	82, 83	mulcld 10060	. . . . . . . . 9 $/\$
85		restsspw 16092	. . . . . . . . . . 11 ℂ_fld ↾_t
86		dvnmul.x	. . . . . . . . . . 11 ℂ_fld ↾_t
87	85, 86	sseldi 3601	. . . . . . . . . 10
88		elpwi 4168	. . . . . . . . . 10
89	87, 88	syl 17	. . . . . . . . 9
90		cnex 10017	. . . . . . . . . 10
91	90	a1i 11	. . . . . . . . 9
92	84, 89, 91, 79	mptelpm 39357	. . . . . . . 8
93		dvn0 23687	. . . . . . . 8 $/\$
94	81, 92, 93	syl2anc 693	. . . . . . 7
95		0z 11388	. . . . . . . . . . . 12
96		fzsn 12383	. . . . . . . . . . . 12
97	95, 96	ax-mp 5	. . . . . . . . . . 11
98	97	sumeq1i 14428	. . . . . . . . . 10
99	98	a1i 11	. . . . . . . . 9 $/\$
100		nfcvd 2765	. . . . . . . . . 10 $/\$
101		nfv 1843	. . . . . . . . . 10 $/\$
102		oveq2 6658	. . . . . . . . . . . . . 14
103		0nn0 11307	. . . . . . . . . . . . . . . 16
104		bcn0 13097	. . . . . . . . . . . . . . . 16
105	103, 104	ax-mp 5	. . . . . . . . . . . . . . 15
106	105	a1i 11	. . . . . . . . . . . . . 14
107	102, 106	eqtrd 2656	. . . . . . . . . . . . 13
108	107	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$
109		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
110	109	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
111		dvnmul.c	. . . . . . . . . . . . . . . . . . . . . 22
112		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . 22
114	111, 113	eqtri 2644	. . . . . . . . . . . . . . . . . . . . 21
115	114	a1i 11	. . . . . . . . . . . . . . . . . . . 20
116		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
117	116	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
118		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . 21
119	4, 118	syl 17	. . . . . . . . . . . . . . . . . . . 20
120		fvexd 6203	. . . . . . . . . . . . . . . . . . . 20
121	115, 117, 119, 120	fvmptd 6288	. . . . . . . . . . . . . . . . . . 19
122	121	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
123	110, 122	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
124		dvnmulf	. . . . . . . . . . . . . . . . . . . 20
125	82, 89, 91, 79	mptelpm 39357	. . . . . . . . . . . . . . . . . . . 20
126	124, 125	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19
127		dvn0 23687	. . . . . . . . . . . . . . . . . . 19 $/\$
128	81, 126, 127	syl2anc 693	. . . . . . . . . . . . . . . . . 18
129	128	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
130	123, 129	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$
131	130	fveq1d 6193	. . . . . . . . . . . . . . 15 $/\$
132	131	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
133		simpr 477	. . . . . . . . . . . . . . . 16 $/\$
134	124	fvmpt2 6291	. . . . . . . . . . . . . . . 16 $/\$
135	133, 82, 134	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$
136	135	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$
137	132, 136	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ $/\$
138		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
139		0m0e0 11130	. . . . . . . . . . . . . . . . . . . 20
140	139	a1i 11	. . . . . . . . . . . . . . . . . . 19
141	138, 140	eqtrd 2656	. . . . . . . . . . . . . . . . . 18
142	141	fveq2d 6195	. . . . . . . . . . . . . . . . 17
143	142	fveq1d 6193	. . . . . . . . . . . . . . . 16
144	143	adantl 482	. . . . . . . . . . . . . . 15 $/\$
145	144	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
146		dvnmul.d	. . . . . . . . . . . . . . . . . . . 20
147		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
148	147	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . 20
149	146, 148	eqtri 2644	. . . . . . . . . . . . . . . . . . 19
150	149	fveq1i 6192	. . . . . . . . . . . . . . . . . 18
151	150	a1i 11	. . . . . . . . . . . . . . . . 17
152		eqidd 2623	. . . . . . . . . . . . . . . . . 18
153		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
154	153	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
155		dvnmul.f	. . . . . . . . . . . . . . . . . . . . . 22
156	83, 89, 91, 79	mptelpm 39357	. . . . . . . . . . . . . . . . . . . . . 22
157	155, 156	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . 21
158		dvn0 23687	. . . . . . . . . . . . . . . . . . . . 21 $/\$
159	81, 157, 158	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20
160	159	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
161	154, 160	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$
162	155	a1i 11	. . . . . . . . . . . . . . . . . . 19
163		mptexg 6484	. . . . . . . . . . . . . . . . . . . 20
164	87, 163	syl 17	. . . . . . . . . . . . . . . . . . 19
165	162, 164	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18
166	152, 161, 119, 165	fvmptd 6288	. . . . . . . . . . . . . . . . 17
167	151, 166	eqtrd 2656	. . . . . . . . . . . . . . . 16
168	167	fveq1d 6193	. . . . . . . . . . . . . . 15
169	168	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
170	162, 83	fvmpt2d 6293	. . . . . . . . . . . . . . 15 $/\$
171	170	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$
172	145, 169, 171	3eqtrd 2660	. . . . . . . . . . . . 13 $/\$ $/\$
173	137, 172	oveq12d 6668	. . . . . . . . . . . 12 $/\$ $/\$
174	108, 173	oveq12d 6668	. . . . . . . . . . 11 $/\$ $/\$
175	84	mulid2d 10058	. . . . . . . . . . . 12 $/\$
176	175	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
177	174, 176	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
178		0re 10040	. . . . . . . . . . 11
179	178	a1i 11	. . . . . . . . . 10 $/\$
180	100, 101, 177, 179, 84	sumsnd 39185	. . . . . . . . 9 $/\$
181	99, 180	eqtr2d 2657	. . . . . . . 8 $/\$
182	181	mpteq2dva 4744	. . . . . . 7
183	94, 182	eqtrd 2656	. . . . . 6
184	183	a1i 11	. . . . 5
185		simp3 1063	. . . . . . 7 ..^ $/\$ $/\$
186		simp1 1061	. . . . . . 7 ..^ $/\$ $/\$ ..^
187		simp2 1062	. . . . . . . 8 ..^ $/\$ $/\$
188		pm3.35 611	. . . . . . . 8 $/\$
189	185, 187, 188	syl2anc 693	. . . . . . 7 ..^ $/\$ $/\$
190	81	adantr 481	. . . . . . . . . 10 $/\$ ..^
191	92	adantr 481	. . . . . . . . . 10 $/\$ ..^
192		elfzonn0 12512	. . . . . . . . . . 11 ..^
193	192	adantl 482	. . . . . . . . . 10 $/\$ ..^
194		dvnp1 23688	. . . . . . . . . 10 $/\$ $/\$
195	190, 191, 193, 194	syl3anc 1326	. . . . . . . . 9 $/\$ ..^
196	195	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
197		simpr 477	. . . . . . . . 9 $/\$ ..^ $/\$
198	197	oveq2d 6666	. . . . . . . 8 $/\$ ..^ $/\$
199		eqid 2622	. . . . . . . . . . 11 ℂ_fld ↾_t ℂ_fld ↾_t
200		eqid 2622	. . . . . . . . . . 11 ℂ_fld ℂ_fld
201	79	adantr 481	. . . . . . . . . . 11 $/\$ ..^
202	86	adantr 481	. . . . . . . . . . 11 $/\$ ..^ ℂ_fld ↾_t
203		fzfid 12772	. . . . . . . . . . 11 $/\$ ..^
204	192	adantr 481	. . . . . . . . . . . . . . . 16 ..^ $/\$
205		elfzelz 12342	. . . . . . . . . . . . . . . . 17
206	205	adantl 482	. . . . . . . . . . . . . . . 16 ..^ $/\$
207	204, 206	bccld 39531	. . . . . . . . . . . . . . 15 ..^ $/\$
208	207	nn0cnd 11353	. . . . . . . . . . . . . 14 ..^ $/\$
209	208	adantll 750	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
210	209	3adant3 1081	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
211		simpll 790	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
212		0zd 11389	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
213		elfzoel2 12469	. . . . . . . . . . . . . . . . . . . . 21 ..^
214	213	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
215	212, 214, 206	3jca 1242	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ $/\$ $/\$
216		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
217	216	adantl 482	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
218	206	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
219	213	zred 11482	. . . . . . . . . . . . . . . . . . . . 21 ..^
220	219	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
221	192	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . 22 ..^
222	221	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
223		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
224	223	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
225		elfzolt2 12479	. . . . . . . . . . . . . . . . . . . . . 22 ..^
226	225	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
227	218, 222, 220, 224, 226	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
228	218, 220, 227	ltled 10185	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
229	215, 217, 228	jca32 558	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
230		elfz2 12333	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
231	229, 230	sylibr 224	. . . . . . . . . . . . . . . . 17 ..^ $/\$
232	231	adantll 750	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
233		dvnmul.dvnf	. . . . . . . . . . . . . . . . 17 $/\$
234	111	a1i 11	. . . . . . . . . . . . . . . . . . 19
235		fvexd 6203	. . . . . . . . . . . . . . . . . . 19 $/\$
236	234, 235	fvmpt2d 6293	. . . . . . . . . . . . . . . . . 18 $/\$
237	236	feq1d 6030	. . . . . . . . . . . . . . . . 17 $/\$
238	233, 237	mpbird 247	. . . . . . . . . . . . . . . 16 $/\$
239	211, 232, 238	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
240	239	3adant3 1081	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
241		simp3 1063	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
242	240, 241	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
243	192	nn0zd 11480	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
244	243	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
245	244, 206	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
246	212, 214, 245	3jca 1242	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$ $/\$
247		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . . . . 24
248	247	zred 11482	. . . . . . . . . . . . . . . . . . . . . . 23
249	205	zred 11482	. . . . . . . . . . . . . . . . . . . . . . 23
250	248, 249	subge0d 10617	. . . . . . . . . . . . . . . . . . . . . 22
251	223, 250	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21
252	251	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
253	222, 218	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
254	220, 218	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
255	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
256	220, 255	jca 554	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $/\$
257		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
258	256, 257	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
259	222, 220, 218, 226	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
260	255, 218, 220, 217	lesub2dd 10644	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
261	253, 254, 258, 259, 260	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
262	219	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
263	262	subid1d 10381	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
264	263	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
265	261, 264	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
266	253, 220, 265	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
267	246, 252, 266	jca32 558	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
268		elfz2 12333	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
269	267, 268	sylibr 224	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
270	269	adantll 750	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
271		ovex 6678	. . . . . . . . . . . . . . . . . 18
272		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
273	272	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
274		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
275	274	feq1d 6030	. . . . . . . . . . . . . . . . . . 19
276	273, 275	imbi12d 334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
277		nfv 1843	. . . . . . . . . . . . . . . . . . 19 $/\$
278		eleq1 2689	. . . . . . . . . . . . . . . . . . . . 21
279	278	anbi2d 740	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
280		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
281	280	feq1d 6030	. . . . . . . . . . . . . . . . . . . 20
282	279, 281	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
283		dvnmul.dvng	. . . . . . . . . . . . . . . . . . 19 $/\$
284	277, 282, 283	chvar 2262	. . . . . . . . . . . . . . . . . 18 $/\$
285	271, 276, 284	vtocl 3259	. . . . . . . . . . . . . . . . 17 $/\$
286	211, 270, 285	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
287	149	a1i 11	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
288		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
289	288	adantl 482	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ $/\$
290		fvexd 6203	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
291	287, 289, 269, 290	fvmptd 6288	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
292	291	adantll 750	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
293	292	feq1d 6030	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
294	286, 293	mpbird 247	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
295	294	3adant3 1081	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
296	295, 241	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
297	242, 296	mulcld 10060	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
298	210, 297	mulcld 10060	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
299	210	3expa 1265	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
300	244	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
301	300, 206	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
302	212, 214, 301	3jca 1242	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $/\$ $/\$
303		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . . . . 26
304	248, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
305		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
306	249, 305	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
307	249	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . 26
308		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
309	249, 248, 308, 223	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . . . . . . . 26
310	249, 306, 304, 307, 309	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . 25
311	249, 304, 310	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . 24
312	311	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
313	222, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
314	313, 218	subge0d 10617	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
315	312, 314	mpbird 247	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
316	313, 218	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
317		elfzop1le2 39502	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
318	317	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
319	313, 220, 218, 318	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
320	260, 264	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
321	316, 254, 220, 319, 320	letrd 10194	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
322	302, 315, 321	jca32 558	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
323		elfz2 12333	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
324	322, 323	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
325	324	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
326		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
327		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22
328	327	anbi2d 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
329		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
330	329	feq1d 6030	. . . . . . . . . . . . . . . . . . . . 21
331	328, 330	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
332	326, 331, 284	vtocl 3259	. . . . . . . . . . . . . . . . . . 19 $/\$
333	211, 325, 332	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
334	149	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
335		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
336	335	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
337		fvexd 6203	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
338	334, 336, 325, 337	fvmptd 6288	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
339	338	feq1d 6030	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
340	333, 339	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
341	340	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
342	242	3expa 1265	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
343	341, 342	mulcomd 10061	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
344	343	oveq2d 6666	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
345	206	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
346	212, 214, 345	3jca 1242	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$ $/\$
347	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
348	347, 249, 306, 216, 307	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . 23
349	347, 306, 348	ltled 10185	. . . . . . . . . . . . . . . . . . . . . 22
350	349	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
351	218, 305	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
352	309	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
353	351, 313, 220, 352, 318	letrd 10194	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
354	346, 350, 353	jca32 558	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
355		elfz2 12333	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
356	354, 355	sylibr 224	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
357	356	adantll 750	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
358		ovex 6678	. . . . . . . . . . . . . . . . . . 19
359		eleq1 2689	. . . . . . . . . . . . . . . . . . . . 21
360	359	anbi2d 740	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
361		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
362	361	feq1d 6030	. . . . . . . . . . . . . . . . . . . 20
363	360, 362	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
364		nfv 1843	. . . . . . . . . . . . . . . . . . . . 21 $/\$
365		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . . 24
366	111, 365	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . . 23
367		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23
368	366, 367	nffv 6198	. . . . . . . . . . . . . . . . . . . . . 22
369		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22
370		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22
371	368, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . 21
372	364, 371	nfim 1825	. . . . . . . . . . . . . . . . . . . 20 $/\$
373		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
374	373	feq1d 6030	. . . . . . . . . . . . . . . . . . . . 21
375	279, 374	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
376	372, 375, 238	chvar 2262	. . . . . . . . . . . . . . . . . . 19 $/\$
377	358, 363, 376	vtocl 3259	. . . . . . . . . . . . . . . . . 18 $/\$
378	211, 357, 377	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
379	378	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
380	296	3expa 1265	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
381	379, 380	mulcld 10060	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
382	341, 342	mulcld 10060	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
383	381, 382	addcld 10059	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
384	344, 383	eqeltrrd 2702	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
385	299, 384	mulcld 10060	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
386	385	3impa 1259	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
387	211, 79	syl 17	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
388	178	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
389	211, 86	syl 17	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ ℂ_fld ↾_t
390	387, 389, 209	dvmptconst 40129	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
391	297	3expa 1265	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
392	211, 232, 236	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
393	392	eqcomd 2628	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
394	239	feqmptd 6249	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
395	393, 394	eqtr2d 2657	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
396	395	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
397	387, 80	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
398	211, 126	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
399		elfznn0 12433	. . . . . . . . . . . . . . . . . 18
400	399	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
401		dvnp1 23688	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
402	397, 398, 400, 401	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
403	402	eqcomd 2628	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
404	114	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
405		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
406	405	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
407		fvexd 6203	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
408	404, 406, 357, 407	fvmptd 6288	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
409	408	eqcomd 2628	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
410	378	feqmptd 6249	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
411	409, 410	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
412	396, 403, 411	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
413	292	eqcomd 2628	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
414	294	feqmptd 6249	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
415	413, 414	eqtr2d 2657	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
416	415	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
417	211, 157	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
418		fznn0sub 12373	. . . . . . . . . . . . . . . . . 18
419	418	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
420		dvnp1 23688	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
421	397, 417, 419, 420	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
422	421	eqcomd 2628	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
423	222	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
424		1cnd 10056	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
425	218	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
426	423, 424, 425	addsubd 10413	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
427	426	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
428	427	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ..^ $/\$
429	428	adantll 750	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
430	338	eqcomd 2628	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
431	340	feqmptd 6249	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
432	429, 430, 431	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
433	416, 422, 432	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
434	387, 342, 379, 412, 380, 341, 433	dvmptmul 23724	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
435	387, 299, 388, 390, 391, 383, 434	dvmptmul 23724	. . . . . . . . . . . 12 $/\$ ..^ $/\$
436	391	mul02d 10234	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
437	344	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
438	384, 299	mulcomd 10061	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
439	437, 438	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
440	436, 439	oveq12d 6668	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
441	385	addid2d 10237	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
442	440, 441	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
443	442	mpteq2dva 4744	. . . . . . . . . . . 12 $/\$ ..^ $/\$
444	435, 443	eqtrd 2656	. . . . . . . . . . 11 $/\$ ..^ $/\$
445	199, 200, 201, 202, 203, 298, 386, 444	dvmptfsum 23738	. . . . . . . . . 10 $/\$ ..^
446	209	adantlr 751	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
447	381	an32s 846	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
448		anass 681	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
449		ancom 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
450	449	anbi2i 730	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
451		anass 681	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
452	451	bicomi 214	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
453	450, 452	bitri 264	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
454	448, 453	bitri 264	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
455	454	imbi1i 339	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
456	342, 455	mpbi 220	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
457	454	imbi1i 339	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
458	341, 457	mpbi 220	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
459	456, 458	mulcld 10060	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
460	446, 447, 459	adddid 10064	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
461	460	sumeq2dv 14433	. . . . . . . . . . . 12 $/\$ ..^ $/\$
462	203	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
463	446, 447	mulcld 10060	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
464	446, 459	mulcld 10060	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
465	462, 463, 464	fsumadd 14470	. . . . . . . . . . . 12 $/\$ ..^ $/\$
466		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
467		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
468	467	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
469	468	fveq1d 6193	. . . . . . . . . . . . . . . . . . . 20
470		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
471	470	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
472	471	fveq1d 6193	. . . . . . . . . . . . . . . . . . . 20
473	469, 472	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
474	466, 473	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
475		nfcv 2764	. . . . . . . . . . . . . . . . . 18
476		nfcv 2764	. . . . . . . . . . . . . . . . . 18
477		nfcv 2764	. . . . . . . . . . . . . . . . . 18
478		nfcv 2764	. . . . . . . . . . . . . . . . . . 19
479		nfcv 2764	. . . . . . . . . . . . . . . . . . 19
480		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22
481	366, 480	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21
482		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21
483	481, 482	nffv 6198	. . . . . . . . . . . . . . . . . . . 20
484		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . 23
485	146, 484	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . 22
486		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22
487	485, 486	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21
488	487, 482	nffv 6198	. . . . . . . . . . . . . . . . . . . 20
489	483, 479, 488	nfov 6676	. . . . . . . . . . . . . . . . . . 19
490	478, 479, 489	nfov 6676	. . . . . . . . . . . . . . . . . 18
491	474, 475, 476, 477, 490	cbvsum 14425	. . . . . . . . . . . . . . . . 17
492	491	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
493		1zzd 11408	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
494	95	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
495	243	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
496		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
497		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21
498	497, 476	nfel 2777	. . . . . . . . . . . . . . . . . . . 20
499	496, 498	nfan 1828	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
500	490, 370	nfel 2777	. . . . . . . . . . . . . . . . . . 19
501	499, 500	nfim 1825	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
502		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
503	502	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
504	474	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19
505	503, 504	imbi12d 334	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
506	501, 505, 463	chvar 2262	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
507		oveq2 6658	. . . . . . . . . . . . . . . . . 18
508		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21
509	508	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
510	509	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
511		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
512	511	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
513	512	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
514	510, 513	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
515	507, 514	oveq12d 6668	. . . . . . . . . . . . . . . . 17
516	493, 494, 495, 506, 515	fsumshft 14512	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
517	492, 516	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
518		0p1e1 11132	. . . . . . . . . . . . . . . . . 18
519	518	oveq1i 6660	. . . . . . . . . . . . . . . . 17
520	519	sumeq1i 14428	. . . . . . . . . . . . . . . 16
521	520	a1i 11	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
522		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . 25
523	522	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . 24
524		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . 24
525	523, 524	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . 23
526	525	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
527	526	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21
528	527	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
529	221	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
530	529	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
531	523	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
532	524	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
533	530, 531, 532	subsub3d 10422	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
534	533	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
535	534	fveq1d 6193	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
536	528, 535	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
537	536	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
538	537	sumeq2dv 14433	. . . . . . . . . . . . . . . . 17 ..^
539	538	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
540		nfv 1843	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
541		nfcv 2764	. . . . . . . . . . . . . . . . 17
542		fzfid 12772	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
543	192	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
544	522	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
545		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
546	544, 545	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
547	543, 546	bccld 39531	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
548	547	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
549	548	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
550	549	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
551	1	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
552		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
553	213	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
554	552, 553, 544	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $/\$ $/\$
555	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
556	522	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
557		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
558		0lt1 10550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
559	558	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
560		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
561	555, 557, 556, 559, 560	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	555, 556, 561	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . 26
563	562	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
564	556	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
565	221	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
566		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
567	565, 566	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
568	219	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
569		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
570	569	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
571	317	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
572	564, 567, 568, 570, 571	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
573	554, 563, 572	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
574		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
575	573, 574	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
576	575	adantll 750	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
577	551, 576, 376	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
578	577	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
579		simplr 792	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
580	578, 579	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
581	243	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$
582	581	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
583	582, 544	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
584	552, 553, 583	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $/\$ $/\$
585	567, 564	subge0d 10617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
586	570, 585	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
587	567, 564	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
588	587	leidd 10594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
589	556, 561	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
590	589	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ $/\$
591	567, 590	ltsubrpd 11904	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$
592	587, 567, 568, 591, 571	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
593	587, 587, 568, 588, 592	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
594	587, 568, 593	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
595	584, 586, 594	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
596		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
597	595, 596	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
598	597	adantll 750	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
599		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
600		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26
601	485, 600	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . . 25
602	601, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . . . . 24
603	599, 602	nfim 1825	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
604		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
605		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25
606	605	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
607		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
608	607	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . 24
609	606, 608	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
610	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
611		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
612	610, 611	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
613	612	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
614	283, 613	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
615	603, 604, 609, 614	vtoclf 3258	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
616	551, 598, 615	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
617	616	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
618	617, 579	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
619	580, 618	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
620	550, 619	mulcld 10060	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
621		1zzd 11408	. . . . . . . . . . . . . . . . . . . . 21 ..^
622	243	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . 21 ..^
623	518	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . 23
624	623	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ..^
625	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
626		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
627	192	nn0ge0d 11354	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
628	625, 221, 626, 627	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . . . 22 ..^
629	624, 628	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 ..^
630	621, 622, 629	3jca 1242	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$
631		eluz2 11693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
632	630, 631	sylibr 224	. . . . . . . . . . . . . . . . . . 19 ..^
633		eluzfz2 12349	. . . . . . . . . . . . . . . . . . 19
634	632, 633	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
635	634	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
636		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
637	636	oveq2d 6666	. . . . . . . . . . . . . . . . . 18
638		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
639	638	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
640		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
641	640	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
642	641	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
643	639, 642	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
644	637, 643	oveq12d 6668	. . . . . . . . . . . . . . . . 17
645	540, 541, 542, 620, 635, 644	fsumsplit1 39804	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$
646		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
647	529, 646	pncand 10393	. . . . . . . . . . . . . . . . . . . . . 22 ..^
648	647	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ..^
649		bcnn 13099	. . . . . . . . . . . . . . . . . . . . . 22
650	192, 649	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ..^
651	648, 650	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 ..^
652	529, 646	addcld 10059	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
653	652	subidd 10380	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
654	653	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 ..^
655	654	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 ..^
656	655	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 ..^
657	651, 656	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 ..^
658	657	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
659		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
660		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
661	660	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
662		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
663		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26
664	366, 663	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . . 25
665	664, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . . . . 24
666	662, 665	nfim 1825	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
667		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
668		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25
669	668	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
670		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
671	670	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . 24
672	669, 671	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
673	666, 667, 672, 238	vtoclf 3258	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
674	659, 661, 673	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
675	674	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
676		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
677		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
678	485, 677	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . . . 26
679	678, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . . . . . 25
680	676, 679	nfim 1825	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
681		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . 24
682		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
683	682	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
684		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
685	684	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . . 25
686	683, 685	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
687	680, 681, 686, 614	vtoclf 3258	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
688	1, 119, 687	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22
689	688	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
690	689	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
691	675, 690	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
692	691	mulid2d 10058	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
693	658, 692	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
694		1m1e0 11089	. . . . . . . . . . . . . . . . . . . . . . . . 25
695	694	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . 24
696	3	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . 24
697	695, 696	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . 23
698	697	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ..^
699	192, 698	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . 21 ..^
700		fzdifsuc2 39525	. . . . . . . . . . . . . . . . . . . . 21 $\$
701	699, 700	syl 17	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$
702	701	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 ..^ $\$
703	702	sumeq1d 14431	. . . . . . . . . . . . . . . . . 18 ..^ $\$
704	703	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $\$
705	693, 704	oveq12d 6668	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$
706	539, 645, 705	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
707	517, 521, 706	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
708		nfcv 2764	. . . . . . . . . . . . . . . . 17
709	366, 677	nffv 6198	. . . . . . . . . . . . . . . . . . 19
710	709, 482	nffv 6198	. . . . . . . . . . . . . . . . . 18
711		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
712	485, 711	nffv 6198	. . . . . . . . . . . . . . . . . . 19
713	712, 482	nffv 6198	. . . . . . . . . . . . . . . . . 18
714	710, 479, 713	nfov 6676	. . . . . . . . . . . . . . . . 17
715	708, 479, 714	nfov 6676	. . . . . . . . . . . . . . . 16
716	696	a1i 11	. . . . . . . . . . . . . . . . . . 19 ..^
717	192, 716	eleqtrrd 2704	. . . . . . . . . . . . . . . . . 18 ..^
718		eluzfz1 12348	. . . . . . . . . . . . . . . . . 18
719	717, 718	syl 17	. . . . . . . . . . . . . . . . 17 ..^
720	719	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
721		oveq2 6658	. . . . . . . . . . . . . . . . 17
722	109	fveq1d 6193	. . . . . . . . . . . . . . . . . 18
723		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
724	723	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
725	724	fveq1d 6193	. . . . . . . . . . . . . . . . . 18
726	722, 725	oveq12d 6668	. . . . . . . . . . . . . . . . 17
727	721, 726	oveq12d 6668	. . . . . . . . . . . . . . . 16
728	496, 715, 462, 464, 720, 727	fsumsplit1 39804	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$
729	652	subid1d 10381	. . . . . . . . . . . . . . . . . . . . 21 ..^
730	729	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 ..^
731	730	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 ..^
732	731	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ..^
733	732	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ..^
734	733	oveq1d 6665	. . . . . . . . . . . . . . . 16 ..^ $\$ $\$
735	734	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$ $\$
736		bcn0 13097	. . . . . . . . . . . . . . . . . . . 20
737	192, 736	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
738	737	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ..^
739	738	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
740	709, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . . . . 24
741	676, 740	nfim 1825	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
742	109	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . 24
743	683, 742	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
744	741, 681, 743, 238	vtoclf 3258	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
745	1, 119, 744	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21
746	745	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
747	746	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
748	485, 663	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . 24
749	748, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . . . 23
750	662, 749	nfim 1825	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
751		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
752	751	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . 23
753	669, 752	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
754	750, 667, 753, 614	vtoclf 3258	. . . . . . . . . . . . . . . . . . . . 21 $/\$
755	659, 661, 754	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
756	755	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
757	747, 756	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
758	757	mulid2d 10058	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
759	739, 758	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
760		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 ..^
761		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $\$
762	243	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $\$
763		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
764		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
765	763, 764	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
766	765	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $\$
767	761, 762, 766	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $\$ $/\$ $/\$
768		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
769	763, 768	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
770		eldifsni 4320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
771	769, 770	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
772		elnnne0 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
773	771, 772	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
774		nnge1 11046	. . . . . . . . . . . . . . . . . . . . . . . . . 26
775	773, 774	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
776	775	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $\$
777		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . 26
778	763, 777	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
779	778	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $\$
780	767, 776, 779	jca32 558	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
781		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
782	780, 781	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $\$
783	782	ex 450	. . . . . . . . . . . . . . . . . . . . 21 ..^ $\$
784		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
785		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
786		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
787	784, 785, 786	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
788	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
789	786	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
790		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
791	558	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
792		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
793	788, 790, 789, 791, 792	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
794	788, 789, 793	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . 26
795		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . 26
796	787, 794, 795	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
797		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
798	796, 797	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . 24
799	788, 793	gtned 10172	. . . . . . . . . . . . . . . . . . . . . . . . 25
800		nelsn 4212	. . . . . . . . . . . . . . . . . . . . . . . . 25
801	799, 800	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
802	798, 801	eldifd 3585	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
803	802	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $\$
804	803	ex 450	. . . . . . . . . . . . . . . . . . . . 21 ..^ $\$
805	783, 804	impbid 202	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$
806	760, 805	alrimi 2082	. . . . . . . . . . . . . . . . . . 19 ..^ $\$
807		dfcleq 2616	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
808	806, 807	sylibr 224	. . . . . . . . . . . . . . . . . 18 ..^ $\$
809	808	sumeq1d 14431	. . . . . . . . . . . . . . . . 17 ..^ $\$
810	809	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$
811	759, 810	oveq12d 6668	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$
812	728, 735, 811	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
813	707, 812	oveq12d 6668	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
814		fzfid 12772	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
815	192	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
816	803, 765	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
817		1zzd 11408	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
818	816, 817	zsubcld 11487	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
819	815, 818	bccld 39531	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
820	819	nn0cnd 11353	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
821	820	adantll 750	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
822	821	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
823		simpl 473	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$
824		fzelp1 12393	. . . . . . . . . . . . . . . . . . 19
825	824	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
826	823, 825, 580	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
827	825, 618	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
828	826, 827	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
829	822, 828	mulcld 10060	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
830	814, 829	fsumcl 14464	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
831	192	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
832		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . 21
833	832	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
834	831, 833	bccld 39531	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
835	834	nn0cnd 11353	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
836	835	adantll 750	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
837	836	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
838		simpll 790	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ ..^
839		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
840	798	ssriv 3607	. . . . . . . . . . . . . . . . . . . 20
841		id 22	. . . . . . . . . . . . . . . . . . . 20
842	840, 841	sseldi 3601	. . . . . . . . . . . . . . . . . . 19
843	842	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
844	838, 839, 843, 456	syl21anc 1325	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
845	843, 458	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
846	844, 845	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
847	837, 846	mulcld 10060	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
848	814, 847	fsumcl 14464	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
849	691, 830, 757, 848	add4d 10264	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
850		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21
851	850	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
852		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
853	852	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21
854		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . 23
855	854	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
856	855	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21
857	853, 856	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20
858	851, 857	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
859		nfcv 2764	. . . . . . . . . . . . . . . . . . 19
860		nfcv 2764	. . . . . . . . . . . . . . . . . . 19
861		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
862	368, 482	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21
863	601, 482	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21
864	862, 479, 863	nfov 6676	. . . . . . . . . . . . . . . . . . . 20
865	861, 479, 864	nfov 6676	. . . . . . . . . . . . . . . . . . 19
866		nfcv 2764	. . . . . . . . . . . . . . . . . . 19
867	858, 859, 860, 865, 866	cbvsum 14425	. . . . . . . . . . . . . . . . . 18
868	867	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
869	868	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
870		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . 24
871	833, 870	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
872	831, 871	bccld 39531	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
873	872	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
874	873	adantll 750	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
875	874	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
876	875, 846	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
877	814, 876, 847	fsumadd 14470	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
878	877	eqcomd 2628	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
879	873, 835	addcomd 10238	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
880		bcpasc 13108	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
881	831, 833, 880	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
882	879, 881	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
883	882	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
884	883	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
885	884	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
886	875, 837, 846	adddird 10065	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
887	885, 886	eqtr2d 2657	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
888	887	sumeq2dv 14433	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
889	869, 878, 888	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
890	889	oveq2d 6666	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
891		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . . . 22
892	831, 891	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
893	892, 833	bccld 39531	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
894	893	nn0cnd 11353	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
895	894	adantll 750	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
896	895	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
897	896, 846	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
898	814, 897	fsumcl 14464	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
899	691, 757, 898	addassd 10062	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
900	192, 891	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ..^
901		bcn0 13097	. . . . . . . . . . . . . . . . . . . . . 22
902	900, 901	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ..^
903	902, 732	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 ..^
904	903	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
905	904, 758	eqtr2d 2657	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
906	808	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $\$
907	906	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $\$
908	907	sumeq1d 14431	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $\$
909	905, 908	oveq12d 6668	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $\$
910		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
911	910, 479, 714	nfov 6676	. . . . . . . . . . . . . . . . . . 19
912	204, 891	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
913	912, 206	bccld 39531	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
914	913	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
915	914	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
916	915	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
917	916, 459	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
918		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
919	918, 726	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
920	496, 911, 462, 917, 720, 919	fsumsplit1 39804	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $\$
921	920	eqcomd 2628	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $\$
922	909, 921	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
923	922	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
924		bcnn 13099	. . . . . . . . . . . . . . . . . . . 20
925	900, 924	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
926	925	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
927	926	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
928	654	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^
929	928	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
930	689, 929	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
931	930	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
932		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
933	931, 932	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
934	675, 933	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
935	934	mulid2d 10058	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
936	656	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
937	927, 935, 936	3eqtrrd 2661	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
938		fzdifsuc 12400	. . . . . . . . . . . . . . . . . . 19 $\$
939	717, 938	syl 17	. . . . . . . . . . . . . . . . . 18 ..^ $\$
940	939	sumeq1d 14431	. . . . . . . . . . . . . . . . 17 ..^ $\$
941	940	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$
942	937, 941	oveq12d 6668	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$
943		nfcv 2764	. . . . . . . . . . . . . . . . . 18
944	664, 482	nffv 6198	. . . . . . . . . . . . . . . . . . 19
945		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21
946	485, 945	nffv 6198	. . . . . . . . . . . . . . . . . . . 20
947	946, 482	nffv 6198	. . . . . . . . . . . . . . . . . . 19
948	944, 479, 947	nfov 6676	. . . . . . . . . . . . . . . . . 18
949	943, 479, 948	nfov 6676	. . . . . . . . . . . . . . . . 17
950		fzfid 12772	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
951	900	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
952		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23
953	952	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
954	951, 953	bccld 39531	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
955	954	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
956	955	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
957	956	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
958	659	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
959	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
960	213	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
961	959, 960, 953	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $/\$ $/\$
962		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . 26
963	962	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
964	953	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
965	951	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
966	219	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
967		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
968	967	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
969	317	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
970	964, 965, 966, 968, 969	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
971	961, 963, 970	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
972	971, 230	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
973	972	adantll 750	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
974	958, 973, 238	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
975	974	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
976		simplr 792	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
977	975, 976	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
978	958	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
979	622	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
980	979, 953	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
981	959, 960, 980	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $/\$ $/\$
982	965, 964	subge0d 10617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
983	968, 982	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
984	965, 964	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
985	966, 964	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
986	966, 178, 257	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
987	965, 966, 964, 969	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
988	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$
989	988, 964, 966, 963	lesub2dd 10644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$
990	984, 985, 986, 987, 989	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
991	263	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$
992	990, 991	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$
993	981, 983, 992	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $/\$ $/\$ $/\$ $/\$
994	993, 323	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
995	994	adantll 750	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
996	995	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
997		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
998	997	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . 23
999	328, 998	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
1000	485, 367	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . . 25
1001	1000, 369, 370	nff 6041	. . . . . . . . . . . . . . . . . . . . . . . 24
1002	364, 1001	nfim 1825	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
1003		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
1004	1003	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . 24
1005	279, 1004	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
1006	1002, 1005, 614	chvar 2262	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1007	326, 999, 1006	vtocl 3259	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1008	978, 996, 1007	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
1009	1008, 976	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
1010	977, 1009	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
1011	957, 1010	mulcld 10060	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
1012	900, 716	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . 19 ..^
1013		eluzfz2 12349	. . . . . . . . . . . . . . . . . . 19
1014	1012, 1013	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
1015	1014	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
1016		oveq2 6658	. . . . . . . . . . . . . . . . . 18
1017	670	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
1018		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
1019	1018	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
1020	1019	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
1021	1017, 1020	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
1022	1016, 1021	oveq12d 6668	. . . . . . . . . . . . . . . . 17
1023	496, 949, 950, 1011, 1015, 1022	fsumsplit1 39804	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$
1024	1023	eqcomd 2628	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$
1025	923, 942, 1024	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
1026	890, 899, 1025	3eqtrd 2660	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
1027	813, 849, 1026	3eqtrd 2660	. . . . . . . . . . . 12 $/\$ ..^ $/\$
1028	461, 465, 1027	3eqtrd 2660	. . . . . . . . . . 11 $/\$ ..^ $/\$
1029	1028	mpteq2dva 4744	. . . . . . . . . 10 $/\$ ..^
1030	445, 1029	eqtrd 2656	. . . . . . . . 9 $/\$ ..^
1031	1030	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
1032	196, 198, 1031	3eqtrd 2660	. . . . . . 7 $/\$ ..^ $/\$
1033	185, 186, 189, 1032	syl21anc 1325	. . . . . 6 ..^ $/\$ $/\$
1034	1033	3exp 1264	. . . . 5 ..^
1035	36, 50, 64, 78, 184, 1034	fzind2 12586	. . . 4
1036	22, 1035	vtoclg 3266	. . 3
1037	2, 6, 1036	sylc 65	. 2
1038	1, 1037	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wceq 1483

wcel 1990

wne 2794

cvv 3200 $\$ cdif 3571

wss 3574

cpw 4158

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

wf 5884

cfv 5888 (class class class)co 6650

cpm 7858

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cfz 12326 ..^cfzo 12465

cbc 13089

csu 14416 ↾_t crest 16081

ctopn 16082 ℂ_fldccnfld 19746

cdv 23627

cdvn 23628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-dvn 23632

This theorem is referenced by: dvnprodlem2 40162

W3C validator