axlowdimlem16 - Metamath Proof Explorer

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

Theorem axlowdimlem16 24677

Description: Lemma for axlowdim 24681. 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 11751	. . . . . 6
2		oveq1 6285	. . . . . . . . . . 11
3		df-3 10636	. . . . . . . . . . 11
4	2, 3	syl6reqr 2462	. . . . . . . . . 10
5	4, 4	oveq12d 6296	. . . . . . . . 9
6	5	sumeq1d 13672	. . . . . . . 8
7	2, 3	syl6eqr 2461	. . . . . . . . . 10
8		3z 10938	. . . . . . . . . 10
9	7, 8	syl6eqel 2498	. . . . . . . . 9
10		ax-1cn 9580	. . . . . . . . . 10
11	10	sqcli 12293	. . . . . . . . 9
12		fveq2 5849	. . . . . . . . . . . 12
13		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
14	13	axlowdimlem11 24672	. . . . . . . . . . . 12
15	12, 14	syl6eq 2459	. . . . . . . . . . 11
16	15	oveq1d 6293	. . . . . . . . . 10
17	16	fsum1 13713	. . . . . . . . 9 $/\$
18	9, 11, 17	sylancl 660	. . . . . . . 8
19	6, 18	eqtrd 2443	. . . . . . 7
20		fveq2 5849	. . . . . . . . . . . 12
21		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
22	21	axlowdimlem8 24669	. . . . . . . . . . . 12
23	20, 22	syl6eq 2459	. . . . . . . . . . 11
24	23	oveq1d 6293	. . . . . . . . . 10
25		sqneg 12273	. . . . . . . . . . 11
26	10, 25	ax-mp 5	. . . . . . . . . 10
27	24, 26	syl6eq 2459	. . . . . . . . 9
28	27	fsum1 13713	. . . . . . . 8 $/\$
29	8, 11, 28	mp2an 670	. . . . . . 7
30	19, 29	syl6reqr 2462	. . . . . 6
31	1, 30	syl 17	. . . . 5
32	31	a1i 11	. . . 4
33		oveq1 6285	. . . . . . 7
34		3m1e2 10693	. . . . . . 7
35	33, 34	syl6eq 2459	. . . . . 6
36	35	oveq2d 6294	. . . . 5
37	36	eleq2d 2472	. . . 4
38		oveq2 6286	. . . . . 6
39	38	sumeq1d 13672	. . . . 5
40	38	sumeq1d 13672	. . . . 5
41	39, 40	eqeq12d 2424	. . . 4
42	32, 37, 41	3imtr4d 268	. . 3
43	42	adantld 465	. 2 $/\$
44		simprl 756	. . . 4 $/\$ $/\$
45		eluzle 11139	. . . . . . 7
46	45	adantl 464	. . . . . 6 $/\$
47		simpl 455	. . . . . 6 $/\$
48		3re 10650	. . . . . . 7
49		eluzelre 11137	. . . . . . . 8
50	49	adantl 464	. . . . . . 7 $/\$
51		ltlen 9717	. . . . . . 7 $/\$ $/\$
52	48, 50, 51	sylancr 661	. . . . . 6 $/\$ $/\$
53	46, 47, 52	mpbir2and 923	. . . . 5 $/\$
54	53	adantrr 715	. . . 4 $/\$ $/\$
55		simprr 758	. . . 4 $/\$ $/\$
56		fzssp1 11781	. . . . . . . . . . . . 13
57		simp3 999	. . . . . . . . . . . . 13 $/\$ $/\$
58	56, 57	sseldi 3440	. . . . . . . . . . . 12 $/\$ $/\$
59		eluzelz 11136	. . . . . . . . . . . . . . . 16
60	59	3ad2ant1 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	60	zcnd 11009	. . . . . . . . . . . . . 14 $/\$ $/\$
62		npcan 9865	. . . . . . . . . . . . . 14 $/\$
63	61, 10, 62	sylancl 660	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	oveq2d 6294	. . . . . . . . . . . 12 $/\$ $/\$
65	58, 64	eleqtrd 2492	. . . . . . . . . . 11 $/\$ $/\$
66		elfzelz 11742	. . . . . . . . . . 11
67	65, 66	syl 17	. . . . . . . . . 10 $/\$ $/\$
68	67	zred 11008	. . . . . . . . 9 $/\$ $/\$
69	68	ltp1d 10516	. . . . . . . 8 $/\$ $/\$
70		fzdisj 11766	. . . . . . . 8
71	69, 70	syl 17	. . . . . . 7 $/\$ $/\$
72		fzsplit 11765	. . . . . . . 8
73	65, 72	syl 17	. . . . . . 7 $/\$ $/\$
74		fzfid 12124	. . . . . . 7 $/\$ $/\$
75		eluzge3nn 11168	. . . . . . . . . . 11
76		2eluzge1 11173	. . . . . . . . . . . . 13
77		fzss1 11777	. . . . . . . . . . . . 13
78	76, 77	ax-mp 5	. . . . . . . . . . . 12
79	78	sseli 3438	. . . . . . . . . . 11
80	13	axlowdimlem10 24671	. . . . . . . . . . 11 $/\$
81	75, 79, 80	syl2an 475	. . . . . . . . . 10 $/\$
82		fzss1 11777	. . . . . . . . . . . 12
83	76, 82	ax-mp 5	. . . . . . . . . . 11
84	83	sseli 3438	. . . . . . . . . 10
85		fveecn 24622	. . . . . . . . . 10 $/\$
86	81, 84, 85	syl2an 475	. . . . . . . . 9 $/\$ $/\$
87	86	sqcld 12352	. . . . . . . 8 $/\$ $/\$
88	87	3adantl2 1154	. . . . . . 7 $/\$ $/\$ $/\$
89	71, 73, 74, 88	fsumsplit 13711	. . . . . 6 $/\$ $/\$
90		fzss1 11777	. . . . . . . . . . . . . . . 16
91	76, 90	ax-mp 5	. . . . . . . . . . . . . . 15
92	91	sseli 3438	. . . . . . . . . . . . . 14
93		elfzelz 11742	. . . . . . . . . . . . . . . . . . . 20
94	93	zred 11008	. . . . . . . . . . . . . . . . . . 19
95	94	3ad2ant3 1020	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
96	49	3ad2ant1 1018	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
97		peano2rem 9922	. . . . . . . . . . . . . . . . . . . 20
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		elfzle2 11744	. . . . . . . . . . . . . . . . . . . 20
100	99	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	96	ltm1d 10518	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
102	95, 98, 96, 100, 101	lelttrd 9774	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
103	95, 96, 102	ltled 9765	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	93	3ad2ant3 1020	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
105		eluz 11140	. . . . . . . . . . . . . . . . . 18 $/\$
106	104, 60, 105	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
107	103, 106	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
108		fzss2 11778	. . . . . . . . . . . . . . . 16
109	107, 108	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
110	109	sseld 3441	. . . . . . . . . . . . . 14 $/\$ $/\$
111	92, 110	syl5 30	. . . . . . . . . . . . 13 $/\$ $/\$
112	111	imp 427	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113		elfzelz 11742	. . . . . . . . . . . . . . 15
114	113	zred 11008	. . . . . . . . . . . . . 14
115	114	adantl 464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	95	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
117		peano2re 9787	. . . . . . . . . . . . . . . . 17
118	94, 117	syl 17	. . . . . . . . . . . . . . . 16
119	118	3ad2ant3 1020	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121		elfzle2 11744	. . . . . . . . . . . . . . 15
122	121	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	116	ltp1d 10516	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124	115, 116, 120, 122, 123	lelttrd 9774	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125	115, 124	ltned 9753	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	13	axlowdimlem12 24673	. . . . . . . . . . . 12 $/\$
127	112, 125, 126	syl2anc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$
128	127	sq0id 12306	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128	sumeq2dv 13674	. . . . . . . . 9 $/\$ $/\$
130		fzfi 12123	. . . . . . . . . . 11
131	130	olci 389	. . . . . . . . . 10 $\/$
132		sumz 13693	. . . . . . . . . 10 $\/$
133	131, 132	ax-mp 5	. . . . . . . . 9
134	129, 133	syl6eq 2459	. . . . . . . 8 $/\$ $/\$
135	104	peano2zd 11011	. . . . . . . . . . 11 $/\$ $/\$
136		sq1 12307	. . . . . . . . . . . . 13
137	16, 136	syl6eq 2459	. . . . . . . . . . . 12
138	137	fsum1 13713	. . . . . . . . . . 11 $/\$
139	135, 10, 138	sylancl 660	. . . . . . . . . 10 $/\$ $/\$
140		oveq2 6286	. . . . . . . . . . . 12
141	140	sumeq1d 13672	. . . . . . . . . . 11
142	141	eqeq1d 2404	. . . . . . . . . 10
143	139, 142	syl5ib 219	. . . . . . . . 9 $/\$ $/\$
144	104	adantl 464	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
145	144	zred 11008	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	60	adantl 464	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	146	zred 11008	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
148	147, 97	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	100	adantl 464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
150	147	ltm1d 10518	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	145, 148, 147, 149, 150	lelttrd 9774	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152		1red 9641	. . . . . . . . . . . . . . . . . . 19
153		2re 10646	. . . . . . . . . . . . . . . . . . . 20
154	153	a1i 11	. . . . . . . . . . . . . . . . . . 19
155		1le2 10790	. . . . . . . . . . . . . . . . . . . 20
156	155	a1i 11	. . . . . . . . . . . . . . . . . . 19
157		elfzle1 11743	. . . . . . . . . . . . . . . . . . 19
158	152, 154, 94, 156, 157	letrd 9773	. . . . . . . . . . . . . . . . . 18
159	158	3ad2ant3 1020	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
160	159	adantl 464	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
161		elnnz1 10931	. . . . . . . . . . . . . . . 16 $/\$
162	144, 160, 161	sylanbrc 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163	75	3ad2ant1 1018	. . . . . . . . . . . . . . . 16 $/\$ $/\$
164	163	adantl 464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
165		nnltp1le 10960	. . . . . . . . . . . . . . 15 $/\$
166	162, 164, 165	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	151, 166	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	135	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
169		eluz 11140	. . . . . . . . . . . . . 14 $/\$
170	168, 146, 169	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	167, 170	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172		simpr1 1003	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
173		simpr3 1005	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
174	172, 173, 81	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175	174	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	162	peano2nnd 10593	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		nnuz 11162	. . . . . . . . . . . . . . . . 17
178	176, 177	syl6eleq 2500	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
179		fzss1 11777	. . . . . . . . . . . . . . . 16
180	178, 179	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	180	sselda 3442	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	175, 181, 85	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
183	182	sqcld 12352	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
184	12	oveq1d 6293	. . . . . . . . . . . . 13
185	14	oveq1i 6288	. . . . . . . . . . . . . 14
186	185, 136	eqtri 2431	. . . . . . . . . . . . 13
187	184, 186	syl6eq 2459	. . . . . . . . . . . 12
188	171, 183, 187	fsum1p 13719	. . . . . . . . . . 11 $/\$ $/\$ $/\$
189	176	peano2nnd 10593	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
190	189, 177	syl6eleq 2500	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
191		fzss1 11777	. . . . . . . . . . . . . . . . . . 19
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
193	192	sselda 3442	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
194	145, 117	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	194	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
196		peano2re 9787	. . . . . . . . . . . . . . . . . . . 20
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
198		elfzelz 11742	. . . . . . . . . . . . . . . . . . . . 21
199	198	zred 11008	. . . . . . . . . . . . . . . . . . . 20
200	199	adantl 464	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
201	195	ltp1d 10516	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
202		elfzle1 11743	. . . . . . . . . . . . . . . . . . . 20
203	202	adantl 464	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
204	195, 197, 200, 201, 203	ltletrd 9776	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
205	195, 204	gtned 9752	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
206	193, 205, 126	syl2anc 659	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
207	206	sq0id 12306	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
208	207	sumeq2dv 13674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
209		fzfi 12123	. . . . . . . . . . . . . . . 16
210	209	olci 389	. . . . . . . . . . . . . . 15 $\/$
211		sumz 13693	. . . . . . . . . . . . . . 15 $\/$
212	210, 211	ax-mp 5	. . . . . . . . . . . . . 14
213	208, 212	syl6eq 2459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
214	213	oveq2d 6294	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
215		1p0e1 10689	. . . . . . . . . . . 12
216	214, 215	syl6eq 2459	. . . . . . . . . . 11 $/\$ $/\$ $/\$
217	188, 216	eqtrd 2443	. . . . . . . . . 10 $/\$ $/\$ $/\$
218	217	ex 432	. . . . . . . . 9 $/\$ $/\$
219	143, 218	pm2.61ine 2716	. . . . . . . 8 $/\$ $/\$
220	134, 219	oveq12d 6296	. . . . . . 7 $/\$ $/\$
221		0p1e1 10688	. . . . . . 7
222	220, 221	syl6eq 2459	. . . . . 6 $/\$ $/\$
223	89, 222	eqtrd 2443	. . . . 5 $/\$ $/\$
224		simp1 997	. . . . . . . 8 $/\$ $/\$
225		2lt3 10744	. . . . . . . . . 10
226	153, 48, 225	ltleii 9739	. . . . . . . . 9
227		2z 10937	. . . . . . . . . 10
228	227	eluz1i 11134	. . . . . . . . 9 $/\$
229	8, 226, 228	mpbir2an 921	. . . . . . . 8
230		uztrn 11143	. . . . . . . 8 $/\$
231	224, 229, 230	sylancl 660	. . . . . . 7 $/\$ $/\$
232		fveq2 5849	. . . . . . . 8
233	232	oveq1d 6293	. . . . . . 7
234	231, 88, 233	fsum1p 13719	. . . . . 6 $/\$ $/\$
235	59	adantr 463	. . . . . . . . . . . . . . 15 $/\$
236	235	zred 11008	. . . . . . . . . . . . . 14 $/\$
237		lttr 9692	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
238	153, 48, 237	mp3an12 1316	. . . . . . . . . . . . . . . . 17 $/\$
239	225, 238	mpani 674	. . . . . . . . . . . . . . . 16
240	49, 239	syl 17	. . . . . . . . . . . . . . 15
241	240	imp 427	. . . . . . . . . . . . . 14 $/\$
242		ltle 9704	. . . . . . . . . . . . . . 15 $/\$
243	153, 242	mpan 668	. . . . . . . . . . . . . 14
244	236, 241, 243	sylc 59	. . . . . . . . . . . . 13 $/\$
245	244, 155	jctil 535	. . . . . . . . . . . 12 $/\$ $/\$
246		1z 10935	. . . . . . . . . . . . . 14
247		elfz 11732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
248	227, 246, 247	mp3an12 1316	. . . . . . . . . . . . 13 $/\$
249	235, 248	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
250	245, 249	mpbird 232	. . . . . . . . . . 11 $/\$
251	250	3adant3 1017	. . . . . . . . . 10 $/\$ $/\$
252	94	ltp1d 10516	. . . . . . . . . . . . . 14
253	154, 94, 118, 157, 252	lelttrd 9774	. . . . . . . . . . . . 13
254	253	3ad2ant3 1020	. . . . . . . . . . . 12 $/\$ $/\$
255		ltne 9712	. . . . . . . . . . . 12 $/\$
256	153, 254, 255	sylancr 661	. . . . . . . . . . 11 $/\$ $/\$
257	256	necomd 2674	. . . . . . . . . 10 $/\$ $/\$
258	13	axlowdimlem12 24673	. . . . . . . . . 10 $/\$
259	251, 257, 258	syl2anc 659	. . . . . . . . 9 $/\$ $/\$
260	259	sq0id 12306	. . . . . . . 8 $/\$ $/\$
261	260	oveq1d 6293	. . . . . . 7 $/\$ $/\$
262	3	oveq1i 6288	. . . . . . . . 9
263	262	sumeq1i 13669	. . . . . . . 8
264	263	oveq2i 6289	. . . . . . 7
265	261, 264	syl6eqr 2461	. . . . . 6 $/\$ $/\$
266		fzfid 12124	. . . . . . . 8 $/\$ $/\$
267		3nn 10735	. . . . . . . . . . . . . 14
268	267, 177	eleqtri 2488	. . . . . . . . . . . . 13
269		fzss1 11777	. . . . . . . . . . . . 13
270	268, 269	ax-mp 5	. . . . . . . . . . . 12
271	270	sseli 3438	. . . . . . . . . . 11
272	81, 271, 85	syl2an 475	. . . . . . . . . 10 $/\$ $/\$
273	272	sqcld 12352	. . . . . . . . 9 $/\$ $/\$
274	273	3adantl2 1154	. . . . . . . 8 $/\$ $/\$ $/\$
275	266, 274	fsumcl 13704	. . . . . . 7 $/\$ $/\$
276	275	addid2d 9815	. . . . . 6 $/\$ $/\$
277	234, 265, 276	3eqtrrd 2448	. . . . 5 $/\$ $/\$
278		simpl 455	. . . . . . . . 9 $/\$
279	21	axlowdimlem7 24668	. . . . . . . . . . . 12
280	279	ad2antrr 724	. . . . . . . . . . 11 $/\$ $/\$
281	271	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
282		fveecn 24622	. . . . . . . . . . 11 $/\$
283	280, 281, 282	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$
284	283	sqcld 12352	. . . . . . . . 9 $/\$ $/\$
285		neg1sqe1 12308	. . . . . . . . . 10
286	24, 285	syl6eq 2459	. . . . . . . . 9
287	278, 284, 286	fsum1p 13719	. . . . . . . 8 $/\$
288		1re 9625	. . . . . . . . . . . . . . . . . 18
289		zaddcl 10945	. . . . . . . . . . . . . . . . . . . 20 $/\$
290	8, 246, 289	mp2an 670	. . . . . . . . . . . . . . . . . . 19
291	290	zrei 10911	. . . . . . . . . . . . . . . . . 18
292		1lt3 10745	. . . . . . . . . . . . . . . . . . 19
293	48	ltp1i 10489	. . . . . . . . . . . . . . . . . . 19
294	288, 48, 291	lttri 9742	. . . . . . . . . . . . . . . . . . 19 $/\$
295	292, 293, 294	mp2an 670	. . . . . . . . . . . . . . . . . 18
296	288, 291, 295	ltleii 9739	. . . . . . . . . . . . . . . . 17
297		eluz 11140	. . . . . . . . . . . . . . . . . 18 $/\$
298	246, 290, 297	mp2an 670	. . . . . . . . . . . . . . . . 17
299	296, 298	mpbir 209	. . . . . . . . . . . . . . . 16
300		fzss1 11777	. . . . . . . . . . . . . . . 16
301	299, 300	ax-mp 5	. . . . . . . . . . . . . . 15
302	301	sseli 3438	. . . . . . . . . . . . . 14
303	302	adantl 464	. . . . . . . . . . . . 13 $/\$ $/\$
304	48, 291	ltnlei 9737	. . . . . . . . . . . . . . . . . . 19
305	293, 304	mpbi 208	. . . . . . . . . . . . . . . . . 18
306	305	intnanr 916	. . . . . . . . . . . . . . . . 17 $/\$
307		elfz 11732	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
308	8, 290, 307	mp3an12 1316	. . . . . . . . . . . . . . . . . 18 $/\$
309	235, 308	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
310	306, 309	mtbiri 301	. . . . . . . . . . . . . . . 16 $/\$
311		eleq1 2474	. . . . . . . . . . . . . . . . 17
312	311	notbid 292	. . . . . . . . . . . . . . . 16
313	310, 312	syl5ibrcom 222	. . . . . . . . . . . . . . 15 $/\$
314	313	necon2ad 2616	. . . . . . . . . . . . . 14 $/\$
315	314	imp 427	. . . . . . . . . . . . 13 $/\$ $/\$
316	21	axlowdimlem9 24670	. . . . . . . . . . . . 13 $/\$
317	303, 315, 316	syl2anc 659	. . . . . . . . . . . 12 $/\$ $/\$
318	317	sq0id 12306	. . . . . . . . . . 11 $/\$ $/\$
319	318	sumeq2dv 13674	. . . . . . . . . 10 $/\$
320		fzfi 12123	. . . . . . . . . . . 12
321	320	olci 389	. . . . . . . . . . 11 $\/$
322		sumz 13693	. . . . . . . . . . 11 $\/$
323	321, 322	ax-mp 5	. . . . . . . . . 10
324	319, 323	syl6eq 2459	. . . . . . . . 9 $/\$
325	324	oveq2d 6294	. . . . . . . 8 $/\$
326	287, 325	eqtrd 2443	. . . . . . 7 $/\$
327	326, 215	syl6eq 2459	. . . . . 6 $/\$
328	327	3adant3 1017	. . . . 5 $/\$ $/\$
329	223, 277, 328	3eqtr4rd 2454	. . . 4 $/\$ $/\$
330	44, 54, 55, 329	syl3anc 1230	. . 3 $/\$ $/\$
331	330	ex 432	. 2 $/\$
332	43, 331	pm2.61ine 2716	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598 $\$ cdif 3411

cun 3412

cin 3413

wss 3414

c0 3738

csn 3972

cop 3978 class class class wbr 4395

cxp 4821

cfv 5569 (class class class)co 6278

cfn 7554

cc 9520

cr 9521

cc0 9522

c1 9523

caddc 9525

clt 9658

cle 9659

cmin 9841

cneg 9842

cn 10576

c2 10626

c3 10627

cz 10905

cuz 11127

cfz 11726

cexp 12210

csu 13657

cee 24608

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-inf2 8091 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 ax-pre-sup 9600

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-int 4228 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-se 4783 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-isom 5578 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-1o 7167 df-oadd 7171 df-er 7348 df-map 7459 df-en 7555 df-dom 7556 df-sdom 7557 df-fin 7558 df-sup 7935 df-oi 7969 df-card 8352 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-div 10248 df-nn 10577 df-2 10635 df-3 10636 df-n0 10837 df-z 10906 df-uz 11128 df-rp 11266 df-fz 11727 df-fzo 11855 df-seq 12152 df-exp 12211 df-hash 12453 df-cj 13081 df-re 13082 df-im 13083 df-sqrt 13217 df-abs 13218 df-clim 13460 df-sum 13658 df-ee 24611

This theorem is referenced by: axlowdimlem17 24678

W3C validator