axlowdimlem16 - Metamath Proof Explorer

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

Theorem axlowdimlem16 24980

Description: Lemma for axlowdim 24984. 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 11807	. . . . . 6
2		oveq1 6295	. . . . . . . . . . 11
3		df-3 10666	. . . . . . . . . . 11
4	2, 3	syl6reqr 2503	. . . . . . . . . 10
5	4, 4	oveq12d 6306	. . . . . . . . 9
6	5	sumeq1d 13760	. . . . . . . 8
7	2, 3	syl6eqr 2502	. . . . . . . . . 10
8		3z 10967	. . . . . . . . . 10
9	7, 8	syl6eqel 2536	. . . . . . . . 9
10		ax-1cn 9594	. . . . . . . . . 10
11	10	sqcli 12352	. . . . . . . . 9
12		fveq2 5863	. . . . . . . . . . . 12
13		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
14	13	axlowdimlem11 24975	. . . . . . . . . . . 12
15	12, 14	syl6eq 2500	. . . . . . . . . . 11
16	15	oveq1d 6303	. . . . . . . . . 10
17	16	fsum1 13801	. . . . . . . . 9 $/\$
18	9, 11, 17	sylancl 667	. . . . . . . 8
19	6, 18	eqtrd 2484	. . . . . . 7
20		fveq2 5863	. . . . . . . . . . . 12
21		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
22	21	axlowdimlem8 24972	. . . . . . . . . . . 12
23	20, 22	syl6eq 2500	. . . . . . . . . . 11
24	23	oveq1d 6303	. . . . . . . . . 10
25		sqneg 12332	. . . . . . . . . . 11
26	10, 25	ax-mp 5	. . . . . . . . . 10
27	24, 26	syl6eq 2500	. . . . . . . . 9
28	27	fsum1 13801	. . . . . . . 8 $/\$
29	8, 11, 28	mp2an 677	. . . . . . 7
30	19, 29	syl6reqr 2503	. . . . . 6
31	1, 30	syl 17	. . . . 5
32	31	a1i 11	. . . 4
33		oveq1 6295	. . . . . . 7
34		3m1e2 10723	. . . . . . 7
35	33, 34	syl6eq 2500	. . . . . 6
36	35	oveq2d 6304	. . . . 5
37	36	eleq2d 2513	. . . 4
38		oveq2 6296	. . . . . 6
39	38	sumeq1d 13760	. . . . 5
40	38	sumeq1d 13760	. . . . 5
41	39, 40	eqeq12d 2465	. . . 4
42	32, 37, 41	3imtr4d 272	. . 3
43	42	adantld 469	. 2 $/\$
44		simprl 763	. . . 4 $/\$ $/\$
45		eluzle 11168	. . . . . . 7
46	45	adantl 468	. . . . . 6 $/\$
47		simpl 459	. . . . . 6 $/\$
48		3re 10680	. . . . . . 7
49		eluzelre 11166	. . . . . . . 8
50	49	adantl 468	. . . . . . 7 $/\$
51		ltlen 9732	. . . . . . 7 $/\$ $/\$
52	48, 50, 51	sylancr 668	. . . . . 6 $/\$ $/\$
53	46, 47, 52	mpbir2and 932	. . . . 5 $/\$
54	53	adantrr 722	. . . 4 $/\$ $/\$
55		simprr 765	. . . 4 $/\$ $/\$
56		fzssp1 11838	. . . . . . . . . . . . 13
57		simp3 1009	. . . . . . . . . . . . 13 $/\$ $/\$
58	56, 57	sseldi 3429	. . . . . . . . . . . 12 $/\$ $/\$
59		eluzelz 11165	. . . . . . . . . . . . . . . 16
60	59	3ad2ant1 1028	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	60	zcnd 11038	. . . . . . . . . . . . . 14 $/\$ $/\$
62		npcan 9881	. . . . . . . . . . . . . 14 $/\$
63	61, 10, 62	sylancl 667	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	oveq2d 6304	. . . . . . . . . . . 12 $/\$ $/\$
65	58, 64	eleqtrd 2530	. . . . . . . . . . 11 $/\$ $/\$
66		elfzelz 11797	. . . . . . . . . . 11
67	65, 66	syl 17	. . . . . . . . . 10 $/\$ $/\$
68	67	zred 11037	. . . . . . . . 9 $/\$ $/\$
69	68	ltp1d 10534	. . . . . . . 8 $/\$ $/\$
70		fzdisj 11823	. . . . . . . 8
71	69, 70	syl 17	. . . . . . 7 $/\$ $/\$
72		fzsplit 11822	. . . . . . . 8
73	65, 72	syl 17	. . . . . . 7 $/\$ $/\$
74		fzfid 12183	. . . . . . 7 $/\$ $/\$
75		eluzge3nn 11197	. . . . . . . . . . 11
76		2eluzge1 11202	. . . . . . . . . . . . 13
77		fzss1 11834	. . . . . . . . . . . . 13
78	76, 77	ax-mp 5	. . . . . . . . . . . 12
79	78	sseli 3427	. . . . . . . . . . 11
80	13	axlowdimlem10 24974	. . . . . . . . . . 11 $/\$
81	75, 79, 80	syl2an 480	. . . . . . . . . 10 $/\$
82		fzss1 11834	. . . . . . . . . . . 12
83	76, 82	ax-mp 5	. . . . . . . . . . 11
84	83	sseli 3427	. . . . . . . . . 10
85		fveecn 24925	. . . . . . . . . 10 $/\$
86	81, 84, 85	syl2an 480	. . . . . . . . 9 $/\$ $/\$
87	86	sqcld 12411	. . . . . . . 8 $/\$ $/\$
88	87	3adantl2 1164	. . . . . . 7 $/\$ $/\$ $/\$
89	71, 73, 74, 88	fsumsplit 13799	. . . . . 6 $/\$ $/\$
90		fzss1 11834	. . . . . . . . . . . . . . . 16
91	76, 90	ax-mp 5	. . . . . . . . . . . . . . 15
92	91	sseli 3427	. . . . . . . . . . . . . 14
93		elfzelz 11797	. . . . . . . . . . . . . . . . . . . 20
94	93	zred 11037	. . . . . . . . . . . . . . . . . . 19
95	94	3ad2ant3 1030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
96	49	3ad2ant1 1028	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
97		peano2rem 9938	. . . . . . . . . . . . . . . . . . . 20
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		elfzle2 11800	. . . . . . . . . . . . . . . . . . . 20
100	99	3ad2ant3 1030	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	96	ltm1d 10536	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
102	95, 98, 96, 100, 101	lelttrd 9790	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
103	95, 96, 102	ltled 9780	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	93	3ad2ant3 1030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
105		eluz 11169	. . . . . . . . . . . . . . . . . 18 $/\$
106	104, 60, 105	syl2anc 666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
107	103, 106	mpbird 236	. . . . . . . . . . . . . . . 16 $/\$ $/\$
108		fzss2 11835	. . . . . . . . . . . . . . . 16
109	107, 108	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
110	109	sseld 3430	. . . . . . . . . . . . . 14 $/\$ $/\$
111	92, 110	syl5 33	. . . . . . . . . . . . 13 $/\$ $/\$
112	111	imp 431	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113		elfzelz 11797	. . . . . . . . . . . . . . 15
114	113	zred 11037	. . . . . . . . . . . . . 14
115	114	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	95	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
117		peano2re 9803	. . . . . . . . . . . . . . . . 17
118	94, 117	syl 17	. . . . . . . . . . . . . . . 16
119	118	3ad2ant3 1030	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121		elfzle2 11800	. . . . . . . . . . . . . . 15
122	121	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	116	ltp1d 10534	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124	115, 116, 120, 122, 123	lelttrd 9790	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125	115, 124	ltned 9768	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	13	axlowdimlem12 24976	. . . . . . . . . . . 12 $/\$
127	112, 125, 126	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
128	127	sq0id 12365	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128	sumeq2dv 13762	. . . . . . . . 9 $/\$ $/\$
130		fzfi 12182	. . . . . . . . . . 11
131	130	olci 393	. . . . . . . . . 10 $\/$
132		sumz 13781	. . . . . . . . . 10 $\/$
133	131, 132	ax-mp 5	. . . . . . . . 9
134	129, 133	syl6eq 2500	. . . . . . . 8 $/\$ $/\$
135	104	peano2zd 11040	. . . . . . . . . . 11 $/\$ $/\$
136		sq1 12366	. . . . . . . . . . . . 13
137	16, 136	syl6eq 2500	. . . . . . . . . . . 12
138	137	fsum1 13801	. . . . . . . . . . 11 $/\$
139	135, 10, 138	sylancl 667	. . . . . . . . . 10 $/\$ $/\$
140		oveq2 6296	. . . . . . . . . . . 12
141	140	sumeq1d 13760	. . . . . . . . . . 11
142	141	eqeq1d 2452	. . . . . . . . . 10
143	139, 142	syl5ib 223	. . . . . . . . 9 $/\$ $/\$
144	104	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
145	144	zred 11037	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	60	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	146	zred 11037	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
148	147, 97	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	100	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
150	147	ltm1d 10536	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	145, 148, 147, 149, 150	lelttrd 9790	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152		1red 9655	. . . . . . . . . . . . . . . . . . 19
153		2re 10676	. . . . . . . . . . . . . . . . . . . 20
154	153	a1i 11	. . . . . . . . . . . . . . . . . . 19
155		1le2 10820	. . . . . . . . . . . . . . . . . . . 20
156	155	a1i 11	. . . . . . . . . . . . . . . . . . 19
157		elfzle1 11799	. . . . . . . . . . . . . . . . . . 19
158	152, 154, 94, 156, 157	letrd 9789	. . . . . . . . . . . . . . . . . 18
159	158	3ad2ant3 1030	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
160	159	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
161		elnnz1 10960	. . . . . . . . . . . . . . . 16 $/\$
162	144, 160, 161	sylanbrc 669	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163	75	3ad2ant1 1028	. . . . . . . . . . . . . . . 16 $/\$ $/\$
164	163	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
165		nnltp1le 10989	. . . . . . . . . . . . . . 15 $/\$
166	162, 164, 165	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	151, 166	mpbid 214	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	135	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
169		eluz 11169	. . . . . . . . . . . . . 14 $/\$
170	168, 146, 169	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	167, 170	mpbird 236	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172		simpr1 1013	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
173		simpr3 1015	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
174	172, 173, 81	syl2anc 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175	174	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	162	peano2nnd 10623	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		nnuz 11191	. . . . . . . . . . . . . . . . 17
178	176, 177	syl6eleq 2538	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
179		fzss1 11834	. . . . . . . . . . . . . . . 16
180	178, 179	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	180	sselda 3431	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	175, 181, 85	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
183	182	sqcld 12411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
184	12	oveq1d 6303	. . . . . . . . . . . . 13
185	14	oveq1i 6298	. . . . . . . . . . . . . 14
186	185, 136	eqtri 2472	. . . . . . . . . . . . 13
187	184, 186	syl6eq 2500	. . . . . . . . . . . 12
188	171, 183, 187	fsum1p 13807	. . . . . . . . . . 11 $/\$ $/\$ $/\$
189	176	peano2nnd 10623	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
190	189, 177	syl6eleq 2538	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
191		fzss1 11834	. . . . . . . . . . . . . . . . . . 19
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
193	192	sselda 3431	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
194	145, 117	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	194	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
196		peano2re 9803	. . . . . . . . . . . . . . . . . . . 20
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
198		elfzelz 11797	. . . . . . . . . . . . . . . . . . . . 21
199	198	zred 11037	. . . . . . . . . . . . . . . . . . . 20
200	199	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
201	195	ltp1d 10534	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
202		elfzle1 11799	. . . . . . . . . . . . . . . . . . . 20
203	202	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
204	195, 197, 200, 201, 203	ltletrd 9792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
205	195, 204	gtned 9767	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
206	193, 205, 126	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
207	206	sq0id 12365	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
208	207	sumeq2dv 13762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
209		fzfi 12182	. . . . . . . . . . . . . . . 16
210	209	olci 393	. . . . . . . . . . . . . . 15 $\/$
211		sumz 13781	. . . . . . . . . . . . . . 15 $\/$
212	210, 211	ax-mp 5	. . . . . . . . . . . . . 14
213	208, 212	syl6eq 2500	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
214	213	oveq2d 6304	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
215		1p0e1 10719	. . . . . . . . . . . 12
216	214, 215	syl6eq 2500	. . . . . . . . . . 11 $/\$ $/\$ $/\$
217	188, 216	eqtrd 2484	. . . . . . . . . 10 $/\$ $/\$ $/\$
218	217	ex 436	. . . . . . . . 9 $/\$ $/\$
219	143, 218	pm2.61ine 2706	. . . . . . . 8 $/\$ $/\$
220	134, 219	oveq12d 6306	. . . . . . 7 $/\$ $/\$
221		0p1e1 10718	. . . . . . 7
222	220, 221	syl6eq 2500	. . . . . 6 $/\$ $/\$
223	89, 222	eqtrd 2484	. . . . 5 $/\$ $/\$
224		simp1 1007	. . . . . . . 8 $/\$ $/\$
225		2lt3 10774	. . . . . . . . . 10
226	153, 48, 225	ltleii 9754	. . . . . . . . 9
227		2z 10966	. . . . . . . . . 10
228	227	eluz1i 11163	. . . . . . . . 9 $/\$
229	8, 226, 228	mpbir2an 930	. . . . . . . 8
230		uztrn 11172	. . . . . . . 8 $/\$
231	224, 229, 230	sylancl 667	. . . . . . 7 $/\$ $/\$
232		fveq2 5863	. . . . . . . 8
233	232	oveq1d 6303	. . . . . . 7
234	231, 88, 233	fsum1p 13807	. . . . . 6 $/\$ $/\$
235	59	adantr 467	. . . . . . . . . . . . . . 15 $/\$
236	235	zred 11037	. . . . . . . . . . . . . 14 $/\$
237		lttr 9707	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
238	153, 48, 237	mp3an12 1353	. . . . . . . . . . . . . . . . 17 $/\$
239	225, 238	mpani 681	. . . . . . . . . . . . . . . 16
240	49, 239	syl 17	. . . . . . . . . . . . . . 15
241	240	imp 431	. . . . . . . . . . . . . 14 $/\$
242		ltle 9719	. . . . . . . . . . . . . . 15 $/\$
243	153, 242	mpan 675	. . . . . . . . . . . . . 14
244	236, 241, 243	sylc 62	. . . . . . . . . . . . 13 $/\$
245	244, 155	jctil 540	. . . . . . . . . . . 12 $/\$ $/\$
246		1z 10964	. . . . . . . . . . . . . 14
247		elfz 11787	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
248	227, 246, 247	mp3an12 1353	. . . . . . . . . . . . 13 $/\$
249	235, 248	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
250	245, 249	mpbird 236	. . . . . . . . . . 11 $/\$
251	250	3adant3 1027	. . . . . . . . . 10 $/\$ $/\$
252	94	ltp1d 10534	. . . . . . . . . . . . . 14
253	154, 94, 118, 157, 252	lelttrd 9790	. . . . . . . . . . . . 13
254	253	3ad2ant3 1030	. . . . . . . . . . . 12 $/\$ $/\$
255		ltne 9727	. . . . . . . . . . . 12 $/\$
256	153, 254, 255	sylancr 668	. . . . . . . . . . 11 $/\$ $/\$
257	256	necomd 2678	. . . . . . . . . 10 $/\$ $/\$
258	13	axlowdimlem12 24976	. . . . . . . . . 10 $/\$
259	251, 257, 258	syl2anc 666	. . . . . . . . 9 $/\$ $/\$
260	259	sq0id 12365	. . . . . . . 8 $/\$ $/\$
261	260	oveq1d 6303	. . . . . . 7 $/\$ $/\$
262	3	oveq1i 6298	. . . . . . . . 9
263	262	sumeq1i 13757	. . . . . . . 8
264	263	oveq2i 6299	. . . . . . 7
265	261, 264	syl6eqr 2502	. . . . . 6 $/\$ $/\$
266		fzfid 12183	. . . . . . . 8 $/\$ $/\$
267		3nn 10765	. . . . . . . . . . . . . 14
268	267, 177	eleqtri 2526	. . . . . . . . . . . . 13
269		fzss1 11834	. . . . . . . . . . . . 13
270	268, 269	ax-mp 5	. . . . . . . . . . . 12
271	270	sseli 3427	. . . . . . . . . . 11
272	81, 271, 85	syl2an 480	. . . . . . . . . 10 $/\$ $/\$
273	272	sqcld 12411	. . . . . . . . 9 $/\$ $/\$
274	273	3adantl2 1164	. . . . . . . 8 $/\$ $/\$ $/\$
275	266, 274	fsumcl 13792	. . . . . . 7 $/\$ $/\$
276	275	addid2d 9831	. . . . . 6 $/\$ $/\$
277	234, 265, 276	3eqtrrd 2489	. . . . 5 $/\$ $/\$
278		simpl 459	. . . . . . . . 9 $/\$
279	21	axlowdimlem7 24971	. . . . . . . . . . . 12
280	279	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$
281	271	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
282		fveecn 24925	. . . . . . . . . . 11 $/\$
283	280, 281, 282	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$
284	283	sqcld 12411	. . . . . . . . 9 $/\$ $/\$
285		neg1sqe1 12367	. . . . . . . . . 10
286	24, 285	syl6eq 2500	. . . . . . . . 9
287	278, 284, 286	fsum1p 13807	. . . . . . . 8 $/\$
288		1re 9639	. . . . . . . . . . . . . . . . . 18
289		zaddcl 10974	. . . . . . . . . . . . . . . . . . . 20 $/\$
290	8, 246, 289	mp2an 677	. . . . . . . . . . . . . . . . . . 19
291	290	zrei 10940	. . . . . . . . . . . . . . . . . 18
292		1lt3 10775	. . . . . . . . . . . . . . . . . . 19
293	48	ltp1i 10507	. . . . . . . . . . . . . . . . . . 19
294	288, 48, 291	lttri 9757	. . . . . . . . . . . . . . . . . . 19 $/\$
295	292, 293, 294	mp2an 677	. . . . . . . . . . . . . . . . . 18
296	288, 291, 295	ltleii 9754	. . . . . . . . . . . . . . . . 17
297		eluz 11169	. . . . . . . . . . . . . . . . . 18 $/\$
298	246, 290, 297	mp2an 677	. . . . . . . . . . . . . . . . 17
299	296, 298	mpbir 213	. . . . . . . . . . . . . . . 16
300		fzss1 11834	. . . . . . . . . . . . . . . 16
301	299, 300	ax-mp 5	. . . . . . . . . . . . . . 15
302	301	sseli 3427	. . . . . . . . . . . . . 14
303	302	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$
304	48, 291	ltnlei 9752	. . . . . . . . . . . . . . . . . . 19
305	293, 304	mpbi 212	. . . . . . . . . . . . . . . . . 18
306	305	intnanr 925	. . . . . . . . . . . . . . . . 17 $/\$
307		elfz 11787	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
308	8, 290, 307	mp3an12 1353	. . . . . . . . . . . . . . . . . 18 $/\$
309	235, 308	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
310	306, 309	mtbiri 305	. . . . . . . . . . . . . . . 16 $/\$
311		eleq1 2516	. . . . . . . . . . . . . . . . 17
312	311	notbid 296	. . . . . . . . . . . . . . . 16
313	310, 312	syl5ibrcom 226	. . . . . . . . . . . . . . 15 $/\$
314	313	necon2ad 2638	. . . . . . . . . . . . . 14 $/\$
315	314	imp 431	. . . . . . . . . . . . 13 $/\$ $/\$
316	21	axlowdimlem9 24973	. . . . . . . . . . . . 13 $/\$
317	303, 315, 316	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$
318	317	sq0id 12365	. . . . . . . . . . 11 $/\$ $/\$
319	318	sumeq2dv 13762	. . . . . . . . . 10 $/\$
320		fzfi 12182	. . . . . . . . . . . 12
321	320	olci 393	. . . . . . . . . . 11 $\/$
322		sumz 13781	. . . . . . . . . . 11 $\/$
323	321, 322	ax-mp 5	. . . . . . . . . 10
324	319, 323	syl6eq 2500	. . . . . . . . 9 $/\$
325	324	oveq2d 6304	. . . . . . . 8 $/\$
326	287, 325	eqtrd 2484	. . . . . . 7 $/\$
327	326, 215	syl6eq 2500	. . . . . 6 $/\$
328	327	3adant3 1027	. . . . 5 $/\$ $/\$
329	223, 277, 328	3eqtr4rd 2495	. . . 4 $/\$ $/\$
330	44, 54, 55, 329	syl3anc 1267	. . 3 $/\$ $/\$
331	330	ex 436	. 2 $/\$
332	43, 331	pm2.61ine 2706	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621 $\$ cdif 3400

cun 3401

cin 3402

wss 3403

c0 3730

csn 3967

cop 3973 class class class wbr 4401

cxp 4831

cfv 5581 (class class class)co 6288

cfn 7566

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

clt 9672

cle 9673

cmin 9857

cneg 9858

cn 10606

c2 10656

c3 10657

cz 10934

cuz 11156

cfz 11781

cexp 12269

csu 13745

cee 24911

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-map 7471 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-oi 8022 df-card 8370 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-fz 11782 df-fzo 11913 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-sum 13746 df-ee 24914

This theorem is referenced by: axlowdimlem17 24981

W3C validator