geomcau - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
Unicode version

Theorem geomcau 15849

Description: If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy.

**Hypothesis**
Ref	Expression
geomcau.1

**Assertion**
Ref	Expression
geomcau	Met $/\$ $/\$ $/\$ $/\$ $/\$ Cau

Distinct variable groups:

**Proof of Theorem geomcau**
Step	Hyp	Ref	Expression
1		0re 6603	. . . . . . . . . 10
2	1	a1i 8	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$
3		geomcau.1	. . . . . . . . . . . . 13
4	3	metcl 9088	. . . . . . . . . . . 12 Met $/\$ $/\$
5	4	3expb 1068	. . . . . . . . . . 11 Met $/\$ $/\$
6		1nn 7117	. . . . . . . . . . . . 13
7		ffvelrn 4787	. . . . . . . . . . . . 13 $/\$
8	6, 7	mpan2 760	. . . . . . . . . . . 12
9		nnaddcl 7123	. . . . . . . . . . . . . 14 $/\$
10	6, 6, 9	mp2an 761	. . . . . . . . . . . . 13
11		ffvelrn 4787	. . . . . . . . . . . . 13 $/\$
12	10, 11	mpan2 760	. . . . . . . . . . . 12
13	8, 12	jca 310	. . . . . . . . . . 11 $/\$
14	5, 13	sylan2 500	. . . . . . . . . 10 Met $/\$
15	14	3ad2ant1 897	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$
16		axmulrcl 6427	. . . . . . . . . . . 12 $/\$
17		rpre 7236	. . . . . . . . . . . 12
18	16, 17	sylan2 500	. . . . . . . . . . 11 $/\$
19	18	3adant3 896	. . . . . . . . . 10 $/\$ $/\$
20	19	3ad2ant2 898	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$
21	3	metge0 9096	. . . . . . . . . . . 12 Met $/\$ $/\$
22	21	3expb 1068	. . . . . . . . . . 11 Met $/\$ $/\$
23	22, 13	sylan2 500	. . . . . . . . . 10 Met $/\$
24	23	3ad2ant1 897	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$
25		rpcn 7237	. . . . . . . . . . . . . . 15
26		exp1 7816	. . . . . . . . . . . . . . 15
27	25, 26	syl 12	. . . . . . . . . . . . . 14
28	27	3ad2ant2 898	. . . . . . . . . . . . 13 $/\$ $/\$
29	28	adantl 424	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$
30	29	opreq2d 4898	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$
31	30	breq2d 3350	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$
32	31	biimp3a 1194	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$
33	2, 15, 20, 24, 32	letrd 6696	. . . . . . . 8 Met $/\$ $/\$ $/\$ $/\$ $/\$
34		prodge02 7007	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
35	34	ancom2s 545	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
36	35	an4s 566	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
37		rpregt0 7242	. . . . . . . . . . . . 13 $/\$
38	36, 37	sylan2 500	. . . . . . . . . . . 12 $/\$ $/\$
39	38	an1rs 547	. . . . . . . . . . 11 $/\$ $/\$
40	39	ex 402	. . . . . . . . . 10 $/\$
41	40	3adant3 896	. . . . . . . . 9 $/\$ $/\$
42	41	3ad2ant2 898	. . . . . . . 8 Met $/\$ $/\$ $/\$ $/\$ $/\$
43	33, 42	mpd 29	. . . . . . 7 Met $/\$ $/\$ $/\$ $/\$ $/\$
44		fveq2 4681	. . . . . . . . . . 11
45		opreq1 4889	. . . . . . . . . . . 12
46	45	fveq2d 4685	. . . . . . . . . . 11
47	44, 46	opreq12d 4900	. . . . . . . . . 10
48		opreq2 4890	. . . . . . . . . . 11
49	48	opreq2d 4898	. . . . . . . . . 10
50	47, 49	breq12d 3351	. . . . . . . . 9
51	50	rcla4v 2376	. . . . . . . 8
52	6, 51	ax-mp 7	. . . . . . 7
53	43, 52	syl3an3 1132	. . . . . 6 Met $/\$ $/\$ $/\$ $/\$ $/\$
54	53	adantr 425	. . . . 5 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		leloe 6688	. . . . . . . . . 10 $/\$ $\/$
56	1, 55	mpan 759	. . . . . . . . 9 $\/$
57	56	3ad2ant1 897	. . . . . . . 8 $/\$ $/\$ $\/$
58	57	3ad2ant2 898	. . . . . . 7 Met $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
59	58	adantr 425	. . . . . 6 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
60		simplr 449	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
61		elrp 7233	. . . . . . . . . . . . . . . . 17 $/\$
62	61	biimpri 169	. . . . . . . . . . . . . . . 16 $/\$
63	62	3ad2antl1 1038	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64		elrp 7233	. . . . . . . . . . . . . . . . . . 19 $/\$
65		resubcl 6601	. . . . . . . . . . . . . . . . . . . . 21 $/\$
66		1re 6598	. . . . . . . . . . . . . . . . . . . . 21
67	65, 66, 17	sylancr 526	. . . . . . . . . . . . . . . . . . . 20
68	67	adantr 425	. . . . . . . . . . . . . . . . . . 19 $/\$
69		posdif 6843	. . . . . . . . . . . . . . . . . . . . 21 $/\$
70	69, 17, 66	sylancl 525	. . . . . . . . . . . . . . . . . . . 20
71	70	biimpa 460	. . . . . . . . . . . . . . . . . . 19 $/\$
72	64, 68, 71	sylanbrc 527	. . . . . . . . . . . . . . . . . 18 $/\$
73		rpreccl 7250	. . . . . . . . . . . . . . . . . 18
74	72, 73	syl 12	. . . . . . . . . . . . . . . . 17 $/\$
75	74	3adant1 894	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	75	adantr 425	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
77		rpmulcl 7248	. . . . . . . . . . . . . . 15 $/\$
78	63, 76, 77	syl11anc 524	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
79	78	adantlr 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
80		rpdivcl 7249	. . . . . . . . . . . . 13 $/\$
81	60, 79, 80	syl11anc 524	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
82		rpreccl 7250	. . . . . . . . . . . . . . 15
83		rpre 7236	. . . . . . . . . . . . . . 15
84	82, 83	syl 12	. . . . . . . . . . . . . 14
85	84	3ad2ant2 898	. . . . . . . . . . . . 13 $/\$ $/\$
86	85	ad2antrr 440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
87		reclt1 7081	. . . . . . . . . . . . . . . 16 $/\$
88	37, 87	syl 12	. . . . . . . . . . . . . . 15
89	88	biimpa 460	. . . . . . . . . . . . . 14 $/\$
90	89	3adant1 894	. . . . . . . . . . . . 13 $/\$ $/\$
91	90	ad2antrr 440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92		expnlbnd 7902	. . . . . . . . . . . 12 $/\$ $/\$
93	81, 86, 91, 92	syl111anc 1100	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94		rpcn 7237	. . . . . . . . . . . . . . . . . . . . 21
95	82, 94	syl 12	. . . . . . . . . . . . . . . . . . . 20
96	95	adantr 425	. . . . . . . . . . . . . . . . . . 19 $/\$
97		rpne0 7243	. . . . . . . . . . . . . . . . . . . . 21
98	82, 97	syl 12	. . . . . . . . . . . . . . . . . . . 20
99	98	adantr 425	. . . . . . . . . . . . . . . . . . 19 $/\$
100		nnnn0 7315	. . . . . . . . . . . . . . . . . . . 20
101	100	adantl 424	. . . . . . . . . . . . . . . . . . 19 $/\$
102		exprec 7837	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
103	96, 99, 101, 102	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eqcomd 1889	. . . . . . . . . . . . . . . . 17 $/\$
105	104	3ad2antl2 1039	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106	105	adantlr 429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
107	106	adantlr 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
108		rpne0 7243	. . . . . . . . . . . . . . . . . . 19
109		recrec 6952	. . . . . . . . . . . . . . . . . . 19 $/\$
110	25, 108, 109	syl11anc 524	. . . . . . . . . . . . . . . . . 18
111	110	3ad2ant2 898	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
112	111	adantr 425	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
113	112	ad2antrr 440	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
114	113	opreq1d 4897	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	107, 114	eqtrd 1925	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
116	115	breq1d 3348	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
117	116	rexbidva 2120	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
118	93, 117	mpbid 212	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
119		reexpcl 7823	. . . . . . . . . . . . . . . . 17 $/\$
120	119, 17, 100	syl2an 503	. . . . . . . . . . . . . . . 16 $/\$
121	120	3ad2antl2 1039	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	121	adantlr 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
123	122	adantlr 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
124		rpre 7236	. . . . . . . . . . . . . . 15
125	124	adantl 424	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
126	125	ad2antrr 440	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
127		remulcl 6457	. . . . . . . . . . . . . . . . . . 19 $/\$
128	17	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	66	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
130		simpr 350	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
131		ltne 6686	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
132	128, 129, 130, 131	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 $/\$
133		subeq0 6563	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
134		ax1cn 6422	. . . . . . . . . . . . . . . . . . . . . . . 24
135	133, 134, 25	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . 23
136	135	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
137	136	necon3bid 2035	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	132, 137	mpbird 213	. . . . . . . . . . . . . . . . . . . 20 $/\$
139		rereccl 6981	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	68, 138, 139	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 $/\$
141	127, 140	sylan2 500	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142	141	3impb 1063	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
143	142	adantr 425	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
144		simpl1 879	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145		simpr 350	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
146	140	3adant1 894	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
147	146	adantr 425	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
148		recgt0 7043	. . . . . . . . . . . . . . . . . . . 20 $/\$
149	68, 71, 148	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 $/\$
150	149	3adant1 894	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
151	150	adantr 425	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
152		mulgt0 6678	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
153	144, 145, 147, 151, 152	syl22anc 1101	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
154	143, 153	jca 310	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
155	154	adantlr 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
156	155	adantr 425	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157		ltmuldiv2 7047	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
158	123, 126, 156, 157	syl111anc 1100	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
159		recn 6466	. . . . . . . . . . . . . . . . 17
160	159	3ad2ant1 897	. . . . . . . . . . . . . . . 16 $/\$ $/\$
161	160	adantr 425	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162	161	ad2antrr 440	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
163	140	recnd 6468	. . . . . . . . . . . . . . . . 17 $/\$
164	163	3adant1 894	. . . . . . . . . . . . . . . 16 $/\$ $/\$
165	164	adantr 425	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
166	165	ad2antrr 440	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
167	120	recnd 6468	. . . . . . . . . . . . . . . . 17 $/\$
168	167	3ad2antl2 1039	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
169	168	adantlr 429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
170	169	adantlr 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
171		mul23 6580	. . . . . . . . . . . . . 14 $/\$ $/\$
172	162, 166, 170, 171	syl111anc 1100	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	breq1d 3348	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
174	158, 173	bitr3d 589	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
175	174	rexbidva 2120	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
176	118, 175	mpbid 212	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
177		opreq2 4890	. . . . . . . . . . . . . 14
178	177	opreq2d 4898	. . . . . . . . . . . . 13
179	178	opreq1d 4897	. . . . . . . . . . . 12
180	179	breq1d 3348	. . . . . . . . . . 11
181	180	rcla4ev 2381	. . . . . . . . . 10 $/\$
182		opreq1 4889	. . . . . . . . . . . . . . . . 17
183	182	eqcomd 1889	. . . . . . . . . . . . . . . 16
184		expcl 7824	. . . . . . . . . . . . . . . . . . . 20 $/\$
185		1nn0 7323	. . . . . . . . . . . . . . . . . . . 20
186	184, 25, 185	sylancl 525	. . . . . . . . . . . . . . . . . . 19
187	186	adantr 425	. . . . . . . . . . . . . . . . . 18 $/\$
188		mul02 6607	. . . . . . . . . . . . . . . . . 18
189	187, 188	syl 12	. . . . . . . . . . . . . . . . 17 $/\$
190	189	3adant1 894	. . . . . . . . . . . . . . . 16 $/\$ $/\$
191	183, 190	sylan9eqr 1951	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
192	191	opreq1d 4897	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
193		mul02 6607	. . . . . . . . . . . . . . . . 17
194	163, 193	syl 12	. . . . . . . . . . . . . . . 16 $/\$
195	194	3adant1 894	. . . . . . . . . . . . . . 15 $/\$ $/\$
196	195	adantr 425	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	192, 196	eqtrd 1925	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
198	197	adantrl 430	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
199		rpgt0 7240	. . . . . . . . . . . . 13
200	199	ad2antrl 442	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
201	198, 200	eqbrtrd 3357	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
202	201	anassrs 489	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
203	181, 6, 202	sylancr 526	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
204	176, 203	jaodan 471	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$
205	204	ex 402	. . . . . . 7 $/\$ $/\$ $/\$ $\/$
206	205	3ad2antl2 1039	. . . . . 6 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
207	59, 206	sylbid 220	. . . . 5 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
208	54, 207	mpd 29	. . . 4 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209		leloe 6688	. . . . . . . . . . . . . 14 $/\$ $\/$
210	209	biimpd 170	. . . . . . . . . . . . 13 $/\$ $\/$
211		nnre 7112	. . . . . . . . . . . . 13
212		nnre 7112	. . . . . . . . . . . . 13
213	210, 211, 212	syl2an 503	. . . . . . . . . . . 12 $/\$ $\/$
214	213	adantl 424	. . . . . . . . . . 11 $/\$ $/\$ $\/$
215	214	ad2antlr 441	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
216		nnltp1le 7139	. . . . . . . . . . . . . . 15 $/\$
217		eluz 7595	. . . . . . . . . . . . . . . 16 $/\$
218		nnz 7362	. . . . . . . . . . . . . . . . 17
219	218	peano2zdi 7376	. . . . . . . . . . . . . . . 16
220		nnz 7362	. . . . . . . . . . . . . . . 16
221	217, 219, 220	syl2an 503	. . . . . . . . . . . . . . 15 $/\$
222	216, 221	bitr4d 590	. . . . . . . . . . . . . 14 $/\$
223	222	adantl 424	. . . . . . . . . . . . 13 $/\$ $/\$
224	223	ad2antlr 441	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225	3	metcl 9088	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$
226	225	3expb 1068	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$
227		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
228	227	ex 402	. . . . . . . . . . . . . . . . . . . . 21
229		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
230	229	ex 402	. . . . . . . . . . . . . . . . . . . . 21
231	228, 230	anim12d 617	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
232	231	imp 377	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
233	226, 232	sylan2 500	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$ $/\$
234	233	anassrs 489	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$
235	234	3ad2antl1 1038	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
236	235	adantrl 430	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
237	236	ad2antrr 440	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
238		remulcl 6457	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
239	238, 120	sylan2 500	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
240	239	anassrs 489	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
241	240	3adantl3 1034	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
242	146	adantr 425	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
243		remulcl 6457	. . . . . . . . . . . . . . . . . . 19 $/\$
244	241, 242, 243	syl11anc 524	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
245	244	adantrr 431	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
246	245	3ad2antl2 1039	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
247	246	adantrl 430	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248	247	ad2antrr 440	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249	124	ad2antrl 442	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
250	249	ad2antrr 440	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
251	236	adantr 425	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		1z 7368	. . . . . . . . . . . . . . . . . . . . . 22
253		eluzsub 15783	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
254	253, 218	syl3an1 1130	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
255	252, 254	mp3an2 1179	. . . . . . . . . . . . . . . . . . . . 21 $/\$
256	255	adantlr 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
257	256	adantl 424	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
258	3	metcl 9088	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Met $/\$ $/\$
259	258	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$ $/\$
260		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
261		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
262		peano2nn 7118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
263	261, 262	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
264	260, 263	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
265	259, 264	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$
266	265	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$
267		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
268		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
269		uzss 7600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
270	268, 269	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
271	267, 270	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
272		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
273	271, 272	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
274		elfzuz 7658	. . . . . . . . . . . . . . . . . . . . . . . . . 26
275	273, 274	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
276	266, 275	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$
277	276	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
278	277	anassrs 489	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
279	278	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
280	279	adantrr 431	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
281	280	adantrr 431	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
282		fsumrecl 8277	. . . . . . . . . . . . . . . . . . 19 $/\$
283	257, 281, 282	syl11anc 524	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
284	283	anassrs 489	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
285	284	adantlrl 434	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
286	247	adantr 425	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
287		simpll1 915	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Met $/\$
288	218	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
289		simpr 350	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
290		fzssuz 7677	. . . . . . . . . . . . . . . . . . . . . . 23
291	290	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22
292		nnuz 7608	. . . . . . . . . . . . . . . . . . . . . . 23
293	270, 292	syl6ssr 2664	. . . . . . . . . . . . . . . . . . . . . 22
294	291, 293	sstrd 2627	. . . . . . . . . . . . . . . . . . . . 21
295	294	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
296	288, 289, 295	3jca 1050	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
297	296	adantll 428	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
298	297	adantll 428	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
299		nnex 7116	. . . . . . . . . . . . . . . . . 18
300	3, 299	mettrifi2 15848	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$ $/\$
301	287, 298, 300	syl11anc 524	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
302		remulcl 6457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
303		reexpcl 7823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
304	303, 17	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
305	302, 304	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
306	305	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
307		nnnn0 7315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
308	273, 307	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
309	308, 274	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
310	306, 309	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
311	310	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
312	311	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
313	312	3adantl3 1034	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
314	313	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
315	314	adantrr 431	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	315	adantrr 431	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
317		fsumrecl 8277	. . . . . . . . . . . . . . . . . . . 20 $/\$
318	257, 316, 317	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
319	245	adantrr 431	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
320	319	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
321		fzssuz 7677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
322	321	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
323	322, 293	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
324	323	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
325	324	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
326	325	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
327	265	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$
328	327	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$
329	328	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
330	326, 329	syld 30	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
331	330	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
332	303, 17, 307	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
333	302, 332	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
334	333	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
335	334	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
336	335	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$
337	336	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
338	326, 337	syld 30	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
339	338	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
340		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
341		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
342	341	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
343	340, 342	opreq12d 4900	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
344		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
345	344	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
346	343, 345	breq12d 3351	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
347	346	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . . . 26
348	347	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$
349	348	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
350	326, 349	syld 30	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
351	350	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
352	331, 339, 351	3jca 1050	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
353	352	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
354		fsumcmp 8300	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
355	257, 353, 354	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
356	288	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
357		remulcl 6457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
358		reexpcl 7823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
359	358, 17	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
360	357, 359	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
361	360	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
362		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
363	362, 270	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
364		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
365	363, 364	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
366		nnnn0 7315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
367	365, 366	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
368	361, 367	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
369	368	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
370	369	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
371	370	3adantl3 1034	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
372	371	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
373	372	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
374	373	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
375		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
376	375	fopab2 4796	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
377	374, 376	sylib 215	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
378		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
379	378	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$ $/\$ $/\$ $/\$ $/\$
380	379	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
381	53	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
382	304	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
383	382	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
384	383, 308	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
385	384	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
386		rpexpcl 7825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
387		rpge0 7241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
388	386, 387	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
389	388	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
390	389	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
391	390, 308	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
392	391	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
393		mulge0 6868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
394	380, 381, 385, 392, 393	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
395		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
396	395	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
397		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
398	396, 375, 397	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
399	398	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
400	394, 399	breqtrrd 3363	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
401	400	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
402	401	adantrr 431	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
403	402	adantrr 431	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
404		nncn 7113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
405		addid2 6482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
406	404, 405	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
407	406	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
408	407	opeq1d 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
409	408	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
410	25	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
411		rpge0 7241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
412		absid 8113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
413	17, 411, 412	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
414	413	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
415	414, 130	eqbrtrd 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
416		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
417	416	geolim 8499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
418	410, 415, 417	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
419		addex 6470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
420		nn0ex 7314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
421	420	opabex2 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
422	419, 421	seq0seqz 7785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
423	418, 422	syl5eqbrr 3371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
424	423	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
425	424	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
426		0z 7355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
427	426	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
428	241	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
429		elnn0uz 7610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
430		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
431		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
432	430, 416, 431	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
433	429, 432	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
434	433	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
435		expcl 7824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
436	429	biimpri 169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
437	435, 25, 436	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
438	434, 437	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
439	438	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
440	439	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
441	430	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
442		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
443		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
444	441, 442, 443	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
445	432	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
446	444, 445	eqtr4d 1928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
447	429, 446	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
448	447	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
449	440, 448	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
450	449	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
451		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
452	420	opabex2 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
453	451, 421, 452	iserzmulc1 8396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
454	427, 428, 450, 453	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
455	425, 454	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
456		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
457	456	opabex2 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
458	457	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
459	458, 452	jctil 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
460	218	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
461	460, 426	jctil 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
462	429, 444	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
463	462	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
464	160	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
465		mulcl 6456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
466	464, 168, 465	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
467	466	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
468	437	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
469	468	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
470		mulcl 6456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
471	467, 469, 470	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
472	463, 471	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
473		addcom 6458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
474		eluzelz 7592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
475		zcn 7349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
476	474, 475	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
477	473, 476, 404	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
478	477	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
479	478	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
480	479	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
481	25	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
482	481	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
483	100	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
484	436	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
485		expadd 7839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
486	482, 483, 484, 485	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
487	480, 486	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
488	487	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
489	160	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
490	168	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
491		mulass 6461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
492	491	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
493	489, 490, 469, 492	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
494	488, 493	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
495		eluzadd 15782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
496	495, 218	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
497	496	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
498	406	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
499	498	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
500	497, 499	eleqtrd 1973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
501		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
502	501	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
503		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
504	502, 375, 503	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
505	500, 504	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
506	505	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
507	494, 506, 463	3eqtr4d 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
508	472, 507	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
509	508	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
510		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
511	509, 510	jctil 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
512		iserzshft2 15829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
513	459, 461, 511, 512	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
514	455, 513	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
515	409, 514	eqbrtrrd 3359	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
516	515	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
517	516	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
518	517	adantrr 431	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
519		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
520	510, 519	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
521	518, 520	syl 12	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
522		fsumleisum 15827	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
523	356, 257, 377, 403, 521, 522	syl23anc 1107	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
524	274, 398	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
525	524	sumeq2i 8248	. . . . . . . . . . . . . . . . . . . . 21 $/\$
526	525	a1i 8	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
527	406	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
528	527	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
529	528	sumeq1d 8250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
530	529	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
531	457	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
532	218	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
533	426	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
534		isumshft2 15830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
535	531, 532, 533, 534	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
536	530, 535	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
537	536	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
538	537	ad2ant2lr 446	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
539	538	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
540		expadd 7839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
541		elnn0uz 7610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
542	541	biimpri 169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
543	540, 25, 100, 542	syl3an 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
544	543	3expa 1067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
545	544	adantlll 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
546	545	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
547		eluzadd 15782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
548	547, 218	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
549	548	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
550		addcom 6458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
551		eluzelz 7592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
552		zcn 7349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
553	551, 552	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
554	550, 553, 404	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
555	554	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
556	406	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
557	556	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
558	555, 557	eleq12d 1965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
559	549, 558	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
560		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
561	560	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
562		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
563	561, 375, 562	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
564	559, 563	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
565	564	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
566	159	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
567	566	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
568	167	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
569	568	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
570	303, 17, 542	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
571	570	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
572	571	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
573	572	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
574		mulass 6461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
575	567, 569, 573, 574	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
576	546, 565, 575	3eqtr4d 1937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
577	576	sumeq2dv 8252	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
578	577	3adantl3 1034	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
579	578	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
580	579	adantrr 431	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
581	580	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
582		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
583		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
584	395, 582, 583	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
585	584	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
586	585, 571	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
587	586	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
588	587	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
589	588	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
590		elnn0uz 7610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
591	590	bicomi 189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
592	591	anbi1i 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
593	592	opabbii 3402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
594	593	geolim 8499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
595	410, 415, 594	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
596		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
597	596	opabex2 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
598	419, 597	seq0seqz 7785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
599	595, 598	syl5eqbrr 3371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
600		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
601	451, 600	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
602	599, 601	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
603	602	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
604	603	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
605	597	isummulc1 8473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
606	427, 428, 589, 604, 605	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
607	584	sumeq2i 8248	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
608	607	opreq2i 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
609	584	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
610	609	sumeq2i 8248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
611	606, 608, 610	3eqtr3g 1952	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
612		nn0uz 7607	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
613	612	sumeq1i 8247	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
614	613	opreq2i 4893	. . . . . . . . . . . . . . . . . . . . . . . . . 26
615	611, 614	syl5req 1941	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
616	615	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
617	616	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
618	617	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
619	481	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$ $/\$ $/\$ $/\$ $/\$
620	619	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
621	17	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
622	621	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Met $/\$ $/\$ $/\$ $/\$ $/\$
623	411	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
624	623	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Met $/\$ $/\$ $/\$ $/\$ $/\$
625	622, 624, 412	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Met $/\$ $/\$ $/\$ $/\$ $/\$
626		simp3 878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
627	626	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Met $/\$ $/\$ $/\$ $/\$ $/\$
628	625, 627	eqbrtrd 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$ $/\$ $/\$ $/\$ $/\$
629	628	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
630		geoisum 8504	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
631	620, 629, 630	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . 25 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
632	631	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . 24 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
633	632	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
634	633	adantrr 431	. . . . . . . . . . . . . . . . . . . . . 22 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
635	618, 634	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . 21 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
636	539, 581, 635	3eqtrd 1929	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
637	523, 526, 636	3brtr3d 3366	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
638	283, 318, 320, 355, 637	letrd 6696	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
639	638	anassrs 489	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
640	639	adantlrl 434	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
641	251, 285, 286, 301, 640	letrd 6696	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
642	641	adantlr 429	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
643		simplr 449	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
644	237, 248, 250, 642, 643	lelttrd 6697	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
645	644	ex 402	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
646	224, 645	sylbid 220	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
647		fveq2 4681	. . . . . . . . . . . . . . . 16
648	647	opreq2d 4898	. . . . . . . . . . . . . . 15
649	648	breq1d 3348	. . . . . . . . . . . . . 14
650	3	met0 9092	. . . . . . . . . . . . . . . . . . 19 Met $/\$
651	650	adantlr 429	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$
652	199	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$
653	651, 652	eqbrtrd 3357	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$
654	653, 227	sylan2 500	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$
655	654	an4s 566	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$
656	655	adantrrr 439	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$
657	649, 656	syl5cbi 226	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$
658	657	3ad2antl1 1038	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
659	658	adantr 425	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
660	646, 659	jaod 469	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
661	215, 660	syld 30	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
662	661	ex 402	. . . . . . . 8 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
663	662	anassrs 489	. . . . . . 7 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
664	663	anassrs 489	. . . . . 6 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
665	664	r19.21adva 2182	. . . . 5 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
666	665	reximdva 2203	. . . 4 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
667	208, 666	mpd 29	. . 3 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
668	667	r19.21aiva 2176	. 2 Met $/\$ $/\$ $/\$ $/\$ $/\$
669	3	iscau5 9219	. . 3 Met $/\$ Cau
670	669	3ad2ant1 897	. 2 Met $/\$ $/\$ $/\$ $/\$ $/\$ Cau
671	668, 670	mpbird 213	1 Met $/\$ $/\$ $/\$ $/\$ $/\$ Cau

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wex 1326

wne 2017

wral 2105

wrex 2106

cvv 2292

wss 2593

cop 3046 class class class wbr 3338

copab 3395

cdm 3986

wf 3994

cfv 3998 (class class class)co 4884

cc 6384

cr 6385

cc0 6386

c1 6387

caddc 6389

cmul 6391

cmin 6445

cdiv 6447

cle 6448

cn 6449

cn0 6450

cz 6451

crp 6453

clt 6653

cuz 7586

cfz 7637

cseqz 7774

cseq0 7775

cexp 7811

cabs 8000

cli 8234

csu 8239 Metcme 9066 Caucca 9198

This theorem is referenced by: heiborlem33 15987 bfplem7 16004

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-5 1302 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 df-sup 5664 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-lt 6399 df-sub 6511 df-neg 6513 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657 df-le 6658 df-div 6892 df-n 7108 df-2 7154 df-rp 7232 df-n0 7309 df-z 7345 df-fl 7463 df-uz 7587 df-fz 7638 df-seq1 7721 df-shft 7754 df-seqz 7776 df-seq0 7777 df-exp 7812 df-sqr 7920 df-re 8001 df-im 8002 df-cj 8003 df-abs 8004 df-clim 8235 df-sum 8240 df-met 9070 df-cau 9201