axlowdimlem16 - Metamath Proof Explorer

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

Theorem axlowdimlem16 24386

Description: Lemma for axlowdim 24390. 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 11722	. . . . . 6
2		oveq1 6303	. . . . . . . . . . 11
3		df-3 10616	. . . . . . . . . . 11
4	2, 3	syl6reqr 2517	. . . . . . . . . 10
5	4, 4	oveq12d 6314	. . . . . . . . 9
6	5	sumeq1d 13534	. . . . . . . 8
7	2, 3	syl6eqr 2516	. . . . . . . . . 10
8		3z 10918	. . . . . . . . . 10
9	7, 8	syl6eqel 2553	. . . . . . . . 9
10		ax-1cn 9567	. . . . . . . . . 10
11	10	sqcli 12250	. . . . . . . . 9
12		fveq2 5872	. . . . . . . . . . . 12
13		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
14	13	axlowdimlem11 24381	. . . . . . . . . . . 12
15	12, 14	syl6eq 2514	. . . . . . . . . . 11
16	15	oveq1d 6311	. . . . . . . . . 10
17	16	fsum1 13575	. . . . . . . . 9 $/\$
18	9, 11, 17	sylancl 662	. . . . . . . 8
19	6, 18	eqtrd 2498	. . . . . . 7
20		fveq2 5872	. . . . . . . . . . . 12
21		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
22	21	axlowdimlem8 24378	. . . . . . . . . . . 12
23	20, 22	syl6eq 2514	. . . . . . . . . . 11
24	23	oveq1d 6311	. . . . . . . . . 10
25		sqneg 12230	. . . . . . . . . . 11
26	10, 25	ax-mp 5	. . . . . . . . . 10
27	24, 26	syl6eq 2514	. . . . . . . . 9
28	27	fsum1 13575	. . . . . . . 8 $/\$
29	8, 11, 28	mp2an 672	. . . . . . 7
30	19, 29	syl6reqr 2517	. . . . . 6
31	1, 30	syl 16	. . . . 5
32	31	a1i 11	. . . 4
33		oveq1 6303	. . . . . . 7
34		3m1e2 10673	. . . . . . 7
35	33, 34	syl6eq 2514	. . . . . 6
36	35	oveq2d 6312	. . . . 5
37	36	eleq2d 2527	. . . 4
38		oveq2 6304	. . . . . 6
39	38	sumeq1d 13534	. . . . 5
40	38	sumeq1d 13534	. . . . 5
41	39, 40	eqeq12d 2479	. . . 4
42	32, 37, 41	3imtr4d 268	. . 3
43	42	adantld 467	. 2 $/\$
44		simprl 756	. . . 4 $/\$ $/\$
45		eluzle 11118	. . . . . . 7
46	45	adantl 466	. . . . . 6 $/\$
47		simpl 457	. . . . . 6 $/\$
48		3re 10630	. . . . . . 7
49		eluzelre 11116	. . . . . . . 8
50	49	adantl 466	. . . . . . 7 $/\$
51		ltlen 9703	. . . . . . 7 $/\$ $/\$
52	48, 50, 51	sylancr 663	. . . . . 6 $/\$ $/\$
53	46, 47, 52	mpbir2and 922	. . . . 5 $/\$
54	53	adantrr 716	. . . 4 $/\$ $/\$
55		simprr 757	. . . 4 $/\$ $/\$
56		fzssp1 11751	. . . . . . . . . . . . 13
57		simp3 998	. . . . . . . . . . . . 13 $/\$ $/\$
58	56, 57	sseldi 3497	. . . . . . . . . . . 12 $/\$ $/\$
59		eluzelz 11115	. . . . . . . . . . . . . . . 16
60	59	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	60	zcnd 10991	. . . . . . . . . . . . . 14 $/\$ $/\$
62		npcan 9848	. . . . . . . . . . . . . 14 $/\$
63	61, 10, 62	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	oveq2d 6312	. . . . . . . . . . . 12 $/\$ $/\$
65	58, 64	eleqtrd 2547	. . . . . . . . . . 11 $/\$ $/\$
66		elfzelz 11713	. . . . . . . . . . 11
67	65, 66	syl 16	. . . . . . . . . 10 $/\$ $/\$
68	67	zred 10990	. . . . . . . . 9 $/\$ $/\$
69	68	ltp1d 10496	. . . . . . . 8 $/\$ $/\$
70		fzdisj 11737	. . . . . . . 8
71	69, 70	syl 16	. . . . . . 7 $/\$ $/\$
72		fzsplit 11736	. . . . . . . 8
73	65, 72	syl 16	. . . . . . 7 $/\$ $/\$
74		fzfid 12085	. . . . . . 7 $/\$ $/\$
75		eluzge3nn 11147	. . . . . . . . . . 11
76		2eluzge1 11152	. . . . . . . . . . . . 13
77		fzss1 11747	. . . . . . . . . . . . 13
78	76, 77	ax-mp 5	. . . . . . . . . . . 12
79	78	sseli 3495	. . . . . . . . . . 11
80	13	axlowdimlem10 24380	. . . . . . . . . . 11 $/\$
81	75, 79, 80	syl2an 477	. . . . . . . . . 10 $/\$
82		fzss1 11747	. . . . . . . . . . . 12
83	76, 82	ax-mp 5	. . . . . . . . . . 11
84	83	sseli 3495	. . . . . . . . . 10
85		fveecn 24331	. . . . . . . . . 10 $/\$
86	81, 84, 85	syl2an 477	. . . . . . . . 9 $/\$ $/\$
87	86	sqcld 12310	. . . . . . . 8 $/\$ $/\$
88	87	3adantl2 1153	. . . . . . 7 $/\$ $/\$ $/\$
89	71, 73, 74, 88	fsumsplit 13573	. . . . . 6 $/\$ $/\$
90		fzss1 11747	. . . . . . . . . . . . . . . 16
91	76, 90	ax-mp 5	. . . . . . . . . . . . . . 15
92	91	sseli 3495	. . . . . . . . . . . . . 14
93		elfzelz 11713	. . . . . . . . . . . . . . . . . . . 20
94	93	zred 10990	. . . . . . . . . . . . . . . . . . 19
95	94	3ad2ant3 1019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
96	49	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
97		peano2rem 9905	. . . . . . . . . . . . . . . . . . . 20
98	96, 97	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		elfzle2 11715	. . . . . . . . . . . . . . . . . . . 20
100	99	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	96	ltm1d 10498	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
102	95, 98, 96, 100, 101	lelttrd 9757	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
103	95, 96, 102	ltled 9750	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	93	3ad2ant3 1019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
105		eluz 11119	. . . . . . . . . . . . . . . . . 18 $/\$
106	104, 60, 105	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
107	103, 106	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
108		fzss2 11748	. . . . . . . . . . . . . . . 16
109	107, 108	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
110	109	sseld 3498	. . . . . . . . . . . . . 14 $/\$ $/\$
111	92, 110	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$
112	111	imp 429	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113		elfzelz 11713	. . . . . . . . . . . . . . 15
114	113	zred 10990	. . . . . . . . . . . . . 14
115	114	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	95	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
117		peano2re 9770	. . . . . . . . . . . . . . . . 17
118	94, 117	syl 16	. . . . . . . . . . . . . . . 16
119	118	3ad2ant3 1019	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121		elfzle2 11715	. . . . . . . . . . . . . . 15
122	121	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	116	ltp1d 10496	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124	115, 116, 120, 122, 123	lelttrd 9757	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125	115, 124	ltned 9738	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	13	axlowdimlem12 24382	. . . . . . . . . . . 12 $/\$
127	112, 125, 126	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
128	127	sq0id 12263	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128	sumeq2dv 13536	. . . . . . . . 9 $/\$ $/\$
130		fzfi 12084	. . . . . . . . . . 11
131	130	olci 391	. . . . . . . . . 10 $\/$
132		sumz 13555	. . . . . . . . . 10 $\/$
133	131, 132	ax-mp 5	. . . . . . . . 9
134	129, 133	syl6eq 2514	. . . . . . . 8 $/\$ $/\$
135	104	peano2zd 10993	. . . . . . . . . . 11 $/\$ $/\$
136		sq1 12264	. . . . . . . . . . . . 13
137	16, 136	syl6eq 2514	. . . . . . . . . . . 12
138	137	fsum1 13575	. . . . . . . . . . 11 $/\$
139	135, 10, 138	sylancl 662	. . . . . . . . . 10 $/\$ $/\$
140		oveq2 6304	. . . . . . . . . . . 12
141	140	sumeq1d 13534	. . . . . . . . . . 11
142	141	eqeq1d 2459	. . . . . . . . . 10
143	139, 142	syl5ib 219	. . . . . . . . 9 $/\$ $/\$
144	104	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
145	144	zred 10990	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	60	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	146	zred 10990	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
148	147, 97	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	100	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
150	147	ltm1d 10498	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	145, 148, 147, 149, 150	lelttrd 9757	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152		1red 9628	. . . . . . . . . . . . . . . . . . 19
153		2re 10626	. . . . . . . . . . . . . . . . . . . 20
154	153	a1i 11	. . . . . . . . . . . . . . . . . . 19
155		1le2 10770	. . . . . . . . . . . . . . . . . . . 20
156	155	a1i 11	. . . . . . . . . . . . . . . . . . 19
157		elfzle1 11714	. . . . . . . . . . . . . . . . . . 19
158	152, 154, 94, 156, 157	letrd 9756	. . . . . . . . . . . . . . . . . 18
159	158	3ad2ant3 1019	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
160	159	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
161		elnnz1 10911	. . . . . . . . . . . . . . . 16 $/\$
162	144, 160, 161	sylanbrc 664	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163	75	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 $/\$ $/\$
164	163	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
165		nnltp1le 10940	. . . . . . . . . . . . . . 15 $/\$
166	162, 164, 165	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	151, 166	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	135	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
169		eluz 11119	. . . . . . . . . . . . . 14 $/\$
170	168, 146, 169	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	167, 170	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172		simpr1 1002	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
173		simpr3 1004	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
174	172, 173, 81	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175	174	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	162	peano2nnd 10573	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		nnuz 11141	. . . . . . . . . . . . . . . . 17
178	176, 177	syl6eleq 2555	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
179		fzss1 11747	. . . . . . . . . . . . . . . 16
180	178, 179	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	180	sselda 3499	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	175, 181, 85	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
183	182	sqcld 12310	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
184	12	oveq1d 6311	. . . . . . . . . . . . 13
185	14	oveq1i 6306	. . . . . . . . . . . . . 14
186	185, 136	eqtri 2486	. . . . . . . . . . . . 13
187	184, 186	syl6eq 2514	. . . . . . . . . . . 12
188	171, 183, 187	fsum1p 13579	. . . . . . . . . . 11 $/\$ $/\$ $/\$
189	176	peano2nnd 10573	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
190	189, 177	syl6eleq 2555	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
191		fzss1 11747	. . . . . . . . . . . . . . . . . . 19
192	190, 191	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
193	192	sselda 3499	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
194	145, 117	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	194	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
196		peano2re 9770	. . . . . . . . . . . . . . . . . . . 20
197	195, 196	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
198		elfzelz 11713	. . . . . . . . . . . . . . . . . . . . 21
199	198	zred 10990	. . . . . . . . . . . . . . . . . . . 20
200	199	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
201	195	ltp1d 10496	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
202		elfzle1 11714	. . . . . . . . . . . . . . . . . . . 20
203	202	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
204	195, 197, 200, 201, 203	ltletrd 9759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
205	195, 204	gtned 9737	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
206	193, 205, 126	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
207	206	sq0id 12263	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
208	207	sumeq2dv 13536	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
209		fzfi 12084	. . . . . . . . . . . . . . . 16
210	209	olci 391	. . . . . . . . . . . . . . 15 $\/$
211		sumz 13555	. . . . . . . . . . . . . . 15 $\/$
212	210, 211	ax-mp 5	. . . . . . . . . . . . . 14
213	208, 212	syl6eq 2514	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
214	213	oveq2d 6312	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
215		1p0e1 10669	. . . . . . . . . . . 12
216	214, 215	syl6eq 2514	. . . . . . . . . . 11 $/\$ $/\$ $/\$
217	188, 216	eqtrd 2498	. . . . . . . . . 10 $/\$ $/\$ $/\$
218	217	ex 434	. . . . . . . . 9 $/\$ $/\$
219	143, 218	pm2.61ine 2770	. . . . . . . 8 $/\$ $/\$
220	134, 219	oveq12d 6314	. . . . . . 7 $/\$ $/\$
221		0p1e1 10668	. . . . . . 7
222	220, 221	syl6eq 2514	. . . . . 6 $/\$ $/\$
223	89, 222	eqtrd 2498	. . . . 5 $/\$ $/\$
224		simp1 996	. . . . . . . 8 $/\$ $/\$
225		2lt3 10724	. . . . . . . . . 10
226	153, 48, 225	ltleii 9724	. . . . . . . . 9
227		2z 10917	. . . . . . . . . 10
228	227	eluz1i 11113	. . . . . . . . 9 $/\$
229	8, 226, 228	mpbir2an 920	. . . . . . . 8
230		uztrn 11122	. . . . . . . 8 $/\$
231	224, 229, 230	sylancl 662	. . . . . . 7 $/\$ $/\$
232		fveq2 5872	. . . . . . . 8
233	232	oveq1d 6311	. . . . . . 7
234	231, 88, 233	fsum1p 13579	. . . . . 6 $/\$ $/\$
235	59	adantr 465	. . . . . . . . . . . . . . 15 $/\$
236	235	zred 10990	. . . . . . . . . . . . . 14 $/\$
237		lttr 9678	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
238	153, 48, 237	mp3an12 1314	. . . . . . . . . . . . . . . . 17 $/\$
239	225, 238	mpani 676	. . . . . . . . . . . . . . . 16
240	49, 239	syl 16	. . . . . . . . . . . . . . 15
241	240	imp 429	. . . . . . . . . . . . . 14 $/\$
242		ltle 9690	. . . . . . . . . . . . . . 15 $/\$
243	153, 242	mpan 670	. . . . . . . . . . . . . 14
244	236, 241, 243	sylc 60	. . . . . . . . . . . . 13 $/\$
245	244, 155	jctil 537	. . . . . . . . . . . 12 $/\$ $/\$
246		1z 10915	. . . . . . . . . . . . . 14
247		elfz 11703	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
248	227, 246, 247	mp3an12 1314	. . . . . . . . . . . . 13 $/\$
249	235, 248	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
250	245, 249	mpbird 232	. . . . . . . . . . 11 $/\$
251	250	3adant3 1016	. . . . . . . . . 10 $/\$ $/\$
252	94	ltp1d 10496	. . . . . . . . . . . . . 14
253	154, 94, 118, 157, 252	lelttrd 9757	. . . . . . . . . . . . 13
254	253	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$
255		ltne 9698	. . . . . . . . . . . 12 $/\$
256	153, 254, 255	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$
257	256	necomd 2728	. . . . . . . . . 10 $/\$ $/\$
258	13	axlowdimlem12 24382	. . . . . . . . . 10 $/\$
259	251, 257, 258	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
260	259	sq0id 12263	. . . . . . . 8 $/\$ $/\$
261	260	oveq1d 6311	. . . . . . 7 $/\$ $/\$
262	3	oveq1i 6306	. . . . . . . . 9
263	262	sumeq1i 13531	. . . . . . . 8
264	263	oveq2i 6307	. . . . . . 7
265	261, 264	syl6eqr 2516	. . . . . 6 $/\$ $/\$
266		fzfid 12085	. . . . . . . 8 $/\$ $/\$
267		3nn 10715	. . . . . . . . . . . . . 14
268	267, 177	eleqtri 2543	. . . . . . . . . . . . 13
269		fzss1 11747	. . . . . . . . . . . . 13
270	268, 269	ax-mp 5	. . . . . . . . . . . 12
271	270	sseli 3495	. . . . . . . . . . 11
272	81, 271, 85	syl2an 477	. . . . . . . . . 10 $/\$ $/\$
273	272	sqcld 12310	. . . . . . . . 9 $/\$ $/\$
274	273	3adantl2 1153	. . . . . . . 8 $/\$ $/\$ $/\$
275	266, 274	fsumcl 13566	. . . . . . 7 $/\$ $/\$
276	275	addid2d 9798	. . . . . 6 $/\$ $/\$
277	234, 265, 276	3eqtrrd 2503	. . . . 5 $/\$ $/\$
278		simpl 457	. . . . . . . . 9 $/\$
279	21	axlowdimlem7 24377	. . . . . . . . . . . 12
280	279	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
281	271	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
282		fveecn 24331	. . . . . . . . . . 11 $/\$
283	280, 281, 282	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$
284	283	sqcld 12310	. . . . . . . . 9 $/\$ $/\$
285		neg1sqe1 12265	. . . . . . . . . 10
286	24, 285	syl6eq 2514	. . . . . . . . 9
287	278, 284, 286	fsum1p 13579	. . . . . . . 8 $/\$
288		1re 9612	. . . . . . . . . . . . . . . . . 18
289		zaddcl 10925	. . . . . . . . . . . . . . . . . . . 20 $/\$
290	8, 246, 289	mp2an 672	. . . . . . . . . . . . . . . . . . 19
291	290	zrei 10891	. . . . . . . . . . . . . . . . . 18
292		1lt3 10725	. . . . . . . . . . . . . . . . . . 19
293	48	ltp1i 10469	. . . . . . . . . . . . . . . . . . 19
294	288, 48, 291	lttri 9727	. . . . . . . . . . . . . . . . . . 19 $/\$
295	292, 293, 294	mp2an 672	. . . . . . . . . . . . . . . . . 18
296	288, 291, 295	ltleii 9724	. . . . . . . . . . . . . . . . 17
297		eluz 11119	. . . . . . . . . . . . . . . . . 18 $/\$
298	246, 290, 297	mp2an 672	. . . . . . . . . . . . . . . . 17
299	296, 298	mpbir 209	. . . . . . . . . . . . . . . 16
300		fzss1 11747	. . . . . . . . . . . . . . . 16
301	299, 300	ax-mp 5	. . . . . . . . . . . . . . 15
302	301	sseli 3495	. . . . . . . . . . . . . 14
303	302	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$
304	48, 291	ltnlei 9722	. . . . . . . . . . . . . . . . . . 19
305	293, 304	mpbi 208	. . . . . . . . . . . . . . . . . 18
306	305	intnanr 915	. . . . . . . . . . . . . . . . 17 $/\$
307		elfz 11703	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
308	8, 290, 307	mp3an12 1314	. . . . . . . . . . . . . . . . . 18 $/\$
309	235, 308	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
310	306, 309	mtbiri 303	. . . . . . . . . . . . . . . 16 $/\$
311		eleq1 2529	. . . . . . . . . . . . . . . . 17
312	311	notbid 294	. . . . . . . . . . . . . . . 16
313	310, 312	syl5ibrcom 222	. . . . . . . . . . . . . . 15 $/\$
314	313	necon2ad 2670	. . . . . . . . . . . . . 14 $/\$
315	314	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$
316	21	axlowdimlem9 24379	. . . . . . . . . . . . 13 $/\$
317	303, 315, 316	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
318	317	sq0id 12263	. . . . . . . . . . 11 $/\$ $/\$
319	318	sumeq2dv 13536	. . . . . . . . . 10 $/\$
320		fzfi 12084	. . . . . . . . . . . 12
321	320	olci 391	. . . . . . . . . . 11 $\/$
322		sumz 13555	. . . . . . . . . . 11 $\/$
323	321, 322	ax-mp 5	. . . . . . . . . 10
324	319, 323	syl6eq 2514	. . . . . . . . 9 $/\$
325	324	oveq2d 6312	. . . . . . . 8 $/\$
326	287, 325	eqtrd 2498	. . . . . . 7 $/\$
327	326, 215	syl6eq 2514	. . . . . 6 $/\$
328	327	3adant3 1016	. . . . 5 $/\$ $/\$
329	223, 277, 328	3eqtr4rd 2509	. . . 4 $/\$ $/\$
330	44, 54, 55, 329	syl3anc 1228	. . 3 $/\$ $/\$
331	330	ex 434	. 2 $/\$
332	43, 331	pm2.61ine 2770	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wcel 1819

wne 2652 $\$ cdif 3468

cun 3469

cin 3470

wss 3471

c0 3793

csn 4032

cop 4038 class class class wbr 4456

cxp 5006

cfv 5594 (class class class)co 6296

cfn 7535

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

clt 9645

cle 9646

cmin 9824

cneg 9825

cn 10556

c2 10606

c3 10607

cz 10885

cuz 11106

cfz 11697

cexp 12168

csu 13519

cee 24317

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11821 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-clim 13322 df-sum 13520 df-ee 24320

This theorem is referenced by: axlowdimlem17 24387

W3C validator