axlowdimlem16 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > axlowdimlem16		Unicode version

Theorem axlowdimlem16 25800

Description: Lemma for axlowdim 25804. 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 11024	. . . . . 6
2		oveq1 6047	. . . . . . . . . . 11
3		df-3 10015	. . . . . . . . . . 11
4	2, 3	syl6reqr 2455	. . . . . . . . . 10
5	4, 4	oveq12d 6058	. . . . . . . . 9
6	5	sumeq1d 12450	. . . . . . . 8
7	2, 3	syl6eqr 2454	. . . . . . . . . 10
8		3nn 10090	. . . . . . . . . . 11
9	8	nnzi 10261	. . . . . . . . . 10
10	7, 9	syl6eqel 2492	. . . . . . . . 9
11		ax-1cn 9004	. . . . . . . . . 10
12	11	sqcli 11417	. . . . . . . . 9
13		fveq2 5687	. . . . . . . . . . . 12
14		axlowdimlem16.2	. . . . . . . . . . . . 13 $\$
15	14	axlowdimlem11 25795	. . . . . . . . . . . 12
16	13, 15	syl6eq 2452	. . . . . . . . . . 11
17	16	oveq1d 6055	. . . . . . . . . 10
18	17	fsum1 12490	. . . . . . . . 9 $/\$
19	10, 12, 18	sylancl 644	. . . . . . . 8
20	6, 19	eqtrd 2436	. . . . . . 7
21		fveq2 5687	. . . . . . . . . . . 12
22		axlowdimlem16.1	. . . . . . . . . . . . 13 $\$
23	22	axlowdimlem8 25792	. . . . . . . . . . . 12
24	21, 23	syl6eq 2452	. . . . . . . . . . 11
25	24	oveq1d 6055	. . . . . . . . . 10
26		sqneg 11397	. . . . . . . . . . 11
27	11, 26	ax-mp 8	. . . . . . . . . 10
28	25, 27	syl6eq 2452	. . . . . . . . 9
29	28	fsum1 12490	. . . . . . . 8 $/\$
30	9, 12, 29	mp2an 654	. . . . . . 7
31	20, 30	syl6reqr 2455	. . . . . 6
32	1, 31	syl 16	. . . . 5
33	32	a1i 11	. . . 4
34		oveq1 6047	. . . . . . 7
35		3m1e2 10052	. . . . . . 7
36	34, 35	syl6eq 2452	. . . . . 6
37	36	oveq2d 6056	. . . . 5
38	37	eleq2d 2471	. . . 4
39		oveq2 6048	. . . . . 6
40	39	sumeq1d 12450	. . . . 5
41	39	sumeq1d 12450	. . . . 5
42	40, 41	eqeq12d 2418	. . . 4
43	33, 38, 42	3imtr4d 260	. . 3
44	43	adantld 454	. 2 $/\$
45		simprl 733	. . . 4 $/\$ $/\$
46		eluzle 10454	. . . . . . 7
47	46	adantl 453	. . . . . 6 $/\$
48		simpl 444	. . . . . 6 $/\$
49		3re 10027	. . . . . . 7
50		eluzelre 10453	. . . . . . . 8
51	50	adantl 453	. . . . . . 7 $/\$
52		ltlen 9131	. . . . . . 7 $/\$ $/\$
53	49, 51, 52	sylancr 645	. . . . . 6 $/\$ $/\$
54	47, 48, 53	mpbir2and 889	. . . . 5 $/\$
55	54	adantrr 698	. . . 4 $/\$ $/\$
56		simprr 734	. . . 4 $/\$ $/\$
57		fzssp1 11051	. . . . . . . . . . . . 13
58		simp3 959	. . . . . . . . . . . . 13 $/\$ $/\$
59	57, 58	sseldi 3306	. . . . . . . . . . . 12 $/\$ $/\$
60		eluzelz 10452	. . . . . . . . . . . . . . . 16
61	60	3ad2ant1 978	. . . . . . . . . . . . . . 15 $/\$ $/\$
62	61	zcnd 10332	. . . . . . . . . . . . . 14 $/\$ $/\$
63		npcan 9270	. . . . . . . . . . . . . 14 $/\$
64	62, 11, 63	sylancl 644	. . . . . . . . . . . . 13 $/\$ $/\$
65	64	oveq2d 6056	. . . . . . . . . . . 12 $/\$ $/\$
66	59, 65	eleqtrd 2480	. . . . . . . . . . 11 $/\$ $/\$
67		elfzelz 11015	. . . . . . . . . . 11
68	66, 67	syl 16	. . . . . . . . . 10 $/\$ $/\$
69	68	zred 10331	. . . . . . . . 9 $/\$ $/\$
70	69	ltp1d 9897	. . . . . . . 8 $/\$ $/\$
71		fzdisj 11034	. . . . . . . 8
72	70, 71	syl 16	. . . . . . 7 $/\$ $/\$
73		fzsplit 11033	. . . . . . . 8
74	66, 73	syl 16	. . . . . . 7 $/\$ $/\$
75		fzfid 11267	. . . . . . 7 $/\$ $/\$
76		uznnssnn 10480	. . . . . . . . . . . . 13
77	8, 76	ax-mp 8	. . . . . . . . . . . 12
78	77	sseli 3304	. . . . . . . . . . 11
79		2nn 10089	. . . . . . . . . . . . . 14
80		nnuz 10477	. . . . . . . . . . . . . 14
81	79, 80	eleqtri 2476	. . . . . . . . . . . . 13
82		fzss1 11047	. . . . . . . . . . . . 13
83	81, 82	ax-mp 8	. . . . . . . . . . . 12
84	83	sseli 3304	. . . . . . . . . . 11
85	14	axlowdimlem10 25794	. . . . . . . . . . 11 $/\$
86	78, 84, 85	syl2an 464	. . . . . . . . . 10 $/\$
87		fzss1 11047	. . . . . . . . . . . 12
88	81, 87	ax-mp 8	. . . . . . . . . . 11
89	88	sseli 3304	. . . . . . . . . 10
90		fveecn 25745	. . . . . . . . . 10 $/\$
91	86, 89, 90	syl2an 464	. . . . . . . . 9 $/\$ $/\$
92	91	sqcld 11476	. . . . . . . 8 $/\$ $/\$
93	92	3adantl2 1114	. . . . . . 7 $/\$ $/\$ $/\$
94	72, 74, 75, 93	fsumsplit 12488	. . . . . 6 $/\$ $/\$
95		fzss1 11047	. . . . . . . . . . . . . . . 16
96	81, 95	ax-mp 8	. . . . . . . . . . . . . . 15
97	96	sseli 3304	. . . . . . . . . . . . . 14
98		elfzelz 11015	. . . . . . . . . . . . . . . . . . . 20
99	98	zred 10331	. . . . . . . . . . . . . . . . . . 19
100	99	3ad2ant3 980	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
101	50	3ad2ant1 978	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102		peano2rem 9323	. . . . . . . . . . . . . . . . . . . 20
103	101, 102	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104		elfzle2 11017	. . . . . . . . . . . . . . . . . . . 20
105	104	3ad2ant3 980	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
106	101	ltm1d 9899	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
107	100, 103, 101, 105, 106	lelttrd 9184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
108	100, 101, 107	ltled 9177	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
109	98	3ad2ant3 980	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
110		eluz 10455	. . . . . . . . . . . . . . . . . 18 $/\$
111	109, 61, 110	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
112	108, 111	mpbird 224	. . . . . . . . . . . . . . . 16 $/\$ $/\$
113		fzss2 11048	. . . . . . . . . . . . . . . 16
114	112, 113	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	114	sseld 3307	. . . . . . . . . . . . . 14 $/\$ $/\$
116	97, 115	syl5 30	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	imp 419	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		elfzelz 11015	. . . . . . . . . . . . . . 15
119	118	zred 10331	. . . . . . . . . . . . . 14
120	119	adantl 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	100	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
122		peano2re 9195	. . . . . . . . . . . . . . . . 17
123	99, 122	syl 16	. . . . . . . . . . . . . . . 16
124	123	3ad2ant3 980	. . . . . . . . . . . . . . 15 $/\$ $/\$
125	124	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
126		elfzle2 11017	. . . . . . . . . . . . . . 15
127	126	adantl 453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
128	121	ltp1d 9897	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
129	120, 121, 125, 127, 128	lelttrd 9184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	120, 129	ltned 9165	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	14	axlowdimlem12 25796	. . . . . . . . . . . 12 $/\$
132	117, 130, 131	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
133	132	sq0id 11430	. . . . . . . . . 10 $/\$ $/\$ $/\$
134	133	sumeq2dv 12452	. . . . . . . . 9 $/\$ $/\$
135		fzfi 11266	. . . . . . . . . . 11
136	135	olci 381	. . . . . . . . . 10 $\/$
137		sumz 12471	. . . . . . . . . 10 $\/$
138	136, 137	ax-mp 8	. . . . . . . . 9
139	134, 138	syl6eq 2452	. . . . . . . 8 $/\$ $/\$
140	109	peano2zd 10334	. . . . . . . . . . 11 $/\$ $/\$
141		sq1 11431	. . . . . . . . . . . . 13
142	17, 141	syl6eq 2452	. . . . . . . . . . . 12
143	142	fsum1 12490	. . . . . . . . . . 11 $/\$
144	140, 11, 143	sylancl 644	. . . . . . . . . 10 $/\$ $/\$
145		oveq2 6048	. . . . . . . . . . . 12
146	145	sumeq1d 12450	. . . . . . . . . . 11
147	146	eqeq1d 2412	. . . . . . . . . 10
148	144, 147	syl5ib 211	. . . . . . . . 9 $/\$ $/\$
149	109	adantl 453	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
150	149	zred 10331	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
151	61	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
152	151	zred 10331	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
153	152, 102	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
154	105	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
155	152	ltm1d 9899	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
156	150, 153, 152, 154, 155	lelttrd 9184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
157		1re 9046	. . . . . . . . . . . . . . . . . . . 20
158	157	a1i 11	. . . . . . . . . . . . . . . . . . 19
159		2re 10025	. . . . . . . . . . . . . . . . . . . 20
160	159	a1i 11	. . . . . . . . . . . . . . . . . . 19
161		1lt2 10098	. . . . . . . . . . . . . . . . . . . . 21
162	157, 159, 161	ltleii 9152	. . . . . . . . . . . . . . . . . . . 20
163	162	a1i 11	. . . . . . . . . . . . . . . . . . 19
164		elfzle1 11016	. . . . . . . . . . . . . . . . . . 19
165	158, 160, 99, 163, 164	letrd 9183	. . . . . . . . . . . . . . . . . 18
166	165	3ad2ant3 980	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
167	166	adantl 453	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
168		elnnz1 10263	. . . . . . . . . . . . . . . 16 $/\$
169	149, 167, 168	sylanbrc 646	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
170	78	3ad2ant1 978	. . . . . . . . . . . . . . . 16 $/\$ $/\$
171	170	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
172		nnltp1le 10286	. . . . . . . . . . . . . . 15 $/\$
173	169, 171, 172	syl2anc 643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
174	156, 173	mpbid 202	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
175	140	adantl 453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
176		eluz 10455	. . . . . . . . . . . . . 14 $/\$
177	175, 151, 176	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	174, 177	mpbird 224	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179		simpr1 963	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		simpr3 965	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	179, 180, 86	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	181	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	169	peano2nnd 9973	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
184	183, 80	syl6eleq 2494	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
185		fzss1 11047	. . . . . . . . . . . . . . . 16
186	184, 185	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
187	186	sselda 3308	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
188	182, 187, 90	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
189	188	sqcld 11476	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
190	13	oveq1d 6055	. . . . . . . . . . . . 13
191	15	oveq1i 6050	. . . . . . . . . . . . . 14
192	191, 141	eqtri 2424	. . . . . . . . . . . . 13
193	190, 192	syl6eq 2452	. . . . . . . . . . . 12
194	178, 189, 193	fsum1p 12494	. . . . . . . . . . 11 $/\$ $/\$ $/\$
195	183	peano2nnd 9973	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
196	195, 80	syl6eleq 2494	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
197		fzss1 11047	. . . . . . . . . . . . . . . . . . 19
198	196, 197	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
199	198	sselda 3308	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
200	150, 122	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
201	200	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
202		peano2re 9195	. . . . . . . . . . . . . . . . . . . 20
203	201, 202	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
204		elfzelz 11015	. . . . . . . . . . . . . . . . . . . . 21
205	204	zred 10331	. . . . . . . . . . . . . . . . . . . 20
206	205	adantl 453	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
207	201	ltp1d 9897	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
208		elfzle1 11016	. . . . . . . . . . . . . . . . . . . 20
209	208	adantl 453	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
210	201, 203, 206, 207, 209	ltletrd 9186	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
211	201, 210	gtned 9164	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
212	199, 211, 131	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
213	212	sq0id 11430	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
214	213	sumeq2dv 12452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215		fzfi 11266	. . . . . . . . . . . . . . . 16
216	215	olci 381	. . . . . . . . . . . . . . 15 $\/$
217		sumz 12471	. . . . . . . . . . . . . . 15 $\/$
218	216, 217	ax-mp 8	. . . . . . . . . . . . . 14
219	214, 218	syl6eq 2452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
220	219	oveq2d 6056	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
221	11	addid1i 9209	. . . . . . . . . . . 12
222	220, 221	syl6eq 2452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	194, 222	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	ex 424	. . . . . . . . 9 $/\$ $/\$
225	148, 224	pm2.61ine 2643	. . . . . . . 8 $/\$ $/\$
226	139, 225	oveq12d 6058	. . . . . . 7 $/\$ $/\$
227		0p1e1 10049	. . . . . . 7
228	226, 227	syl6eq 2452	. . . . . 6 $/\$ $/\$
229	94, 228	eqtrd 2436	. . . . 5 $/\$ $/\$
230		simp1 957	. . . . . . . 8 $/\$ $/\$
231		2lt3 10099	. . . . . . . . . 10
232	159, 49, 231	ltleii 9152	. . . . . . . . 9
233		2z 10268	. . . . . . . . . 10
234	233	eluz1i 10451	. . . . . . . . 9 $/\$
235	9, 232, 234	mpbir2an 887	. . . . . . . 8
236		uztrn 10458	. . . . . . . 8 $/\$
237	230, 235, 236	sylancl 644	. . . . . . 7 $/\$ $/\$
238		fveq2 5687	. . . . . . . 8
239	238	oveq1d 6055	. . . . . . 7
240	237, 93, 239	fsum1p 12494	. . . . . 6 $/\$ $/\$
241	60	adantr 452	. . . . . . . . . . . . . . 15 $/\$
242	241	zred 10331	. . . . . . . . . . . . . 14 $/\$
243		lttr 9108	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
244	159, 49, 243	mp3an12 1269	. . . . . . . . . . . . . . . . 17 $/\$
245	231, 244	mpani 658	. . . . . . . . . . . . . . . 16
246	50, 245	syl 16	. . . . . . . . . . . . . . 15
247	246	imp 419	. . . . . . . . . . . . . 14 $/\$
248		ltle 9119	. . . . . . . . . . . . . . 15 $/\$
249	159, 248	mpan 652	. . . . . . . . . . . . . 14
250	242, 247, 249	sylc 58	. . . . . . . . . . . . 13 $/\$
251	250, 162	jctil 524	. . . . . . . . . . . 12 $/\$ $/\$
252		1z 10267	. . . . . . . . . . . . . 14
253		elfz 11005	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
254	233, 252, 253	mp3an12 1269	. . . . . . . . . . . . 13 $/\$
255	241, 254	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
256	251, 255	mpbird 224	. . . . . . . . . . 11 $/\$
257	256	3adant3 977	. . . . . . . . . 10 $/\$ $/\$
258	99	ltp1d 9897	. . . . . . . . . . . . . 14
259	160, 99, 123, 164, 258	lelttrd 9184	. . . . . . . . . . . . 13
260	259	3ad2ant3 980	. . . . . . . . . . . 12 $/\$ $/\$
261		ltne 9126	. . . . . . . . . . . 12 $/\$
262	159, 260, 261	sylancr 645	. . . . . . . . . . 11 $/\$ $/\$
263	262	necomd 2650	. . . . . . . . . 10 $/\$ $/\$
264	14	axlowdimlem12 25796	. . . . . . . . . 10 $/\$
265	257, 263, 264	syl2anc 643	. . . . . . . . 9 $/\$ $/\$
266	265	sq0id 11430	. . . . . . . 8 $/\$ $/\$
267	266	oveq1d 6055	. . . . . . 7 $/\$ $/\$
268	3	oveq1i 6050	. . . . . . . . 9
269	268	sumeq1i 12447	. . . . . . . 8
270	269	oveq2i 6051	. . . . . . 7
271	267, 270	syl6eqr 2454	. . . . . 6 $/\$ $/\$
272		fzfid 11267	. . . . . . . 8 $/\$ $/\$
273	8, 80	eleqtri 2476	. . . . . . . . . . . . 13
274		fzss1 11047	. . . . . . . . . . . . 13
275	273, 274	ax-mp 8	. . . . . . . . . . . 12
276	275	sseli 3304	. . . . . . . . . . 11
277	86, 276, 90	syl2an 464	. . . . . . . . . 10 $/\$ $/\$
278	277	sqcld 11476	. . . . . . . . 9 $/\$ $/\$
279	278	3adantl2 1114	. . . . . . . 8 $/\$ $/\$ $/\$
280	272, 279	fsumcl 12482	. . . . . . 7 $/\$ $/\$
281	280	addid2d 9223	. . . . . 6 $/\$ $/\$
282	240, 271, 281	3eqtrrd 2441	. . . . 5 $/\$ $/\$
283		simpl 444	. . . . . . . . 9 $/\$
284	22	axlowdimlem7 25791	. . . . . . . . . . . 12
285	284	ad2antrr 707	. . . . . . . . . . 11 $/\$ $/\$
286	276	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
287		fveecn 25745	. . . . . . . . . . 11 $/\$
288	285, 286, 287	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$
289	288	sqcld 11476	. . . . . . . . 9 $/\$ $/\$
290	27, 141	eqtri 2424	. . . . . . . . . 10
291	25, 290	syl6eq 2452	. . . . . . . . 9
292	283, 289, 291	fsum1p 12494	. . . . . . . 8 $/\$
293		zaddcl 10273	. . . . . . . . . . . . . . . . . . . 20 $/\$
294	9, 252, 293	mp2an 654	. . . . . . . . . . . . . . . . . . 19
295	294	zrei 10244	. . . . . . . . . . . . . . . . . 18
296		1lt3 10100	. . . . . . . . . . . . . . . . . . 19
297	49	ltp1i 9870	. . . . . . . . . . . . . . . . . . 19
298	157, 49, 295	lttri 9155	. . . . . . . . . . . . . . . . . . 19 $/\$
299	296, 297, 298	mp2an 654	. . . . . . . . . . . . . . . . . 18
300	157, 295, 299	ltleii 9152	. . . . . . . . . . . . . . . . 17
301		eluz 10455	. . . . . . . . . . . . . . . . . 18 $/\$
302	252, 294, 301	mp2an 654	. . . . . . . . . . . . . . . . 17
303	300, 302	mpbir 201	. . . . . . . . . . . . . . . 16
304		fzss1 11047	. . . . . . . . . . . . . . . 16
305	303, 304	ax-mp 8	. . . . . . . . . . . . . . 15
306	305	sseli 3304	. . . . . . . . . . . . . 14
307	306	adantl 453	. . . . . . . . . . . . 13 $/\$ $/\$
308	49, 295	ltnlei 9150	. . . . . . . . . . . . . . . . . . 19
309	297, 308	mpbi 200	. . . . . . . . . . . . . . . . . 18
310	309	intnanr 882	. . . . . . . . . . . . . . . . 17 $/\$
311		elfz 11005	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
312	9, 294, 311	mp3an12 1269	. . . . . . . . . . . . . . . . . 18 $/\$
313	241, 312	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
314	310, 313	mtbiri 295	. . . . . . . . . . . . . . . 16 $/\$
315		eleq1 2464	. . . . . . . . . . . . . . . . 17
316	315	notbid 286	. . . . . . . . . . . . . . . 16
317	314, 316	syl5ibrcom 214	. . . . . . . . . . . . . . 15 $/\$
318	317	necon2ad 2615	. . . . . . . . . . . . . 14 $/\$
319	318	imp 419	. . . . . . . . . . . . 13 $/\$ $/\$
320	22	axlowdimlem9 25793	. . . . . . . . . . . . 13 $/\$
321	307, 319, 320	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$
322	321	sq0id 11430	. . . . . . . . . . 11 $/\$ $/\$
323	322	sumeq2dv 12452	. . . . . . . . . 10 $/\$
324		fzfi 11266	. . . . . . . . . . . 12
325	324	olci 381	. . . . . . . . . . 11 $\/$
326		sumz 12471	. . . . . . . . . . 11 $\/$
327	325, 326	ax-mp 8	. . . . . . . . . 10
328	323, 327	syl6eq 2452	. . . . . . . . 9 $/\$
329	328	oveq2d 6056	. . . . . . . 8 $/\$
330	292, 329	eqtrd 2436	. . . . . . 7 $/\$
331	330, 221	syl6eq 2452	. . . . . 6 $/\$
332	331	3adant3 977	. . . . 5 $/\$ $/\$
333	229, 282, 332	3eqtr4rd 2447	. . . 4 $/\$ $/\$
334	45, 55, 56, 333	syl3anc 1184	. . 3 $/\$ $/\$
335	334	ex 424	. 2 $/\$
336	44, 335	pm2.61ine 2643	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567 $\$ cdif 3277

cun 3278

cin 3279

wss 3280

c0 3588

csn 3774

cop 3777 class class class wbr 4172

cxp 4835

cfv 5413 (class class class)co 6040

cfn 7068

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

clt 9076

cle 9077

cmin 9247

cneg 9248

cn 9956

c2 10005

c3 10006

cz 10238

cuz 10444

cfz 10999

cexp 11337

csu 12434

cee 25731

This theorem is referenced by: axlowdimlem17 25801

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435 df-ee 25734

W3C validator