ovolicc2lem4OLD - Metamath Proof Explorer

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

Theorem ovolicc2lem4OLD 22473

Description: Lemma for ovolicc2 22476. (Contributed by Mario Carneiro, 14-Jun-2014.) Obsolete version of ovolicc2lem4 22474 as of 17-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)

**Hypotheses**
Ref	Expression
ovolicc.1
ovolicc.2
ovolicc.3
ovolicc2.4
ovolicc2.5
ovolicc2.6
ovolicc2.7
ovolicc2.8
ovolicc2.9	$/\$
ovolicc2.10
ovolicc2.11
ovolicc2.12	$/\$
ovolicc2.13
ovolicc2.14
ovolicc2.15
ovolicc2.16
ovolicc2lem4OLD.17

**Assertion**
Ref	Expression
ovolicc2lem4OLD

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem ovolicc2lem4OLD Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		arch 10866	. . . . 5
2	1	ad2antlr 733	. . . 4 $/\$ $/\$
3		df-ima 4847	. . . . . . . . . . . . . . . 16
4		ovolicc2.8	. . . . . . . . . . . . . . . . . . 19
5		nnuz 11194	. . . . . . . . . . . . . . . . . . . . 21
6		ovolicc2.15	. . . . . . . . . . . . . . . . . . . . 21
7		1zzd 10968	. . . . . . . . . . . . . . . . . . . . 21
8		ovolicc2.14	. . . . . . . . . . . . . . . . . . . . 21
9		ovolicc2.11	. . . . . . . . . . . . . . . . . . . . 21
10	5, 6, 7, 8, 9	algrf 14532	. . . . . . . . . . . . . . . . . . . 20
11		ovolicc2.10	. . . . . . . . . . . . . . . . . . . . 21
12		ssrab2 3514	. . . . . . . . . . . . . . . . . . . . 21
13	11, 12	eqsstri 3462	. . . . . . . . . . . . . . . . . . . 20
14		fss 5737	. . . . . . . . . . . . . . . . . . . 20 $/\$
15	10, 13, 14	sylancl 668	. . . . . . . . . . . . . . . . . . 19
16		fco 5739	. . . . . . . . . . . . . . . . . . 19 $/\$
17	4, 15, 16	syl2anc 667	. . . . . . . . . . . . . . . . . 18
18		elfznn 11828	. . . . . . . . . . . . . . . . . . 19
19	18	ssriv 3436	. . . . . . . . . . . . . . . . . 18
20		fssres 5749	. . . . . . . . . . . . . . . . . 18 $/\$
21	17, 19, 20	sylancl 668	. . . . . . . . . . . . . . . . 17
22		frn 5735	. . . . . . . . . . . . . . . . 17
23	21, 22	syl 17	. . . . . . . . . . . . . . . 16
24	3, 23	syl5eqss 3476	. . . . . . . . . . . . . . 15
25		nnssre 10613	. . . . . . . . . . . . . . 15
26	24, 25	syl6ss 3444	. . . . . . . . . . . . . 14
27	26	ad3antrrr 736	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
28		simpr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	27, 28	sseldd 3433	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30		simpllr 769	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
31		nnre 10616	. . . . . . . . . . . . 13
32	31	ad2antlr 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33		lelttr 9724	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
34	29, 30, 32, 33	syl3anc 1268	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
35	34	ancomsd 456	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
36	35	expdimp 439	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
37	36	an32s 813	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
38	37	ralimdva 2796	. . . . . . 7 $/\$ $/\$ $/\$
39	38	impancom 442	. . . . . 6 $/\$ $/\$ $/\$
40	39	an32s 813	. . . . 5 $/\$ $/\$ $/\$
41	40	reximdva 2862	. . . 4 $/\$ $/\$
42	2, 41	mpd 15	. . 3 $/\$ $/\$
43		fzfid 12186	. . . . 5
44		fvres 5879	. . . . . . . . . . . . . . 15
45	44	adantl 468	. . . . . . . . . . . . . 14 $/\$
46		fvco3 5942	. . . . . . . . . . . . . . 15 $/\$
47	10, 18, 46	syl2an 480	. . . . . . . . . . . . . 14 $/\$
48	45, 47	eqtrd 2485	. . . . . . . . . . . . 13 $/\$
49	48	adantrr 723	. . . . . . . . . . . 12 $/\$ $/\$
50		fvres 5879	. . . . . . . . . . . . . 14
51	50	ad2antll 735	. . . . . . . . . . . . 13 $/\$ $/\$
52		elfznn 11828	. . . . . . . . . . . . . . 15
53	52	adantl 468	. . . . . . . . . . . . . 14 $/\$
54		fvco3 5942	. . . . . . . . . . . . . 14 $/\$
55	10, 53, 54	syl2an 480	. . . . . . . . . . . . 13 $/\$ $/\$
56	51, 55	eqtrd 2485	. . . . . . . . . . . 12 $/\$ $/\$
57	49, 56	eqeq12d 2466	. . . . . . . . . . 11 $/\$ $/\$
58		fveq2 5865	. . . . . . . . . . . . 13
59	58	fveq2d 5869	. . . . . . . . . . . 12
60	19	a1i 11	. . . . . . . . . . . . . . . . 17
61		elfznn 11828	. . . . . . . . . . . . . . . . . . . . 21
62	61	ad2antlr 733	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
63	62	nnred 10624	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		ovolicc2.16	. . . . . . . . . . . . . . . . . . . . . . 23
65		ssrab2 3514	. . . . . . . . . . . . . . . . . . . . . . 23
66	64, 65	eqsstri 3462	. . . . . . . . . . . . . . . . . . . . . 22
67	66, 25	sstri 3441	. . . . . . . . . . . . . . . . . . . . 21
68		ovolicc2lem4OLD.17	. . . . . . . . . . . . . . . . . . . . . 22
69	66, 5	sseqtri 3464	. . . . . . . . . . . . . . . . . . . . . . 23
70		1z 10967	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	5	uzinf 12179	. . . . . . . . . . . . . . . . . . . . . . . . 25
72	70, 71	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
73		ovolicc2.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74		elin 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
75	73, 74	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
76	75	simprd 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		ssfi 7792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
78	76, 13, 77	sylancl 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
79	78	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
80	10	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
81		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
82	81	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
83	82	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84		simpll 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
85		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
86		ral0 3874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
87		simplr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
88	87	raleqdv 2993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
89	86, 88	mpbiri 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
90	89	ralrimivw 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
91		rabid2 2968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
92	90, 91	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
93	85, 92	eleqtrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
94		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
95	94, 92	eleqtrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
96		ovolicc.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
97		ovolicc.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
98		ovolicc.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
99		ovolicc2.4	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100		ovolicc2.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
101		ovolicc2.7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102		ovolicc2.9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103		ovolicc2.12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
104		ovolicc2.13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
105	96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64	ovolicc2lem3 22472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
106	84, 93, 95, 105	syl12anc 1266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
107	83, 106	syl5ibr 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
108	107	ralrimivva 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
109		dff13 6159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
110	80, 108, 109	sylanbrc 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
111		f1domg 7589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112	79, 110, 111	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
113		domfi 7793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
114	79, 112, 113	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
115	114	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . 25
116	115	necon3bd 2638	. . . . . . . . . . . . . . . . . . . . . . . 24
117	72, 116	mpi 20	. . . . . . . . . . . . . . . . . . . . . . 23
118		infmssuzclOLD 11247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
119	69, 117, 118	sylancr 669	. . . . . . . . . . . . . . . . . . . . . 22
120	68, 119	syl5eqel 2533	. . . . . . . . . . . . . . . . . . . . 21
121	67, 120	sseldi 3430	. . . . . . . . . . . . . . . . . . . 20
122	121	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123	67	sseli 3428	. . . . . . . . . . . . . . . . . . . 20
124	123	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125		elfzle2 11803	. . . . . . . . . . . . . . . . . . . 20
126	125	ad2antlr 733	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
127		infmssuzleOLD 11246	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128	69, 127	mpan 676	. . . . . . . . . . . . . . . . . . . . 21
129	68, 128	syl5eqbr 4436	. . . . . . . . . . . . . . . . . . . 20
130	129	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
131	63, 122, 124, 126, 130	letrd 9792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
132	131	ralrimiva 2802	. . . . . . . . . . . . . . . . 17 $/\$
133	60, 132	ssrabdv 3508	. . . . . . . . . . . . . . . 16
134	133	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$
135		simprl 764	. . . . . . . . . . . . . . 15 $/\$ $/\$
136	134, 135	sseldd 3433	. . . . . . . . . . . . . 14 $/\$ $/\$
137		simprr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	134, 137	sseldd 3433	. . . . . . . . . . . . . 14 $/\$ $/\$
139	136, 138	jca 535	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139, 105	syldan 473	. . . . . . . . . . . 12 $/\$ $/\$
141	59, 140	syl5ibr 225	. . . . . . . . . . 11 $/\$ $/\$
142	57, 141	sylbid 219	. . . . . . . . . 10 $/\$ $/\$
143	142	ralrimivva 2809	. . . . . . . . 9
144		dff13 6159	. . . . . . . . 9 $/\$
145	21, 143, 144	sylanbrc 670	. . . . . . . 8
146		f1f1orn 5825	. . . . . . . 8
147	145, 146	syl 17	. . . . . . 7
148		f1oeq3 5807	. . . . . . . 8
149	3, 148	ax-mp 5	. . . . . . 7
150	147, 149	sylibr 216	. . . . . 6
151		f1ofo 5821	. . . . . 6
152	150, 151	syl 17	. . . . 5
153		fofi 7860	. . . . 5 $/\$
154	43, 152, 153	syl2anc 667	. . . 4
155		fimaxre2 10552	. . . 4 $/\$
156	26, 154, 155	syl2anc 667	. . 3
157	42, 156	r19.29a 2932	. 2
158	97, 96	resubcld 10047	. . . . 5
159	158	rexrd 9690	. . . 4
160	159	adantr 467	. . 3 $/\$ $/\$
161		fzfid 12186	. . . . . 6
162		elfznn 11828	. . . . . . . . 9
163		eqid 2451	. . . . . . . . . . . 12
164	163	ovolfsf 22424	. . . . . . . . . . 11
165	100, 164	syl 17	. . . . . . . . . 10
166	165	ffvelrnda 6022	. . . . . . . . 9 $/\$
167	162, 166	sylan2 477	. . . . . . . 8 $/\$
168		elrege0 11738	. . . . . . . 8 $/\$
169	167, 168	sylib 200	. . . . . . 7 $/\$ $/\$
170	169	simpld 461	. . . . . 6 $/\$
171	161, 170	fsumrecl 13800	. . . . 5
172	171	adantr 467	. . . 4 $/\$ $/\$
173	172	rexrd 9690	. . 3 $/\$ $/\$
174	163, 99	ovolsf 22425	. . . . . . . . 9
175	100, 174	syl 17	. . . . . . . 8
176		frn 5735	. . . . . . . 8
177	175, 176	syl 17	. . . . . . 7
178		rge0ssre 11740	. . . . . . 7
179	177, 178	syl6ss 3444	. . . . . 6
180		ressxr 9684	. . . . . 6
181	179, 180	syl6ss 3444	. . . . 5
182		supxrcl 11600	. . . . 5
183	181, 182	syl 17	. . . 4
184	183	adantr 467	. . 3 $/\$ $/\$
185	158	adantr 467	. . . 4 $/\$ $/\$
186	24	sselda 3432	. . . . . . 7 $/\$
187	178, 166	sseldi 3430	. . . . . . 7 $/\$
188	186, 187	syldan 473	. . . . . 6 $/\$
189	154, 188	fsumrecl 13800	. . . . 5
190	189	adantr 467	. . . 4 $/\$ $/\$
191		inss2 3653	. . . . . . . . . . 11
192		fss 5737	. . . . . . . . . . 11 $/\$
193	100, 191, 192	sylancl 668	. . . . . . . . . 10
194	66, 120	sseldi 3430	. . . . . . . . . . . 12
195	15, 194	ffvelrnd 6023	. . . . . . . . . . 11
196	4, 195	ffvelrnd 6023	. . . . . . . . . 10
197	193, 196	ffvelrnd 6023	. . . . . . . . 9
198		xp2nd 6824	. . . . . . . . 9
199	197, 198	syl 17	. . . . . . . 8
200	13, 8	sseldi 3430	. . . . . . . . . . 11
201	4, 200	ffvelrnd 6023	. . . . . . . . . 10
202	193, 201	ffvelrnd 6023	. . . . . . . . 9
203		xp1st 6823	. . . . . . . . 9
204	202, 203	syl 17	. . . . . . . 8
205	199, 204	resubcld 10047	. . . . . . 7
206		fveq2 5865	. . . . . . . . . 10
207	187	recnd 9669	. . . . . . . . . . 11 $/\$
208	186, 207	syldan 473	. . . . . . . . . 10 $/\$
209	206, 43, 150, 48, 208	fsumf1o 13789	. . . . . . . . 9
210	100	adantr 467	. . . . . . . . . . 11 $/\$
211	4	adantr 467	. . . . . . . . . . . 12 $/\$
212		ffvelrn 6020	. . . . . . . . . . . . 13 $/\$
213	15, 18, 212	syl2an 480	. . . . . . . . . . . 12 $/\$
214	211, 213	ffvelrnd 6023	. . . . . . . . . . 11 $/\$
215	163	ovolfsval 22423	. . . . . . . . . . 11 $/\$
216	210, 214, 215	syl2anc 667	. . . . . . . . . 10 $/\$
217	216	sumeq2dv 13769	. . . . . . . . 9
218	193	adantr 467	. . . . . . . . . . . . . . 15 $/\$
219	4	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
220	15	ffvelrnda 6022	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	ffvelrnd 6023	. . . . . . . . . . . . . . 15 $/\$
222	218, 221	ffvelrnd 6023	. . . . . . . . . . . . . 14 $/\$
223		xp2nd 6824	. . . . . . . . . . . . . 14
224	222, 223	syl 17	. . . . . . . . . . . . 13 $/\$
225	18, 224	sylan2 477	. . . . . . . . . . . 12 $/\$
226	225	recnd 9669	. . . . . . . . . . 11 $/\$
227	193	adantr 467	. . . . . . . . . . . . . 14 $/\$
228	227, 214	ffvelrnd 6023	. . . . . . . . . . . . 13 $/\$
229		xp1st 6823	. . . . . . . . . . . . 13
230	228, 229	syl 17	. . . . . . . . . . . 12 $/\$
231	230	recnd 9669	. . . . . . . . . . 11 $/\$
232	43, 226, 231	fsumsub 13849	. . . . . . . . . 10
233	69, 120	sseldi 3430	. . . . . . . . . . . . 13
234		fveq2 5865	. . . . . . . . . . . . . . . 16
235	234	fveq2d 5869	. . . . . . . . . . . . . . 15
236	235	fveq2d 5869	. . . . . . . . . . . . . 14
237	236	fveq2d 5869	. . . . . . . . . . . . 13
238	233, 226, 237	fsumm1 13812	. . . . . . . . . . . 12
239		fzfid 12186	. . . . . . . . . . . . . . 15
240		elfznn 11828	. . . . . . . . . . . . . . . 16
241	240, 224	sylan2 477	. . . . . . . . . . . . . . 15 $/\$
242	239, 241	fsumrecl 13800	. . . . . . . . . . . . . 14
243	242	recnd 9669	. . . . . . . . . . . . 13
244	199	recnd 9669	. . . . . . . . . . . . 13
245	243, 244	addcomd 9835	. . . . . . . . . . . 12
246	238, 245	eqtrd 2485	. . . . . . . . . . 11
247		fveq2 5865	. . . . . . . . . . . . . . . 16
248	247	fveq2d 5869	. . . . . . . . . . . . . . 15
249	248	fveq2d 5869	. . . . . . . . . . . . . 14
250	249	fveq2d 5869	. . . . . . . . . . . . 13
251	233, 231, 250	fsum1p 13814	. . . . . . . . . . . 12
252	5, 6, 7, 8	algr0 14531	. . . . . . . . . . . . . . . 16
253	252	fveq2d 5869	. . . . . . . . . . . . . . 15
254	253	fveq2d 5869	. . . . . . . . . . . . . 14
255	254	fveq2d 5869	. . . . . . . . . . . . 13
256	7	peano2zd 11043	. . . . . . . . . . . . . . 15
257	194	nnzd 11039	. . . . . . . . . . . . . . 15
258		fzp1ss 11847	. . . . . . . . . . . . . . . . . 18
259	70, 258	mp1i 13	. . . . . . . . . . . . . . . . 17
260	259	sselda 3432	. . . . . . . . . . . . . . . 16 $/\$
261	260, 231	syldan 473	. . . . . . . . . . . . . . 15 $/\$
262		fveq2 5865	. . . . . . . . . . . . . . . . . 18
263	262	fveq2d 5869	. . . . . . . . . . . . . . . . 17
264	263	fveq2d 5869	. . . . . . . . . . . . . . . 16
265	264	fveq2d 5869	. . . . . . . . . . . . . . 15
266	7, 256, 257, 261, 265	fsumshftm 13842	. . . . . . . . . . . . . 14
267		ax-1cn 9597	. . . . . . . . . . . . . . . . . 18
268	267, 267	pncan3oi 9891	. . . . . . . . . . . . . . . . 17
269	268	oveq1i 6300	. . . . . . . . . . . . . . . 16
270	269	sumeq1i 13764	. . . . . . . . . . . . . . 15
271		oveq1 6297	. . . . . . . . . . . . . . . . . . . 20
272	271	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19
273	272	fveq2d 5869	. . . . . . . . . . . . . . . . . 18
274	273	fveq2d 5869	. . . . . . . . . . . . . . . . 17
275	274	fveq2d 5869	. . . . . . . . . . . . . . . 16
276	275	cbvsumv 13762	. . . . . . . . . . . . . . 15
277	270, 276	eqtri 2473	. . . . . . . . . . . . . 14
278	266, 277	syl6eq 2501	. . . . . . . . . . . . 13
279	255, 278	oveq12d 6308	. . . . . . . . . . . 12
280	251, 279	eqtrd 2485	. . . . . . . . . . 11
281	246, 280	oveq12d 6308	. . . . . . . . . 10
282	204	recnd 9669	. . . . . . . . . . 11
283		peano2nn 10621	. . . . . . . . . . . . . . . . . 18
284		ffvelrn 6020	. . . . . . . . . . . . . . . . . 18 $/\$
285	15, 283, 284	syl2an 480	. . . . . . . . . . . . . . . . 17 $/\$
286	219, 285	ffvelrnd 6023	. . . . . . . . . . . . . . . 16 $/\$
287	218, 286	ffvelrnd 6023	. . . . . . . . . . . . . . 15 $/\$
288		xp1st 6823	. . . . . . . . . . . . . . 15
289	287, 288	syl 17	. . . . . . . . . . . . . 14 $/\$
290	240, 289	sylan2 477	. . . . . . . . . . . . 13 $/\$
291	239, 290	fsumrecl 13800	. . . . . . . . . . . 12
292	291	recnd 9669	. . . . . . . . . . 11
293	244, 243, 282, 292	addsub4d 10033	. . . . . . . . . 10
294	232, 281, 293	3eqtrd 2489	. . . . . . . . 9
295	209, 217, 294	3eqtrd 2489	. . . . . . . 8
296	295, 189	eqeltrrd 2530	. . . . . . 7
297		fveq2 5865	. . . . . . . . . . . . . . 15
298	297	eleq2d 2514	. . . . . . . . . . . . . 14
299	298, 64	elrab2 3198	. . . . . . . . . . . . 13 $/\$
300	120, 299	sylib 200	. . . . . . . . . . . 12 $/\$
301	300	simprd 465	. . . . . . . . . . 11
302	96, 97, 98, 99, 100, 73, 101, 4, 102	ovolicc2lem1 22470	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
303	195, 302	mpdan 674	. . . . . . . . . . 11 $/\$ $/\$
304	301, 303	mpbid 214	. . . . . . . . . 10 $/\$ $/\$
305	304	simp3d 1022	. . . . . . . . 9
306	96, 97, 98, 99, 100, 73, 101, 4, 102	ovolicc2lem1 22470	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
307	200, 306	mpdan 674	. . . . . . . . . . 11 $/\$ $/\$
308	104, 307	mpbid 214	. . . . . . . . . 10 $/\$ $/\$
309	308	simp2d 1021	. . . . . . . . 9
310	97, 204, 199, 96, 305, 309	lt2subd 10237	. . . . . . . 8
311	158, 205, 310	ltled 9783	. . . . . . 7
312	240	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
313		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
314	257	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
315		elfzm11 11865	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
316	70, 314, 315	sylancr 669	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
317	313, 316	mpbid 214	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
318	317	simp3d 1022	. . . . . . . . . . . . . . . . . . . 20 $/\$
319	312	nnred 10624	. . . . . . . . . . . . . . . . . . . . 21 $/\$
320	121	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$
321	319, 320	ltnled 9782	. . . . . . . . . . . . . . . . . . . 20 $/\$
322	318, 321	mpbid 214	. . . . . . . . . . . . . . . . . . 19 $/\$
323		infmssuzleOLD 11246	. . . . . . . . . . . . . . . . . . . . 21 $/\$
324	69, 323	mpan 676	. . . . . . . . . . . . . . . . . . . 20
325	68, 324	syl5eqbr 4436	. . . . . . . . . . . . . . . . . . 19
326	322, 325	nsyl 125	. . . . . . . . . . . . . . . . . 18 $/\$
327	312, 326	jca 535	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
328	96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64	ovolicc2lem2 22471	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
329	327, 328	syldan 473	. . . . . . . . . . . . . . . 16 $/\$
330	329	iftrued 3889	. . . . . . . . . . . . . . 15 $/\$
331		ffvelrn 6020	. . . . . . . . . . . . . . . . 17 $/\$
332	10, 240, 331	syl2an 480	. . . . . . . . . . . . . . . 16 $/\$
333	103	ralrimiva 2802	. . . . . . . . . . . . . . . . 17
334	333	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
335		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . 22
336	335	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . 21
337	336	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20
338	337	breq1d 4412	. . . . . . . . . . . . . . . . . . 19
339	338, 337	ifbieq1d 3904	. . . . . . . . . . . . . . . . . 18
340		fveq2 5865	. . . . . . . . . . . . . . . . . 18
341	339, 340	eleq12d 2523	. . . . . . . . . . . . . . . . 17
342	341	rspcv 3146	. . . . . . . . . . . . . . . 16
343	332, 334, 342	sylc 62	. . . . . . . . . . . . . . 15 $/\$
344	330, 343	eqeltrrd 2530	. . . . . . . . . . . . . 14 $/\$
345	5, 6, 7, 8, 9	algrp1 14533	. . . . . . . . . . . . . . 15 $/\$
346	240, 345	sylan2 477	. . . . . . . . . . . . . 14 $/\$
347	344, 346	eleqtrrd 2532	. . . . . . . . . . . . 13 $/\$
348	240, 285	sylan2 477	. . . . . . . . . . . . . 14 $/\$
349	96, 97, 98, 99, 100, 73, 101, 4, 102	ovolicc2lem1 22470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
350	348, 349	syldan 473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
351	347, 350	mpbid 214	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
352	351	simp2d 1021	. . . . . . . . . . 11 $/\$
353	290, 241, 352	ltled 9783	. . . . . . . . . 10 $/\$
354	239, 290, 241, 353	fsumle 13859	. . . . . . . . 9
355	242, 291	subge0d 10203	. . . . . . . . 9
356	354, 355	mpbird 236	. . . . . . . 8
357	242, 291	resubcld 10047	. . . . . . . . 9
358	205, 357	addge01d 10201	. . . . . . . 8
359	356, 358	mpbid 214	. . . . . . 7
360	158, 205, 296, 311, 359	letrd 9792	. . . . . 6
361	360, 295	breqtrrd 4429	. . . . 5
362	361	adantr 467	. . . 4 $/\$ $/\$
363		fzfid 12186	. . . . 5 $/\$ $/\$
364	170	adantlr 721	. . . . 5 $/\$ $/\$ $/\$
365	169	simprd 465	. . . . . 6 $/\$
366	365	adantlr 721	. . . . 5 $/\$ $/\$ $/\$
367	24	adantr 467	. . . . . . . . . . . 12 $/\$
368	367	sselda 3432	. . . . . . . . . . 11 $/\$ $/\$
369	368	nnred 10624	. . . . . . . . . 10 $/\$ $/\$
370	31	ad2antlr 733	. . . . . . . . . 10 $/\$ $/\$
371		ltle 9722	. . . . . . . . . 10 $/\$
372	369, 370, 371	syl2anc 667	. . . . . . . . 9 $/\$ $/\$
373	368, 5	syl6eleq 2539	. . . . . . . . . 10 $/\$ $/\$
374		nnz 10959	. . . . . . . . . . 11
375	374	ad2antlr 733	. . . . . . . . . 10 $/\$ $/\$
376		elfz5 11792	. . . . . . . . . 10 $/\$
377	373, 375, 376	syl2anc 667	. . . . . . . . 9 $/\$ $/\$
378	372, 377	sylibrd 238	. . . . . . . 8 $/\$ $/\$
379	378	ralimdva 2796	. . . . . . 7 $/\$
380	379	impr 625	. . . . . 6 $/\$ $/\$
381		dfss3 3422	. . . . . 6
382	380, 381	sylibr 216	. . . . 5 $/\$ $/\$
383	363, 364, 366, 382	fsumless 13856	. . . 4 $/\$ $/\$
384	185, 190, 172, 362, 383	letrd 9792	. . 3 $/\$ $/\$
385		eqidd 2452	. . . . . 6 $/\$ $/\$ $/\$
386		simprl 764	. . . . . . 7 $/\$ $/\$
387	386, 5	syl6eleq 2539	. . . . . 6 $/\$ $/\$
388	364	recnd 9669	. . . . . 6 $/\$ $/\$ $/\$
389	385, 387, 388	fsumser 13796	. . . . 5 $/\$ $/\$
390	99	fveq1i 5866	. . . . 5
391	389, 390	syl6eqr 2503	. . . 4 $/\$ $/\$
392	181	adantr 467	. . . . 5 $/\$ $/\$
393		ffn 5728	. . . . . . . 8
394	175, 393	syl 17	. . . . . . 7
395	394	adantr 467	. . . . . 6 $/\$ $/\$
396		fnfvelrn 6019	. . . . . 6 $/\$
397	395, 386, 396	syl2anc 667	. . . . 5 $/\$ $/\$
398		supxrub 11610	. . . . 5 $/\$
399	392, 397, 398	syl2anc 667	. . . 4 $/\$ $/\$
400	391, 399	eqbrtrd 4423	. . 3 $/\$ $/\$
401	160, 173, 184, 384, 400	xrletrd 11459	. 2 $/\$ $/\$
402	157, 401	rexlimddv 2883	1