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 25066

Description: Lemma for axlowdim 25070. 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 11836	. . . . . 6
2		oveq1 6315	. . . . . . . . . . 11
3		df-3 10691	. . . . . . . . . . 11
4	2, 3	syl6reqr 2524	. . . . . . . . . 10
5	4, 4	oveq12d 6326	. . . . . . . . 9
6	5	sumeq1d 13844	. . . . . . . 8
7	2, 3	syl6eqr 2523	. . . . . . . . . 10
8		3z 10994	. . . . . . . . . 10
9	7, 8	syl6eqel 2557	. . . . . . . . 9
10		ax-1cn 9615	. . . . . . . . . 10
11	10	sqcli 12393	. . . . . . . . 9
12		fveq2 5879	. . . . . . . . . . . 12
13		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
14	13	axlowdimlem11 25061	. . . . . . . . . . . 12
15	12, 14	syl6eq 2521	. . . . . . . . . . 11
16	15	oveq1d 6323	. . . . . . . . . 10
17	16	fsum1 13885	. . . . . . . . 9 $/\$
18	9, 11, 17	sylancl 675	. . . . . . . 8
19	6, 18	eqtrd 2505	. . . . . . 7
20		fveq2 5879	. . . . . . . . . . . 12
21		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
22	21	axlowdimlem8 25058	. . . . . . . . . . . 12
23	20, 22	syl6eq 2521	. . . . . . . . . . 11
24	23	oveq1d 6323	. . . . . . . . . 10
25		sqneg 12373	. . . . . . . . . . 11
26	10, 25	ax-mp 5	. . . . . . . . . 10
27	24, 26	syl6eq 2521	. . . . . . . . 9
28	27	fsum1 13885	. . . . . . . 8 $/\$
29	8, 11, 28	mp2an 686	. . . . . . 7
30	19, 29	syl6reqr 2524	. . . . . 6
31	1, 30	syl 17	. . . . 5
32	31	a1i 11	. . . 4
33		oveq1 6315	. . . . . . 7
34		3m1e2 10748	. . . . . . 7
35	33, 34	syl6eq 2521	. . . . . 6
36	35	oveq2d 6324	. . . . 5
37	36	eleq2d 2534	. . . 4
38		oveq2 6316	. . . . . 6
39	38	sumeq1d 13844	. . . . 5
40	38	sumeq1d 13844	. . . . 5
41	39, 40	eqeq12d 2486	. . . 4
42	32, 37, 41	3imtr4d 276	. . 3
43	42	adantld 474	. 2 $/\$
44		simprl 772	. . . 4 $/\$ $/\$
45		eluzle 11195	. . . . . . 7
46	45	adantl 473	. . . . . 6 $/\$
47		simpl 464	. . . . . 6 $/\$
48		3re 10705	. . . . . . 7
49		eluzelre 11193	. . . . . . . 8
50	49	adantl 473	. . . . . . 7 $/\$
51		ltlen 9753	. . . . . . 7 $/\$ $/\$
52	48, 50, 51	sylancr 676	. . . . . 6 $/\$ $/\$
53	46, 47, 52	mpbir2and 936	. . . . 5 $/\$
54	53	adantrr 731	. . . 4 $/\$ $/\$
55		simprr 774	. . . 4 $/\$ $/\$
56		fzssp1 11867	. . . . . . . . . . . . 13
57		simp3 1032	. . . . . . . . . . . . 13 $/\$ $/\$
58	56, 57	sseldi 3416	. . . . . . . . . . . 12 $/\$ $/\$
59		eluzelz 11192	. . . . . . . . . . . . . . . 16
60	59	3ad2ant1 1051	. . . . . . . . . . . . . . 15 $/\$ $/\$
61	60	zcnd 11064	. . . . . . . . . . . . . 14 $/\$ $/\$
62		npcan 9904	. . . . . . . . . . . . . 14 $/\$
63	61, 10, 62	sylancl 675	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	oveq2d 6324	. . . . . . . . . . . 12 $/\$ $/\$
65	58, 64	eleqtrd 2551	. . . . . . . . . . 11 $/\$ $/\$
66		elfzelz 11826	. . . . . . . . . . 11
67	65, 66	syl 17	. . . . . . . . . 10 $/\$ $/\$
68	67	zred 11063	. . . . . . . . 9 $/\$ $/\$
69	68	ltp1d 10559	. . . . . . . 8 $/\$ $/\$
70		fzdisj 11852	. . . . . . . 8
71	69, 70	syl 17	. . . . . . 7 $/\$ $/\$
72		fzsplit 11851	. . . . . . . 8
73	65, 72	syl 17	. . . . . . 7 $/\$ $/\$
74		fzfid 12224	. . . . . . 7 $/\$ $/\$
75		eluzge3nn 11224	. . . . . . . . . . 11
76		2eluzge1 11228	. . . . . . . . . . . . 13
77		fzss1 11863	. . . . . . . . . . . . 13
78	76, 77	ax-mp 5	. . . . . . . . . . . 12
79	78	sseli 3414	. . . . . . . . . . 11
80	13	axlowdimlem10 25060	. . . . . . . . . . 11 $/\$
81	75, 79, 80	syl2an 485	. . . . . . . . . 10 $/\$
82		fzss1 11863	. . . . . . . . . . . 12
83	76, 82	ax-mp 5	. . . . . . . . . . 11
84	83	sseli 3414	. . . . . . . . . 10
85		fveecn 25011	. . . . . . . . . 10 $/\$
86	81, 84, 85	syl2an 485	. . . . . . . . 9 $/\$ $/\$
87	86	sqcld 12452	. . . . . . . 8 $/\$ $/\$
88	87	3adantl2 1187	. . . . . . 7 $/\$ $/\$ $/\$
89	71, 73, 74, 88	fsumsplit 13883	. . . . . 6 $/\$ $/\$
90		fzss1 11863	. . . . . . . . . . . . . . . 16
91	76, 90	ax-mp 5	. . . . . . . . . . . . . . 15
92	91	sseli 3414	. . . . . . . . . . . . . 14
93		elfzelz 11826	. . . . . . . . . . . . . . . . . . . 20
94	93	zred 11063	. . . . . . . . . . . . . . . . . . 19
95	94	3ad2ant3 1053	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
96	49	3ad2ant1 1051	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
97		peano2rem 9961	. . . . . . . . . . . . . . . . . . . 20
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		elfzle2 11829	. . . . . . . . . . . . . . . . . . . 20
100	99	3ad2ant3 1053	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	96	ltm1d 10561	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
102	95, 98, 96, 100, 101	lelttrd 9810	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
103	95, 96, 102	ltled 9800	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
104	93	3ad2ant3 1053	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
105		eluz 11196	. . . . . . . . . . . . . . . . . 18 $/\$
106	104, 60, 105	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
107	103, 106	mpbird 240	. . . . . . . . . . . . . . . 16 $/\$ $/\$
108		fzss2 11864	. . . . . . . . . . . . . . . 16
109	107, 108	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
110	109	sseld 3417	. . . . . . . . . . . . . 14 $/\$ $/\$
111	92, 110	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$
112	111	imp 436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113		elfzelz 11826	. . . . . . . . . . . . . . 15
114	113	zred 11063	. . . . . . . . . . . . . 14
115	114	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
116	95	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
117		peano2re 9824	. . . . . . . . . . . . . . . . 17
118	94, 117	syl 17	. . . . . . . . . . . . . . . 16
119	118	3ad2ant3 1053	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121		elfzle2 11829	. . . . . . . . . . . . . . 15
122	121	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	116	ltp1d 10559	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124	115, 116, 120, 122, 123	lelttrd 9810	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125	115, 124	ltned 9788	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	13	axlowdimlem12 25062	. . . . . . . . . . . 12 $/\$
127	112, 125, 126	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
128	127	sq0id 12406	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128	sumeq2dv 13846	. . . . . . . . 9 $/\$ $/\$
130		fzfi 12223	. . . . . . . . . . 11
131	130	olci 398	. . . . . . . . . 10 $\/$
132		sumz 13865	. . . . . . . . . 10 $\/$
133	131, 132	ax-mp 5	. . . . . . . . 9
134	129, 133	syl6eq 2521	. . . . . . . 8 $/\$ $/\$
135	104	peano2zd 11066	. . . . . . . . . . 11 $/\$ $/\$
136		sq1 12407	. . . . . . . . . . . . 13
137	16, 136	syl6eq 2521	. . . . . . . . . . . 12
138	137	fsum1 13885	. . . . . . . . . . 11 $/\$
139	135, 10, 138	sylancl 675	. . . . . . . . . 10 $/\$ $/\$
140		oveq2 6316	. . . . . . . . . . . 12
141	140	sumeq1d 13844	. . . . . . . . . . 11
142	141	eqeq1d 2473	. . . . . . . . . 10
143	139, 142	syl5ib 227	. . . . . . . . 9 $/\$ $/\$
144	104	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
145	144	zred 11063	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	60	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	146	zred 11063	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
148	147, 97	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
149	100	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
150	147	ltm1d 10561	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	145, 148, 147, 149, 150	lelttrd 9810	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152		1red 9676	. . . . . . . . . . . . . . . . . . 19
153		2re 10701	. . . . . . . . . . . . . . . . . . . 20
154	153	a1i 11	. . . . . . . . . . . . . . . . . . 19
155		1le2 10846	. . . . . . . . . . . . . . . . . . . 20
156	155	a1i 11	. . . . . . . . . . . . . . . . . . 19
157		elfzle1 11828	. . . . . . . . . . . . . . . . . . 19
158	152, 154, 94, 156, 157	letrd 9809	. . . . . . . . . . . . . . . . . 18
159	158	3ad2ant3 1053	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
160	159	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
161		elnnz1 10987	. . . . . . . . . . . . . . . 16 $/\$
162	144, 160, 161	sylanbrc 677	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
163	75	3ad2ant1 1051	. . . . . . . . . . . . . . . 16 $/\$ $/\$
164	163	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
165		nnltp1le 11016	. . . . . . . . . . . . . . 15 $/\$
166	162, 164, 165	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167	151, 166	mpbid 215	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	135	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
169		eluz 11196	. . . . . . . . . . . . . 14 $/\$
170	168, 146, 169	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	167, 170	mpbird 240	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172		simpr1 1036	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
173		simpr3 1038	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
174	172, 173, 81	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175	174	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	162	peano2nnd 10648	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		nnuz 11218	. . . . . . . . . . . . . . . . 17
178	176, 177	syl6eleq 2559	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
179		fzss1 11863	. . . . . . . . . . . . . . . 16
180	178, 179	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	180	sselda 3418	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	175, 181, 85	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
183	182	sqcld 12452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
184	12	oveq1d 6323	. . . . . . . . . . . . 13
185	14	oveq1i 6318	. . . . . . . . . . . . . 14
186	185, 136	eqtri 2493	. . . . . . . . . . . . 13
187	184, 186	syl6eq 2521	. . . . . . . . . . . 12
188	171, 183, 187	fsum1p 13891	. . . . . . . . . . 11 $/\$ $/\$ $/\$
189	176	peano2nnd 10648	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
190	189, 177	syl6eleq 2559	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
191		fzss1 11863	. . . . . . . . . . . . . . . . . . 19
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
193	192	sselda 3418	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
194	145, 117	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	194	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
196		peano2re 9824	. . . . . . . . . . . . . . . . . . . 20
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
198		elfzelz 11826	. . . . . . . . . . . . . . . . . . . . 21
199	198	zred 11063	. . . . . . . . . . . . . . . . . . . 20
200	199	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
201	195	ltp1d 10559	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
202		elfzle1 11828	. . . . . . . . . . . . . . . . . . . 20
203	202	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
204	195, 197, 200, 201, 203	ltletrd 9812	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
205	195, 204	gtned 9787	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
206	193, 205, 126	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
207	206	sq0id 12406	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
208	207	sumeq2dv 13846	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
209		fzfi 12223	. . . . . . . . . . . . . . . 16
210	209	olci 398	. . . . . . . . . . . . . . 15 $\/$
211		sumz 13865	. . . . . . . . . . . . . . 15 $\/$
212	210, 211	ax-mp 5	. . . . . . . . . . . . . 14
213	208, 212	syl6eq 2521	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
214	213	oveq2d 6324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
215		1p0e1 10744	. . . . . . . . . . . 12
216	214, 215	syl6eq 2521	. . . . . . . . . . 11 $/\$ $/\$ $/\$
217	188, 216	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $/\$
218	217	ex 441	. . . . . . . . 9 $/\$ $/\$
219	143, 218	pm2.61ine 2726	. . . . . . . 8 $/\$ $/\$
220	134, 219	oveq12d 6326	. . . . . . 7 $/\$ $/\$
221		0p1e1 10743	. . . . . . 7
222	220, 221	syl6eq 2521	. . . . . 6 $/\$ $/\$
223	89, 222	eqtrd 2505	. . . . 5 $/\$ $/\$
224		simp1 1030	. . . . . . . 8 $/\$ $/\$
225		2lt3 10800	. . . . . . . . . 10
226	153, 48, 225	ltleii 9775	. . . . . . . . 9
227		2z 10993	. . . . . . . . . 10
228	227	eluz1i 11190	. . . . . . . . 9 $/\$
229	8, 226, 228	mpbir2an 934	. . . . . . . 8
230		uztrn 11199	. . . . . . . 8 $/\$
231	224, 229, 230	sylancl 675	. . . . . . 7 $/\$ $/\$
232		fveq2 5879	. . . . . . . 8
233	232	oveq1d 6323	. . . . . . 7
234	231, 88, 233	fsum1p 13891	. . . . . 6 $/\$ $/\$
235	59	adantr 472	. . . . . . . . . . . . . . 15 $/\$
236	235	zred 11063	. . . . . . . . . . . . . 14 $/\$
237		lttr 9728	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
238	153, 48, 237	mp3an12 1380	. . . . . . . . . . . . . . . . 17 $/\$
239	225, 238	mpani 690	. . . . . . . . . . . . . . . 16
240	49, 239	syl 17	. . . . . . . . . . . . . . 15
241	240	imp 436	. . . . . . . . . . . . . 14 $/\$
242		ltle 9740	. . . . . . . . . . . . . . 15 $/\$
243	153, 242	mpan 684	. . . . . . . . . . . . . 14
244	236, 241, 243	sylc 61	. . . . . . . . . . . . 13 $/\$
245	244, 155	jctil 546	. . . . . . . . . . . 12 $/\$ $/\$
246		1z 10991	. . . . . . . . . . . . . 14
247		elfz 11816	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
248	227, 246, 247	mp3an12 1380	. . . . . . . . . . . . 13 $/\$
249	235, 248	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
250	245, 249	mpbird 240	. . . . . . . . . . 11 $/\$
251	250	3adant3 1050	. . . . . . . . . 10 $/\$ $/\$
252	94	ltp1d 10559	. . . . . . . . . . . . . 14
253	154, 94, 118, 157, 252	lelttrd 9810	. . . . . . . . . . . . 13
254	253	3ad2ant3 1053	. . . . . . . . . . . 12 $/\$ $/\$
255		ltne 9748	. . . . . . . . . . . 12 $/\$
256	153, 254, 255	sylancr 676	. . . . . . . . . . 11 $/\$ $/\$
257	256	necomd 2698	. . . . . . . . . 10 $/\$ $/\$
258	13	axlowdimlem12 25062	. . . . . . . . . 10 $/\$
259	251, 257, 258	syl2anc 673	. . . . . . . . 9 $/\$ $/\$
260	259	sq0id 12406	. . . . . . . 8 $/\$ $/\$
261	260	oveq1d 6323	. . . . . . 7 $/\$ $/\$
262	3	oveq1i 6318	. . . . . . . . 9
263	262	sumeq1i 13841	. . . . . . . 8
264	263	oveq2i 6319	. . . . . . 7
265	261, 264	syl6eqr 2523	. . . . . 6 $/\$ $/\$
266		fzfid 12224	. . . . . . . 8 $/\$ $/\$
267		3nn 10791	. . . . . . . . . . . . . 14
268	267, 177	eleqtri 2547	. . . . . . . . . . . . 13
269		fzss1 11863	. . . . . . . . . . . . 13
270	268, 269	ax-mp 5	. . . . . . . . . . . 12
271	270	sseli 3414	. . . . . . . . . . 11
272	81, 271, 85	syl2an 485	. . . . . . . . . 10 $/\$ $/\$
273	272	sqcld 12452	. . . . . . . . 9 $/\$ $/\$
274	273	3adantl2 1187	. . . . . . . 8 $/\$ $/\$ $/\$
275	266, 274	fsumcl 13876	. . . . . . 7 $/\$ $/\$
276	275	addid2d 9852	. . . . . 6 $/\$ $/\$
277	234, 265, 276	3eqtrrd 2510	. . . . 5 $/\$ $/\$
278		simpl 464	. . . . . . . . 9 $/\$
279	21	axlowdimlem7 25057	. . . . . . . . . . . 12
280	279	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$
281	271	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
282		fveecn 25011	. . . . . . . . . . 11 $/\$
283	280, 281, 282	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$
284	283	sqcld 12452	. . . . . . . . 9 $/\$ $/\$
285		neg1sqe1 12408	. . . . . . . . . 10
286	24, 285	syl6eq 2521	. . . . . . . . 9
287	278, 284, 286	fsum1p 13891	. . . . . . . 8 $/\$
288		1re 9660	. . . . . . . . . . . . . . . . . 18
289		zaddcl 11001	. . . . . . . . . . . . . . . . . . . 20 $/\$
290	8, 246, 289	mp2an 686	. . . . . . . . . . . . . . . . . . 19
291	290	zrei 10967	. . . . . . . . . . . . . . . . . 18
292		1lt3 10801	. . . . . . . . . . . . . . . . . . 19
293	48	ltp1i 10532	. . . . . . . . . . . . . . . . . . 19
294	288, 48, 291	lttri 9778	. . . . . . . . . . . . . . . . . . 19 $/\$
295	292, 293, 294	mp2an 686	. . . . . . . . . . . . . . . . . 18
296	288, 291, 295	ltleii 9775	. . . . . . . . . . . . . . . . 17
297		eluz 11196	. . . . . . . . . . . . . . . . . 18 $/\$
298	246, 290, 297	mp2an 686	. . . . . . . . . . . . . . . . 17
299	296, 298	mpbir 214	. . . . . . . . . . . . . . . 16
300		fzss1 11863	. . . . . . . . . . . . . . . 16
301	299, 300	ax-mp 5	. . . . . . . . . . . . . . 15
302	301	sseli 3414	. . . . . . . . . . . . . 14
303	302	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$
304	48, 291	ltnlei 9773	. . . . . . . . . . . . . . . . . . 19
305	293, 304	mpbi 213	. . . . . . . . . . . . . . . . . 18
306	305	intnanr 929	. . . . . . . . . . . . . . . . 17 $/\$
307		elfz 11816	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
308	8, 290, 307	mp3an12 1380	. . . . . . . . . . . . . . . . . 18 $/\$
309	235, 308	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
310	306, 309	mtbiri 310	. . . . . . . . . . . . . . . 16 $/\$
311		eleq1 2537	. . . . . . . . . . . . . . . . 17
312	311	notbid 301	. . . . . . . . . . . . . . . 16
313	310, 312	syl5ibrcom 230	. . . . . . . . . . . . . . 15 $/\$
314	313	necon2ad 2658	. . . . . . . . . . . . . 14 $/\$
315	314	imp 436	. . . . . . . . . . . . 13 $/\$ $/\$
316	21	axlowdimlem9 25059	. . . . . . . . . . . . 13 $/\$
317	303, 315, 316	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$
318	317	sq0id 12406	. . . . . . . . . . 11 $/\$ $/\$
319	318	sumeq2dv 13846	. . . . . . . . . 10 $/\$
320		fzfi 12223	. . . . . . . . . . . 12
321	320	olci 398	. . . . . . . . . . 11 $\/$
322		sumz 13865	. . . . . . . . . . 11 $\/$
323	321, 322	ax-mp 5	. . . . . . . . . 10
324	319, 323	syl6eq 2521	. . . . . . . . 9 $/\$
325	324	oveq2d 6324	. . . . . . . 8 $/\$
326	287, 325	eqtrd 2505	. . . . . . 7 $/\$
327	326, 215	syl6eq 2521	. . . . . 6 $/\$
328	327	3adant3 1050	. . . . 5 $/\$ $/\$
329	223, 277, 328	3eqtr4rd 2516	. . . 4 $/\$ $/\$
330	44, 54, 55, 329	syl3anc 1292	. . 3 $/\$ $/\$
331	330	ex 441	. 2 $/\$
332	43, 331	pm2.61ine 2726	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

csn 3959

cop 3965 class class class wbr 4395

cxp 4837

cfv 5589 (class class class)co 6308

cfn 7587

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

clt 9693

cle 9694

cmin 9880

cneg 9881

cn 10631

c2 10681

c3 10682

cz 10961

cuz 11182

cfz 11810

cexp 12310

csu 13829

cee 24997

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-oi 8043 df-card 8391 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-fz 11811 df-fzo 11943 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-sum 13830 df-ee 25000

This theorem is referenced by: axlowdimlem17 25067

W3C validator