axlowdimlem16 - Metamath Proof Explorer

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

Theorem axlowdimlem16 23964

Description: Lemma for axlowdim 23968. 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 11697	. . . . . 6
2		oveq1 6291	. . . . . . . . . . 11
3		df-3 10595	. . . . . . . . . . 11
4	2, 3	syl6reqr 2527	. . . . . . . . . 10
5	4, 4	oveq12d 6302	. . . . . . . . 9
6	5	sumeq1d 13486	. . . . . . . 8
7	2, 3	syl6eqr 2526	. . . . . . . . . 10
8		3z 10897	. . . . . . . . . 10
9	7, 8	syl6eqel 2563	. . . . . . . . 9
10		ax-1cn 9550	. . . . . . . . . 10
11	10	sqcli 12216	. . . . . . . . 9
12		fveq2 5866	. . . . . . . . . . . 12
13		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
14	13	axlowdimlem11 23959	. . . . . . . . . . . 12
15	12, 14	syl6eq 2524	. . . . . . . . . . 11
16	15	oveq1d 6299	. . . . . . . . . 10
17	16	fsum1 13527	. . . . . . . . 9 $/\$
18	9, 11, 17	sylancl 662	. . . . . . . 8
19	6, 18	eqtrd 2508	. . . . . . 7
20		fveq2 5866	. . . . . . . . . . . 12
21		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
22	21	axlowdimlem8 23956	. . . . . . . . . . . 12
23	20, 22	syl6eq 2524	. . . . . . . . . . 11
24	23	oveq1d 6299	. . . . . . . . . 10
25		sqneg 12196	. . . . . . . . . . 11
26	10, 25	ax-mp 5	. . . . . . . . . 10
27	24, 26	syl6eq 2524	. . . . . . . . 9
28	27	fsum1 13527	. . . . . . . 8 $/\$
29	8, 11, 28	mp2an 672	. . . . . . 7
30	19, 29	syl6reqr 2527	. . . . . 6
31	1, 30	syl 16	. . . . 5
32	31	a1i 11	. . . 4
33		oveq1 6291	. . . . . . 7
34		3m1e2 10652	. . . . . . 7
35	33, 34	syl6eq 2524	. . . . . 6
36	35	oveq2d 6300	. . . . 5
37	36	eleq2d 2537	. . . 4
38		oveq2 6292	. . . . . 6
39	38	sumeq1d 13486	. . . . 5
40	38	sumeq1d 13486	. . . . 5
41	39, 40	eqeq12d 2489	. . . 4
42	32, 37, 41	3imtr4d 268	. . 3
43	42	adantld 467	. 2 $/\$
44		simprl 755	. . . 4 $/\$ $/\$
45		eluzle 11094	. . . . . . 7
46	45	adantl 466	. . . . . 6 $/\$
47		simpl 457	. . . . . 6 $/\$
48		3re 10609	. . . . . . 7
49		eluzelre 11092	. . . . . . . 8
50	49	adantl 466	. . . . . . 7 $/\$
51		ltlen 9686	. . . . . . 7 $/\$ $/\$
52	48, 50, 51	sylancr 663	. . . . . 6 $/\$ $/\$
53	46, 47, 52	mpbir2and 920	. . . . 5 $/\$
54	53	adantrr 716	. . . 4 $/\$ $/\$
55		simprr 756	. . . 4 $/\$ $/\$
56		fzssp1 11726	. . . . . . . . . . . . 13
57		simp3 998	. . . . . . . . . . . . 13 $/\$ $/\$
58	56, 57	sseldi 3502	. . . . . . . . . . . 12 $/\$ $/\$
59		eluzelz 11091	. . . . . . . . . . . . . . . 16
60	59	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	60	zcnd 10967	. . . . . . . . . . . . . 14 $/\$ $/\$
62		npcan 9829	. . . . . . . . . . . . . 14 $/\$
63	61, 10, 62	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	oveq2d 6300	. . . . . . . . . . . 12 $/\$ $/\$
65	58, 64	eleqtrd 2557	. . . . . . . . . . 11 $/\$ $/\$
66		elfzelz 11688	. . . . . . . . . . 11
67	65, 66	syl 16	. . . . . . . . . 10 $/\$ $/\$
68	67	zred 10966	. . . . . . . . 9 $/\$ $/\$
69	68	ltp1d 10476	. . . . . . . 8 $/\$ $/\$
70		fzdisj 11712	. . . . . . . 8
71	69, 70	syl 16	. . . . . . 7 $/\$ $/\$
72		fzsplit 11711	. . . . . . . 8
73	65, 72	syl 16	. . . . . . 7 $/\$ $/\$
74		fzfid 12051	. . . . . . 7 $/\$ $/\$
75		3nn 10694	. . . . . . . . . . . . 13
76		uznnssnn 11128	. . . . . . . . . . . . 13
77	75, 76	ax-mp 5	. . . . . . . . . . . 12
78	77	sseli 3500	. . . . . . . . . . 11
79		2nn 10693	. . . . . . . . . . . . . 14
80		nnuz 11117	. . . . . . . . . . . . . 14
81	79, 80	eleqtri 2553	. . . . . . . . . . . . 13
82		fzss1 11722	. . . . . . . . . . . . 13
83	81, 82	ax-mp 5	. . . . . . . . . . . 12
84	83	sseli 3500	. . . . . . . . . . 11
85	13	axlowdimlem10 23958	. . . . . . . . . . 11 $/\$
86	78, 84, 85	syl2an 477	. . . . . . . . . 10 $/\$
87		fzss1 11722	. . . . . . . . . . . 12
88	81, 87	ax-mp 5	. . . . . . . . . . 11
89	88	sseli 3500	. . . . . . . . . 10
90		fveecn 23909	. . . . . . . . . 10 $/\$
91	86, 89, 90	syl2an 477	. . . . . . . . 9 $/\$ $/\$
92	91	sqcld 12276	. . . . . . . 8 $/\$ $/\$
93	92	3adantl2 1153	. . . . . . 7 $/\$ $/\$ $/\$
94	71, 73, 74, 93	fsumsplit 13525	. . . . . 6 $/\$ $/\$
95		fzss1 11722	. . . . . . . . . . . . . . . 16
96	81, 95	ax-mp 5	. . . . . . . . . . . . . . 15
97	96	sseli 3500	. . . . . . . . . . . . . 14
98		elfzelz 11688	. . . . . . . . . . . . . . . . . . . 20
99	98	zred 10966	. . . . . . . . . . . . . . . . . . 19
100	99	3ad2ant3 1019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
101	49	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102		peano2rem 9886	. . . . . . . . . . . . . . . . . . . 20
103	101, 102	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104		elfzle2 11690	. . . . . . . . . . . . . . . . . . . 20
105	104	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
106	101	ltm1d 10478	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
107	100, 103, 101, 105, 106	lelttrd 9739	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
108	100, 101, 107	ltled 9732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
109	98	3ad2ant3 1019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
110		eluz 11095	. . . . . . . . . . . . . . . . . 18 $/\$
111	109, 60, 110	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
112	108, 111	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113		fzss2 11723	. . . . . . . . . . . . . . . 16
114	112, 113	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	114	sseld 3503	. . . . . . . . . . . . . 14 $/\$ $/\$
116	97, 115	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	imp 429	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		elfzelz 11688	. . . . . . . . . . . . . . 15
119	118	zred 10966	. . . . . . . . . . . . . 14
120	119	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	100	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
122		peano2re 9752	. . . . . . . . . . . . . . . . 17
123	99, 122	syl 16	. . . . . . . . . . . . . . . 16
124	123	3ad2ant3 1019	. . . . . . . . . . . . . . 15 $/\$ $/\$
125	124	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
126		elfzle2 11690	. . . . . . . . . . . . . . 15
127	126	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
128	121	ltp1d 10476	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
129	120, 121, 125, 127, 128	lelttrd 9739	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	120, 129	ltned 9720	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	13	axlowdimlem12 23960	. . . . . . . . . . . 12 $/\$
132	117, 130, 131	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
133	132	sq0id 12229	. . . . . . . . . 10 $/\$ $/\$ $/\$
134	133	sumeq2dv 13488	. . . . . . . . 9 $/\$ $/\$
135		fzfi 12050	. . . . . . . . . . 11
136	135	olci 391	. . . . . . . . . 10 $\/$
137		sumz 13507	. . . . . . . . . 10 $\/$
138	136, 137	ax-mp 5	. . . . . . . . 9
139	134, 138	syl6eq 2524	. . . . . . . 8 $/\$ $/\$
140	109	peano2zd 10969	. . . . . . . . . . 11 $/\$ $/\$
141		sq1 12230	. . . . . . . . . . . . 13
142	16, 141	syl6eq 2524	. . . . . . . . . . . 12
143	142	fsum1 13527	. . . . . . . . . . 11 $/\$
144	140, 10, 143	sylancl 662	. . . . . . . . . 10 $/\$ $/\$
145		oveq2 6292	. . . . . . . . . . . 12
146	145	sumeq1d 13486	. . . . . . . . . . 11
147	146	eqeq1d 2469	. . . . . . . . . 10
148	144, 147	syl5ib 219	. . . . . . . . 9 $/\$ $/\$
149	109	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
150	149	zred 10966	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	60	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
152	151	zred 10966	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
153	152, 102	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
154	105	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
155	152	ltm1d 10478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
156	150, 153, 152, 154, 155	lelttrd 9739	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
157		1re 9595	. . . . . . . . . . . . . . . . . . . 20
158	157	a1i 11	. . . . . . . . . . . . . . . . . . 19
159		2re 10605	. . . . . . . . . . . . . . . . . . . 20
160	159	a1i 11	. . . . . . . . . . . . . . . . . . 19
161		1le2 10749	. . . . . . . . . . . . . . . . . . . 20
162	161	a1i 11	. . . . . . . . . . . . . . . . . . 19
163		elfzle1 11689	. . . . . . . . . . . . . . . . . . 19
164	158, 160, 99, 162, 163	letrd 9738	. . . . . . . . . . . . . . . . . 18
165	164	3ad2ant3 1019	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	165	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
167		elnnz1 10890	. . . . . . . . . . . . . . . 16 $/\$
168	149, 166, 167	sylanbrc 664	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
169	78	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 $/\$ $/\$
170	169	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
171		nnltp1le 10918	. . . . . . . . . . . . . . 15 $/\$
172	168, 170, 171	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
173	156, 172	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
174	140	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175		eluz 11095	. . . . . . . . . . . . . 14 $/\$
176	174, 151, 175	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
177	173, 176	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
178		simpr1 1002	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
179		simpr3 1004	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180	178, 179, 86	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	180	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	168	peano2nnd 10553	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
183	182, 80	syl6eleq 2565	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
184		fzss1 11722	. . . . . . . . . . . . . . . 16
185	183, 184	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
186	185	sselda 3504	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	181, 186, 90	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
188	187	sqcld 12276	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
189	12	oveq1d 6299	. . . . . . . . . . . . 13
190	14	oveq1i 6294	. . . . . . . . . . . . . 14
191	190, 141	eqtri 2496	. . . . . . . . . . . . 13
192	189, 191	syl6eq 2524	. . . . . . . . . . . 12
193	177, 188, 192	fsum1p 13531	. . . . . . . . . . 11 $/\$ $/\$ $/\$
194	182	peano2nnd 10553	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
195	194, 80	syl6eleq 2565	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196		fzss1 11722	. . . . . . . . . . . . . . . . . . 19
197	195, 196	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
198	197	sselda 3504	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
199	150, 122	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
200	199	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
201		peano2re 9752	. . . . . . . . . . . . . . . . . . . 20
202	200, 201	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
203		elfzelz 11688	. . . . . . . . . . . . . . . . . . . . 21
204	203	zred 10966	. . . . . . . . . . . . . . . . . . . 20
205	204	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
206	200	ltp1d 10476	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
207		elfzle1 11689	. . . . . . . . . . . . . . . . . . . 20
208	207	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
209	200, 202, 205, 206, 208	ltletrd 9741	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
210	200, 209	gtned 9719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
211	198, 210, 131	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
212	211	sq0id 12229	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
213	212	sumeq2dv 13488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
214		fzfi 12050	. . . . . . . . . . . . . . . 16
215	214	olci 391	. . . . . . . . . . . . . . 15 $\/$
216		sumz 13507	. . . . . . . . . . . . . . 15 $\/$
217	215, 216	ax-mp 5	. . . . . . . . . . . . . 14
218	213, 217	syl6eq 2524	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
219	218	oveq2d 6300	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
220		1p0e1 10648	. . . . . . . . . . . 12
221	219, 220	syl6eq 2524	. . . . . . . . . . 11 $/\$ $/\$ $/\$
222	193, 221	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	222	ex 434	. . . . . . . . 9 $/\$ $/\$
224	148, 223	pm2.61ine 2780	. . . . . . . 8 $/\$ $/\$
225	139, 224	oveq12d 6302	. . . . . . 7 $/\$ $/\$
226		0p1e1 10647	. . . . . . 7
227	225, 226	syl6eq 2524	. . . . . 6 $/\$ $/\$
228	94, 227	eqtrd 2508	. . . . 5 $/\$ $/\$
229		simp1 996	. . . . . . . 8 $/\$ $/\$
230		2lt3 10703	. . . . . . . . . 10
231	159, 48, 230	ltleii 9707	. . . . . . . . 9
232		2z 10896	. . . . . . . . . 10
233	232	eluz1i 11089	. . . . . . . . 9 $/\$
234	8, 231, 233	mpbir2an 918	. . . . . . . 8
235		uztrn 11098	. . . . . . . 8 $/\$
236	229, 234, 235	sylancl 662	. . . . . . 7 $/\$ $/\$
237		fveq2 5866	. . . . . . . 8
238	237	oveq1d 6299	. . . . . . 7
239	236, 93, 238	fsum1p 13531	. . . . . 6 $/\$ $/\$
240	59	adantr 465	. . . . . . . . . . . . . . 15 $/\$
241	240	zred 10966	. . . . . . . . . . . . . 14 $/\$
242		lttr 9661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
243	159, 48, 242	mp3an12 1314	. . . . . . . . . . . . . . . . 17 $/\$
244	230, 243	mpani 676	. . . . . . . . . . . . . . . 16
245	49, 244	syl 16	. . . . . . . . . . . . . . 15
246	245	imp 429	. . . . . . . . . . . . . 14 $/\$
247		ltle 9673	. . . . . . . . . . . . . . 15 $/\$
248	159, 247	mpan 670	. . . . . . . . . . . . . 14
249	241, 246, 248	sylc 60	. . . . . . . . . . . . 13 $/\$
250	249, 161	jctil 537	. . . . . . . . . . . 12 $/\$ $/\$
251		1z 10894	. . . . . . . . . . . . . 14
252		elfz 11678	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
253	232, 251, 252	mp3an12 1314	. . . . . . . . . . . . 13 $/\$
254	240, 253	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
255	250, 254	mpbird 232	. . . . . . . . . . 11 $/\$
256	255	3adant3 1016	. . . . . . . . . 10 $/\$ $/\$
257	99	ltp1d 10476	. . . . . . . . . . . . . 14
258	160, 99, 123, 163, 257	lelttrd 9739	. . . . . . . . . . . . 13
259	258	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$
260		ltne 9681	. . . . . . . . . . . 12 $/\$
261	159, 259, 260	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$
262	261	necomd 2738	. . . . . . . . . 10 $/\$ $/\$
263	13	axlowdimlem12 23960	. . . . . . . . . 10 $/\$
264	256, 262, 263	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
265	264	sq0id 12229	. . . . . . . 8 $/\$ $/\$
266	265	oveq1d 6299	. . . . . . 7 $/\$ $/\$
267	3	oveq1i 6294	. . . . . . . . 9
268	267	sumeq1i 13483	. . . . . . . 8
269	268	oveq2i 6295	. . . . . . 7
270	266, 269	syl6eqr 2526	. . . . . 6 $/\$ $/\$
271		fzfid 12051	. . . . . . . 8 $/\$ $/\$
272	75, 80	eleqtri 2553	. . . . . . . . . . . . 13
273		fzss1 11722	. . . . . . . . . . . . 13
274	272, 273	ax-mp 5	. . . . . . . . . . . 12
275	274	sseli 3500	. . . . . . . . . . 11
276	86, 275, 90	syl2an 477	. . . . . . . . . 10 $/\$ $/\$
277	276	sqcld 12276	. . . . . . . . 9 $/\$ $/\$
278	277	3adantl2 1153	. . . . . . . 8 $/\$ $/\$ $/\$
279	271, 278	fsumcl 13518	. . . . . . 7 $/\$ $/\$
280	279	addid2d 9780	. . . . . 6 $/\$ $/\$
281	239, 270, 280	3eqtrrd 2513	. . . . 5 $/\$ $/\$
282		simpl 457	. . . . . . . . 9 $/\$
283	21	axlowdimlem7 23955	. . . . . . . . . . . 12
284	283	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
285	275	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
286		fveecn 23909	. . . . . . . . . . 11 $/\$
287	284, 285, 286	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$
288	287	sqcld 12276	. . . . . . . . 9 $/\$ $/\$
289		neg1sqe1 12231	. . . . . . . . . 10
290	24, 289	syl6eq 2524	. . . . . . . . 9
291	282, 288, 290	fsum1p 13531	. . . . . . . 8 $/\$
292		zaddcl 10903	. . . . . . . . . . . . . . . . . . . 20 $/\$
293	8, 251, 292	mp2an 672	. . . . . . . . . . . . . . . . . . 19
294	293	zrei 10870	. . . . . . . . . . . . . . . . . 18
295		1lt3 10704	. . . . . . . . . . . . . . . . . . 19
296	48	ltp1i 10449	. . . . . . . . . . . . . . . . . . 19
297	157, 48, 294	lttri 9710	. . . . . . . . . . . . . . . . . . 19 $/\$
298	295, 296, 297	mp2an 672	. . . . . . . . . . . . . . . . . 18
299	157, 294, 298	ltleii 9707	. . . . . . . . . . . . . . . . 17
300		eluz 11095	. . . . . . . . . . . . . . . . . 18 $/\$
301	251, 293, 300	mp2an 672	. . . . . . . . . . . . . . . . 17
302	299, 301	mpbir 209	. . . . . . . . . . . . . . . 16
303		fzss1 11722	. . . . . . . . . . . . . . . 16
304	302, 303	ax-mp 5	. . . . . . . . . . . . . . 15
305	304	sseli 3500	. . . . . . . . . . . . . 14
306	305	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$
307	48, 294	ltnlei 9705	. . . . . . . . . . . . . . . . . . 19
308	296, 307	mpbi 208	. . . . . . . . . . . . . . . . . 18
309	308	intnanr 913	. . . . . . . . . . . . . . . . 17 $/\$
310		elfz 11678	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
311	8, 293, 310	mp3an12 1314	. . . . . . . . . . . . . . . . . 18 $/\$
312	240, 311	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
313	309, 312	mtbiri 303	. . . . . . . . . . . . . . . 16 $/\$
314		eleq1 2539	. . . . . . . . . . . . . . . . 17
315	314	notbid 294	. . . . . . . . . . . . . . . 16
316	313, 315	syl5ibrcom 222	. . . . . . . . . . . . . . 15 $/\$
317	316	necon2ad 2680	. . . . . . . . . . . . . 14 $/\$
318	317	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$
319	21	axlowdimlem9 23957	. . . . . . . . . . . . 13 $/\$
320	306, 318, 319	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
321	320	sq0id 12229	. . . . . . . . . . 11 $/\$ $/\$
322	321	sumeq2dv 13488	. . . . . . . . . 10 $/\$
323		fzfi 12050	. . . . . . . . . . . 12
324	323	olci 391	. . . . . . . . . . 11 $\/$
325		sumz 13507	. . . . . . . . . . 11 $\/$
326	324, 325	ax-mp 5	. . . . . . . . . 10
327	322, 326	syl6eq 2524	. . . . . . . . 9 $/\$
328	327	oveq2d 6300	. . . . . . . 8 $/\$
329	291, 328	eqtrd 2508	. . . . . . 7 $/\$
330	329, 220	syl6eq 2524	. . . . . 6 $/\$
331	330	3adant3 1016	. . . . 5 $/\$ $/\$
332	228, 281, 331	3eqtr4rd 2519	. . . 4 $/\$ $/\$
333	44, 54, 55, 332	syl3anc 1228	. . 3 $/\$ $/\$
334	333	ex 434	. 2 $/\$
335	43, 334	pm2.61ine 2780	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wne 2662 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

csn 4027

cop 4033 class class class wbr 4447

cxp 4997

cfv 5588 (class class class)co 6284

cfn 7516

cc 9490

cr 9491

cc0 9492

c1 9493

caddc 9495

clt 9628

cle 9629

cmin 9805

cneg 9806

cn 10536

c2 10585

c3 10586

cz 10864

cuz 11082

cfz 11672

cexp 12134

csu 13471

cee 23895

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

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-sup 7901 df-oi 7935 df-card 8320 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-n0 10796 df-z 10865 df-uz 11083 df-rp 11221 df-fz 11673 df-fzo 11793 df-seq 12076 df-exp 12135 df-hash 12374 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-clim 13274 df-sum 13472 df-ee 23898

This theorem is referenced by: axlowdimlem17 23965

W3C validator