axlowdimlem16 - Metamath Proof Explorer

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

Theorem axlowdimlem16 23203

Description: Lemma for axlowdim 23207. Set up a summation that will help establish distance. (Contributed by Scott Fenton, 21-Apr-2013.)

**Hypotheses**
Ref	Expression
axlowdimlem16.1	$\$
axlowdimlem16.2	$\$

**Assertion**
Ref	Expression
axlowdimlem16	$/\$

Distinct variable groups:

**Proof of Theorem axlowdimlem16**
Step	Hyp	Ref	Expression
1		elfz1eq 11462	. . . . . 6
2		oveq1 6098	. . . . . . . . . . 11
3		df-3 10381	. . . . . . . . . . 11
4	2, 3	syl6reqr 2494	. . . . . . . . . 10
5	4, 4	oveq12d 6109	. . . . . . . . 9
6	5	sumeq1d 13178	. . . . . . . 8
7	2, 3	syl6eqr 2493	. . . . . . . . . 10
8		3z 10679	. . . . . . . . . 10
9	7, 8	syl6eqel 2531	. . . . . . . . 9
10		ax-1cn 9340	. . . . . . . . . 10
11	10	sqcli 11946	. . . . . . . . 9
12		fveq2 5691	. . . . . . . . . . . 12
13		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
14	13	axlowdimlem11 23198	. . . . . . . . . . . 12
15	12, 14	syl6eq 2491	. . . . . . . . . . 11
16	15	oveq1d 6106	. . . . . . . . . 10
17	16	fsum1 13218	. . . . . . . . 9 $/\$
18	9, 11, 17	sylancl 662	. . . . . . . 8
19	6, 18	eqtrd 2475	. . . . . . 7
20		fveq2 5691	. . . . . . . . . . . 12
21		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
22	21	axlowdimlem8 23195	. . . . . . . . . . . 12
23	20, 22	syl6eq 2491	. . . . . . . . . . 11
24	23	oveq1d 6106	. . . . . . . . . 10
25		sqneg 11926	. . . . . . . . . . 11
26	10, 25	ax-mp 5	. . . . . . . . . 10
27	24, 26	syl6eq 2491	. . . . . . . . 9
28	27	fsum1 13218	. . . . . . . 8 $/\$
29	8, 11, 28	mp2an 672	. . . . . . 7
30	19, 29	syl6reqr 2494	. . . . . 6
31	1, 30	syl 16	. . . . 5
32	31	a1i 11	. . . 4
33		oveq1 6098	. . . . . . 7
34		3m1e2 10438	. . . . . . 7
35	33, 34	syl6eq 2491	. . . . . 6
36	35	oveq2d 6107	. . . . 5
37	36	eleq2d 2510	. . . 4
38		oveq2 6099	. . . . . 6
39	38	sumeq1d 13178	. . . . 5
40	38	sumeq1d 13178	. . . . 5
41	39, 40	eqeq12d 2457	. . . 4
42	32, 37, 41	3imtr4d 268	. . 3
43	42	adantld 467	. 2 $/\$
44		simprl 755	. . . 4 $/\$ $/\$
45		eluzle 10873	. . . . . . 7
46	45	adantl 466	. . . . . 6 $/\$
47		simpl 457	. . . . . 6 $/\$
48		3re 10395	. . . . . . 7
49		eluzelre 10871	. . . . . . . 8
50	49	adantl 466	. . . . . . 7 $/\$
51		ltlen 9476	. . . . . . 7 $/\$ $/\$
52	48, 50, 51	sylancr 663	. . . . . 6 $/\$ $/\$
53	46, 47, 52	mpbir2and 913	. . . . 5 $/\$
54	53	adantrr 716	. . . 4 $/\$ $/\$
55		simprr 756	. . . 4 $/\$ $/\$
56		fzssp1 11501	. . . . . . . . . . . . 13
57		simp3 990	. . . . . . . . . . . . 13 $/\$ $/\$
58	56, 57	sseldi 3354	. . . . . . . . . . . 12 $/\$ $/\$
59		eluzelz 10870	. . . . . . . . . . . . . . . 16
60	59	3ad2ant1 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	60	zcnd 10748	. . . . . . . . . . . . . 14 $/\$ $/\$
62		npcan 9619	. . . . . . . . . . . . . 14 $/\$
63	61, 10, 62	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	oveq2d 6107	. . . . . . . . . . . 12 $/\$ $/\$
65	58, 64	eleqtrd 2519	. . . . . . . . . . 11 $/\$ $/\$
66		elfzelz 11453	. . . . . . . . . . 11
67	65, 66	syl 16	. . . . . . . . . 10 $/\$ $/\$
68	67	zred 10747	. . . . . . . . 9 $/\$ $/\$
69	68	ltp1d 10263	. . . . . . . 8 $/\$ $/\$
70		fzdisj 11476	. . . . . . . 8
71	69, 70	syl 16	. . . . . . 7 $/\$ $/\$
72		fzsplit 11475	. . . . . . . 8
73	65, 72	syl 16	. . . . . . 7 $/\$ $/\$
74		fzfid 11795	. . . . . . 7 $/\$ $/\$
75		3nn 10480	. . . . . . . . . . . . 13
76		uznnssnn 10902	. . . . . . . . . . . . 13
77	75, 76	ax-mp 5	. . . . . . . . . . . 12
78	77	sseli 3352	. . . . . . . . . . 11
79		2nn 10479	. . . . . . . . . . . . . 14
80		nnuz 10896	. . . . . . . . . . . . . 14
81	79, 80	eleqtri 2515	. . . . . . . . . . . . 13
82		fzss1 11497	. . . . . . . . . . . . 13
83	81, 82	ax-mp 5	. . . . . . . . . . . 12
84	83	sseli 3352	. . . . . . . . . . 11
85	13	axlowdimlem10 23197	. . . . . . . . . . 11 $/\$
86	78, 84, 85	syl2an 477	. . . . . . . . . 10 $/\$
87		fzss1 11497	. . . . . . . . . . . 12
88	81, 87	ax-mp 5	. . . . . . . . . . 11
89	88	sseli 3352	. . . . . . . . . 10
90		fveecn 23148	. . . . . . . . . 10 $/\$
91	86, 89, 90	syl2an 477	. . . . . . . . 9 $/\$ $/\$
92	91	sqcld 12006	. . . . . . . 8 $/\$ $/\$
93	92	3adantl2 1145	. . . . . . 7 $/\$ $/\$ $/\$
94	71, 73, 74, 93	fsumsplit 13216	. . . . . 6 $/\$ $/\$
95		fzss1 11497	. . . . . . . . . . . . . . . 16
96	81, 95	ax-mp 5	. . . . . . . . . . . . . . 15
97	96	sseli 3352	. . . . . . . . . . . . . 14
98		elfzelz 11453	. . . . . . . . . . . . . . . . . . . 20
99	98	zred 10747	. . . . . . . . . . . . . . . . . . 19
100	99	3ad2ant3 1011	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
101	49	3ad2ant1 1009	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102		peano2rem 9675	. . . . . . . . . . . . . . . . . . . 20
103	101, 102	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104		elfzle2 11455	. . . . . . . . . . . . . . . . . . . 20
105	104	3ad2ant3 1011	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
106	101	ltm1d 10265	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
107	100, 103, 101, 105, 106	lelttrd 9529	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
108	100, 101, 107	ltled 9522	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
109	98	3ad2ant3 1011	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
110		eluz 10874	. . . . . . . . . . . . . . . . . 18 $/\$
111	109, 60, 110	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
112	108, 111	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113		fzss2 11498	. . . . . . . . . . . . . . . 16
114	112, 113	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	114	sseld 3355	. . . . . . . . . . . . . 14 $/\$ $/\$
116	97, 115	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	imp 429	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		elfzelz 11453	. . . . . . . . . . . . . . 15
119	118	zred 10747	. . . . . . . . . . . . . 14
120	119	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	100	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
122		peano2re 9542	. . . . . . . . . . . . . . . . 17
123	99, 122	syl 16	. . . . . . . . . . . . . . . 16
124	123	3ad2ant3 1011	. . . . . . . . . . . . . . 15 $/\$ $/\$
125	124	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
126		elfzle2 11455	. . . . . . . . . . . . . . 15
127	126	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
128	121	ltp1d 10263	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
129	120, 121, 125, 127, 128	lelttrd 9529	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	120, 129	ltned 9510	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	13	axlowdimlem12 23199	. . . . . . . . . . . 12 $/\$
132	117, 130, 131	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
133	132	sq0id 11959	. . . . . . . . . 10 $/\$ $/\$ $/\$
134	133	sumeq2dv 13180	. . . . . . . . 9 $/\$ $/\$
135		fzfi 11794	. . . . . . . . . . 11
136	135	olci 391	. . . . . . . . . 10 $\/$
137		sumz 13199	. . . . . . . . . 10 $\/$
138	136, 137	ax-mp 5	. . . . . . . . 9
139	134, 138	syl6eq 2491	. . . . . . . 8 $/\$ $/\$
140	109	peano2zd 10750	. . . . . . . . . . 11 $/\$ $/\$
141		sq1 11960	. . . . . . . . . . . . 13
142	16, 141	syl6eq 2491	. . . . . . . . . . . 12
143	142	fsum1 13218	. . . . . . . . . . 11 $/\$
144	140, 10, 143	sylancl 662	. . . . . . . . . 10 $/\$ $/\$
145		oveq2 6099	. . . . . . . . . . . 12
146	145	sumeq1d 13178	. . . . . . . . . . 11
147	146	eqeq1d 2451	. . . . . . . . . 10
148	144, 147	syl5ib 219	. . . . . . . . 9 $/\$ $/\$
149	109	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
150	149	zred 10747	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	60	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
152	151	zred 10747	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
153	152, 102	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
154	105	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
155	152	ltm1d 10265	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
156	150, 153, 152, 154, 155	lelttrd 9529	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
157		1re 9385	. . . . . . . . . . . . . . . . . . . 20
158	157	a1i 11	. . . . . . . . . . . . . . . . . . 19
159		2re 10391	. . . . . . . . . . . . . . . . . . . 20
160	159	a1i 11	. . . . . . . . . . . . . . . . . . 19
161		1le2 10535	. . . . . . . . . . . . . . . . . . . 20
162	161	a1i 11	. . . . . . . . . . . . . . . . . . 19
163		elfzle1 11454	. . . . . . . . . . . . . . . . . . 19
164	158, 160, 99, 162, 163	letrd 9528	. . . . . . . . . . . . . . . . . 18
165	164	3ad2ant3 1011	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	165	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
167		elnnz1 10672	. . . . . . . . . . . . . . . 16 $/\$
168	149, 166, 167	sylanbrc 664	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
169	78	3ad2ant1 1009	. . . . . . . . . . . . . . . 16 $/\$ $/\$
170	169	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
171		nnltp1le 10700	. . . . . . . . . . . . . . 15 $/\$
172	168, 170, 171	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
173	156, 172	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
174	140	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175		eluz 10874	. . . . . . . . . . . . . 14 $/\$
176	174, 151, 175	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
177	173, 176	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
178		simpr1 994	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
179		simpr3 996	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180	178, 179, 86	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	180	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	168	peano2nnd 10339	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
183	182, 80	syl6eleq 2533	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
184		fzss1 11497	. . . . . . . . . . . . . . . 16
185	183, 184	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
186	185	sselda 3356	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	181, 186, 90	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
188	187	sqcld 12006	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
189	12	oveq1d 6106	. . . . . . . . . . . . 13
190	14	oveq1i 6101	. . . . . . . . . . . . . 14
191	190, 141	eqtri 2463	. . . . . . . . . . . . 13
192	189, 191	syl6eq 2491	. . . . . . . . . . . 12
193	177, 188, 192	fsum1p 13222	. . . . . . . . . . 11 $/\$ $/\$ $/\$
194	182	peano2nnd 10339	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
195	194, 80	syl6eleq 2533	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196		fzss1 11497	. . . . . . . . . . . . . . . . . . 19
197	195, 196	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
198	197	sselda 3356	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
199	150, 122	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
200	199	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
201		peano2re 9542	. . . . . . . . . . . . . . . . . . . 20
202	200, 201	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
203		elfzelz 11453	. . . . . . . . . . . . . . . . . . . . 21
204	203	zred 10747	. . . . . . . . . . . . . . . . . . . 20
205	204	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
206	200	ltp1d 10263	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
207		elfzle1 11454	. . . . . . . . . . . . . . . . . . . 20
208	207	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
209	200, 202, 205, 206, 208	ltletrd 9531	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
210	200, 209	gtned 9509	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
211	198, 210, 131	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
212	211	sq0id 11959	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
213	212	sumeq2dv 13180	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
214		fzfi 11794	. . . . . . . . . . . . . . . 16
215	214	olci 391	. . . . . . . . . . . . . . 15 $\/$
216		sumz 13199	. . . . . . . . . . . . . . 15 $\/$
217	215, 216	ax-mp 5	. . . . . . . . . . . . . 14
218	213, 217	syl6eq 2491	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
219	218	oveq2d 6107	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
220		1p0e1 10434	. . . . . . . . . . . 12
221	219, 220	syl6eq 2491	. . . . . . . . . . 11 $/\$ $/\$ $/\$
222	193, 221	eqtrd 2475	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	222	ex 434	. . . . . . . . 9 $/\$ $/\$
224	148, 223	pm2.61ine 2687	. . . . . . . 8 $/\$ $/\$
225	139, 224	oveq12d 6109	. . . . . . 7 $/\$ $/\$
226		0p1e1 10433	. . . . . . 7
227	225, 226	syl6eq 2491	. . . . . 6 $/\$ $/\$
228	94, 227	eqtrd 2475	. . . . 5 $/\$ $/\$
229		simp1 988	. . . . . . . 8 $/\$ $/\$
230		2lt3 10489	. . . . . . . . . 10
231	159, 48, 230	ltleii 9497	. . . . . . . . 9
232		2z 10678	. . . . . . . . . 10
233	232	eluz1i 10868	. . . . . . . . 9 $/\$
234	8, 231, 233	mpbir2an 911	. . . . . . . 8
235		uztrn 10877	. . . . . . . 8 $/\$
236	229, 234, 235	sylancl 662	. . . . . . 7 $/\$ $/\$
237		fveq2 5691	. . . . . . . 8
238	237	oveq1d 6106	. . . . . . 7
239	236, 93, 238	fsum1p 13222	. . . . . 6 $/\$ $/\$
240	59	adantr 465	. . . . . . . . . . . . . . 15 $/\$
241	240	zred 10747	. . . . . . . . . . . . . 14 $/\$
242		lttr 9451	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
243	159, 48, 242	mp3an12 1304	. . . . . . . . . . . . . . . . 17 $/\$
244	230, 243	mpani 676	. . . . . . . . . . . . . . . 16
245	49, 244	syl 16	. . . . . . . . . . . . . . 15
246	245	imp 429	. . . . . . . . . . . . . 14 $/\$
247		ltle 9463	. . . . . . . . . . . . . . 15 $/\$
248	159, 247	mpan 670	. . . . . . . . . . . . . 14
249	241, 246, 248	sylc 60	. . . . . . . . . . . . 13 $/\$
250	249, 161	jctil 537	. . . . . . . . . . . 12 $/\$ $/\$
251		1z 10676	. . . . . . . . . . . . . 14
252		elfz 11443	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
253	232, 251, 252	mp3an12 1304	. . . . . . . . . . . . 13 $/\$
254	240, 253	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
255	250, 254	mpbird 232	. . . . . . . . . . 11 $/\$
256	255	3adant3 1008	. . . . . . . . . 10 $/\$ $/\$
257	99	ltp1d 10263	. . . . . . . . . . . . . 14
258	160, 99, 123, 163, 257	lelttrd 9529	. . . . . . . . . . . . 13
259	258	3ad2ant3 1011	. . . . . . . . . . . 12 $/\$ $/\$
260		ltne 9471	. . . . . . . . . . . 12 $/\$
261	159, 259, 260	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$
262	261	necomd 2695	. . . . . . . . . 10 $/\$ $/\$
263	13	axlowdimlem12 23199	. . . . . . . . . 10 $/\$
264	256, 262, 263	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
265	264	sq0id 11959	. . . . . . . 8 $/\$ $/\$
266	265	oveq1d 6106	. . . . . . 7 $/\$ $/\$
267	3	oveq1i 6101	. . . . . . . . 9
268	267	sumeq1i 13175	. . . . . . . 8
269	268	oveq2i 6102	. . . . . . 7
270	266, 269	syl6eqr 2493	. . . . . 6 $/\$ $/\$
271		fzfid 11795	. . . . . . . 8 $/\$ $/\$
272	75, 80	eleqtri 2515	. . . . . . . . . . . . 13
273		fzss1 11497	. . . . . . . . . . . . 13
274	272, 273	ax-mp 5	. . . . . . . . . . . 12
275	274	sseli 3352	. . . . . . . . . . 11
276	86, 275, 90	syl2an 477	. . . . . . . . . 10 $/\$ $/\$
277	276	sqcld 12006	. . . . . . . . 9 $/\$ $/\$
278	277	3adantl2 1145	. . . . . . . 8 $/\$ $/\$ $/\$
279	271, 278	fsumcl 13210	. . . . . . 7 $/\$ $/\$
280	279	addid2d 9570	. . . . . 6 $/\$ $/\$
281	239, 270, 280	3eqtrrd 2480	. . . . 5 $/\$ $/\$
282		simpl 457	. . . . . . . . 9 $/\$
283	21	axlowdimlem7 23194	. . . . . . . . . . . 12
284	283	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
285	275	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
286		fveecn 23148	. . . . . . . . . . 11 $/\$
287	284, 285, 286	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$
288	287	sqcld 12006	. . . . . . . . 9 $/\$ $/\$
289		neg1sqe1 11961	. . . . . . . . . 10
290	24, 289	syl6eq 2491	. . . . . . . . 9
291	282, 288, 290	fsum1p 13222	. . . . . . . 8 $/\$
292		zaddcl 10685	. . . . . . . . . . . . . . . . . . . 20 $/\$
293	8, 251, 292	mp2an 672	. . . . . . . . . . . . . . . . . . 19
294	293	zrei 10652	. . . . . . . . . . . . . . . . . 18
295		1lt3 10490	. . . . . . . . . . . . . . . . . . 19
296	48	ltp1i 10236	. . . . . . . . . . . . . . . . . . 19
297	157, 48, 294	lttri 9500	. . . . . . . . . . . . . . . . . . 19 $/\$
298	295, 296, 297	mp2an 672	. . . . . . . . . . . . . . . . . 18
299	157, 294, 298	ltleii 9497	. . . . . . . . . . . . . . . . 17
300		eluz 10874	. . . . . . . . . . . . . . . . . 18 $/\$
301	251, 293, 300	mp2an 672	. . . . . . . . . . . . . . . . 17
302	299, 301	mpbir 209	. . . . . . . . . . . . . . . 16
303		fzss1 11497	. . . . . . . . . . . . . . . 16
304	302, 303	ax-mp 5	. . . . . . . . . . . . . . 15
305	304	sseli 3352	. . . . . . . . . . . . . 14
306	305	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$
307	48, 294	ltnlei 9495	. . . . . . . . . . . . . . . . . . 19
308	296, 307	mpbi 208	. . . . . . . . . . . . . . . . . 18
309	308	intnanr 906	. . . . . . . . . . . . . . . . 17 $/\$
310		elfz 11443	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
311	8, 293, 310	mp3an12 1304	. . . . . . . . . . . . . . . . . 18 $/\$
312	240, 311	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
313	309, 312	mtbiri 303	. . . . . . . . . . . . . . . 16 $/\$
314		eleq1 2503	. . . . . . . . . . . . . . . . 17
315	314	notbid 294	. . . . . . . . . . . . . . . 16
316	313, 315	syl5ibrcom 222	. . . . . . . . . . . . . . 15 $/\$
317	316	necon2ad 2659	. . . . . . . . . . . . . 14 $/\$
318	317	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$
319	21	axlowdimlem9 23196	. . . . . . . . . . . . 13 $/\$
320	306, 318, 319	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
321	320	sq0id 11959	. . . . . . . . . . 11 $/\$ $/\$
322	321	sumeq2dv 13180	. . . . . . . . . 10 $/\$
323		fzfi 11794	. . . . . . . . . . . 12
324	323	olci 391	. . . . . . . . . . 11 $\/$
325		sumz 13199	. . . . . . . . . . 11 $\/$
326	324, 325	ax-mp 5	. . . . . . . . . 10
327	322, 326	syl6eq 2491	. . . . . . . . 9 $/\$
328	327	oveq2d 6107	. . . . . . . 8 $/\$
329	291, 328	eqtrd 2475	. . . . . . 7 $/\$
330	329, 220	syl6eq 2491	. . . . . 6 $/\$
331	330	3adant3 1008	. . . . 5 $/\$ $/\$
332	228, 281, 331	3eqtr4rd 2486	. . . 4 $/\$ $/\$
333	44, 54, 55, 332	syl3anc 1218	. . 3 $/\$ $/\$
334	333	ex 434	. 2 $/\$
335	43, 334	pm2.61ine 2687	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wne 2606 $\$ cdif 3325

cun 3326

cin 3327

wss 3328

c0 3637

csn 3877

cop 3883 class class class wbr 4292

cxp 4838

cfv 5418 (class class class)co 6091

cfn 7310

cc 9280

cr 9281

cc0 9282

c1 9283

caddc 9285

clt 9418

cle 9419

cmin 9595

cneg 9596

cn 10322

c2 10371

c3 10372

cz 10646

cuz 10861

cfz 11437

cexp 11865

csu 13163

cee 23134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-inf2 7847 ax-cnex 9338 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359 ax-pre-sup 9360

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-nel 2609 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-se 4680 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-isom 5427 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-1st 6577 df-2nd 6578 df-recs 6832 df-rdg 6866 df-1o 6920 df-oadd 6924 df-er 7101 df-map 7216 df-en 7311 df-dom 7312 df-sdom 7313 df-fin 7314 df-sup 7691 df-oi 7724 df-card 8109 df-pnf 9420 df-mnf 9421 df-xr 9422 df-ltxr 9423 df-le 9424 df-sub 9597 df-neg 9598 df-div 9994 df-nn 10323 df-2 10380 df-3 10381 df-n0 10580 df-z 10647 df-uz 10862 df-rp 10992 df-fz 11438 df-fzo 11549 df-seq 11807 df-exp 11866 df-hash 12104 df-cj 12588 df-re 12589 df-im 12590 df-sqr 12724 df-abs 12725 df-clim 12966 df-sum 13164 df-ee 23137

This theorem is referenced by: axlowdimlem17 23204

W3C validator