bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 24268

Description: Lemma for bpos 24270. Evaluate

and show it is less than

. (Contributed by Mario Carneiro, 14-Mar-2014.)

**Hypotheses**
Ref	Expression
bposlem7.1
bposlem7.2

**Assertion**
Ref	Expression
bposlem8	; $/\$ ;

**Proof of Theorem bposlem8**
Step	Hyp	Ref	Expression
1		6nn0 10919	. . . . 5
2		4nn 10798	. . . . 5
3	1, 2	decnncl 11093	. . . 4 ;
4		fveq2 5888	. . . . . . . . . . . . . 14 ; ;
5		8cn 10723	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 12386	. . . . . . . . . . . . . . . . 17
7		8t8e64 11174	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2484	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5891	. . . . . . . . . . . . . . 15 ;
10		0re 9669	. . . . . . . . . . . . . . . . 17
11		8re 10722	. . . . . . . . . . . . . . . . 17
12		8pos 10738	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9783	. . . . . . . . . . . . . . . 16
14	11	sqrtsqi 13486	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2486	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2512	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5892	. . . . . . . . . . . 12 ;
19		8nn 10802	. . . . . . . . . . . . 13
20		nnrp 11340	. . . . . . . . . . . . 13
21		fveq2 5888	. . . . . . . . . . . . . . . . 17
22		cu2 12405	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5891	. . . . . . . . . . . . . . . . . 18
24		2rp 11336	. . . . . . . . . . . . . . . . . . 19
25		3z 10999	. . . . . . . . . . . . . . . . . . 19
26		relogexp 23594	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 683	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2486	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2512	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6333	. . . . . . . . . . . . . . 15
32		3cn 10712	. . . . . . . . . . . . . . . 16
33		2nn 10796	. . . . . . . . . . . . . . . . . 18
34		nnrp 11340	. . . . . . . . . . . . . . . . . 18
35		relogcl 23574	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9681	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10672	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10393	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2512	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6343	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5971	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2512	. . . . . . . . . . 11 ;
46	45	oveq2d 6331	. . . . . . . . . 10 ;
47		sqrt2re 14351	. . . . . . . . . . . . 13
48	47	recni 9681	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10377	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9678	. . . . . . . . . . 11
51		4cn 10715	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9854	. . . . . . . . . . . . . . 15
53		2re 10707	. . . . . . . . . . . . . . . . 17
54		0le2 10728	. . . . . . . . . . . . . . . . 17
55		remsqsqrt 13369	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 683	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6326	. . . . . . . . . . . . . . 15
58		4t2e8 10792	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2488	. . . . . . . . . . . . . 14
60	59	oveq2i 6326	. . . . . . . . . . . . 13
61	51, 48	mulcli 9674	. . . . . . . . . . . . . . 15
62		nnrp 11340	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrtcl 13377	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11353	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 683	. . . . . . . . . . . . . . . 16
68		rpne0 11346	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 11346	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10337	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1360	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 684	. . . . . . . . . . . . . 14
75		4ne0 10734	. . . . . . . . . . . . . . 15
76		divdiv1 10346	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1360	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 684	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2487	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10391	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2493	. . . . . . . . . . . 12
82	81	oveq1i 6325	. . . . . . . . . . 11
83	50, 82	eqtr3i 2486	. . . . . . . . . 10
84	46, 83	syl6eq 2512	. . . . . . . . 9 ;
85		oveq1 6322	. . . . . . . . . . . . . 14 ; ;
86		df-6 10700	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6326	. . . . . . . . . . . . . . . . 17
88		2exp6 15107	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10708	. . . . . . . . . . . . . . . . . 18
90		5nn0 10918	. . . . . . . . . . . . . . . . . 18
91		expp1 12311	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 683	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2492	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6325	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 12317	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 683	. . . . . . . . . . . . . . . . 17
97	96	nncni 10647	. . . . . . . . . . . . . . . 16
98		2ne0 10730	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10382	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2484	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2512	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5892	. . . . . . . . . . . 12 ;
103		nnrp 11340	. . . . . . . . . . . . 13
104		fveq2 5888	. . . . . . . . . . . . . . . . 17
105		5nn 10799	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10990	. . . . . . . . . . . . . . . . . 18
107		relogexp 23594	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 683	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2512	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6333	. . . . . . . . . . . . . . 15
112		5cn 10717	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10672	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10393	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2512	. . . . . . . . . . . . . 14
116		ovex 6343	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5971	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2512	. . . . . . . . . . 11 ;
120	119	oveq2d 6331	. . . . . . . . . 10 ;
121		9cn 10725	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10377	. . . . . . . . . . 11
123	112, 97, 113	divcli 10377	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9678	. . . . . . . . . 10
125	120, 124	syl6eqr 2514	. . . . . . . . 9 ;
126	84, 125	oveq12d 6333	. . . . . . . 8 ;
127	32, 51, 75	divcli 10377	. . . . . . . . . 10
128	127, 48, 71	divcli 10377	. . . . . . . . 9
129	122, 123	mulcli 9674	. . . . . . . . 9
130	128, 129, 37	adddiri 9680	. . . . . . . 8
131	126, 130	syl6eqr 2514	. . . . . . 7 ;
132		oveq2 6323	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5892	. . . . . . . . . 10 ; ;
134	3	nnrei 10646	. . . . . . . . . . . 12 ;
135	3	nngt0i 10671	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9783	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrtmulii 13498	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6326	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2484	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2512	. . . . . . . . 9 ;
141	140	oveq2d 6331	. . . . . . . 8 ;
142	48, 5	mulcli 9674	. . . . . . . . . 10
143		rpmulcl 11353	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 674	. . . . . . . . . . 11
145		rpne0 11346	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10315	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1373	. . . . . . . . 9
149	48, 5	mulcomi 9675	. . . . . . . . . . . 12
150	149	oveq2i 6326	. . . . . . . . . . 11
151		recdiv2 10348	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 684	. . . . . . . . . . 11
153	150, 152	eqtr4i 2487	. . . . . . . . . 10
154	153	oveq1i 6325	. . . . . . . . 9
155	148, 154	eqtri 2484	. . . . . . . 8
156	141, 155	syl6eq 2512	. . . . . . 7 ;
157	131, 156	oveq12d 6333	. . . . . 6 ;
158	128, 129	addcli 9673	. . . . . . 7
159	5, 38	reccli 10365	. . . . . . . 8
160	159, 48, 71	divcli 10377	. . . . . . 7
161	158, 160, 37	adddiri 9680	. . . . . 6
162	157, 161	syl6eqr 2514	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6343	. . . . 5
165	162, 163, 164	fvmpt 5971	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10711	. . . . . . . 8
168		4re 10714	. . . . . . . 8
169	167, 168, 75	redivcli 10402	. . . . . . 7
170	169, 47, 71	redivcli 10402	. . . . . 6
171		9re 10724	. . . . . . . 8
172	171, 168, 75	redivcli 10402	. . . . . . 7
173		5re 10716	. . . . . . . 8
174	96	nnrei 10646	. . . . . . . 8
175	173, 174, 113	redivcli 10402	. . . . . . 7
176	172, 175	remulcli 9683	. . . . . 6
177	170, 176	readdcli 9682	. . . . 5
178	11, 38	rereccli 10400	. . . . . 6
179	178, 47, 71	redivcli 10402	. . . . 5
180	177, 179	readdcli 9682	. . . 4
181	180, 36	remulcli 9683	. . 3
182	166, 181	eqeltri 2536	. 2 ;
183	128, 129, 160	add32i 9878	. . . . . 6
184		6cn 10719	. . . . . . . . . . 11
185		ax-1cn 9623	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10392	. . . . . . . . . 10
187		df-7 10701	. . . . . . . . . . 11
188	187	oveq1i 6325	. . . . . . . . . 10
189		divcan5 10337	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1360	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 684	. . . . . . . . . . . 12
192		3t2e6 10790	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9676	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9676	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6327	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2486	. . . . . . . . . . 11
197	196	oveq1i 6325	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2495	. . . . . . . . 9
199	198	oveq1i 6325	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10392	. . . . . . . 8
201		7cn 10721	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10390	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2492	. . . . . . 7
204	203	oveq1i 6325	. . . . . 6
205	183, 204	eqtri 2484	. . . . 5
206		4nn0 10917	. . . . . . . . . . . 12
207		9nn0 10922	. . . . . . . . . . . 12
208		0nn0 10913	. . . . . . . . . . . 12
209		9lt10 10841	. . . . . . . . . . . 12
210		4lt5 10811	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 11102	. . . . . . . . . . 11 ; ;
212		7t7e49 11167	. . . . . . . . . . 11 ;
213	56	oveq1i 6325	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9856	. . . . . . . . . . . 12
215		5t2e10 10793	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9676	. . . . . . . . . . . . . 14
217	216	oveq1i 6325	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9678	. . . . . . . . . . . . 13
219	90	dec0u 11095	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2492	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2492	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4445	. . . . . . . . . 10
223		7re 10720	. . . . . . . . . . . 12
224		7pos 10737	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9783	. . . . . . . . . . 11
226		nnrp 11340	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11353	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 683	. . . . . . . . . . . 12
230		rpge0 11343	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 11337	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10547	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 683	. . . . . . . . . 10
236	222, 235	mpbir 214	. . . . . . . . 9
237		rpgt0 11342	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10508	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1363	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 683	. . . . . . . . 9
242	236, 241	mpbir 214	. . . . . . . 8
243	223, 47, 71	redivcli 10402	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10564	. . . . . . . 8
245	242, 244	mpbi 213	. . . . . . 7
246		divsubdir 10331	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1363	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 683	. . . . . . . . 9
249		5p3e8 10777	. . . . . . . . . . . 12
250	249	oveq1i 6325	. . . . . . . . . . 11
251	112, 32	pncan3oi 9917	. . . . . . . . . . 11
252	250, 251	eqtr3i 2486	. . . . . . . . . 10
253	252	oveq1i 6325	. . . . . . . . 9
254	5, 38	dividi 10368	. . . . . . . . . 10
255	254	oveq1i 6325	. . . . . . . . 9
256	248, 253, 255	3eqtr3ri 2493	. . . . . . . 8
257		5lt8 10828	. . . . . . . . . . . . 13
258	11, 173	remulcli 9683	. . . . . . . . . . . . . 14
259	173, 11, 258	ltadd2i 9791	. . . . . . . . . . . . 13
260	257, 259	mpbi 213	. . . . . . . . . . . 12
261		df-9 10703	. . . . . . . . . . . . . 14
262	261	oveq1i 6325	. . . . . . . . . . . . 13
263	5, 185, 112	adddiri 9680	. . . . . . . . . . . . 13
264	112	mulid2i 9672	. . . . . . . . . . . . . 14
265	264	oveq2i 6326	. . . . . . . . . . . . 13
266	262, 263, 265	3eqtri 2488	. . . . . . . . . . . 12
267	86	oveq2i 6326	. . . . . . . . . . . . 13
268	5, 112, 185	adddii 9679	. . . . . . . . . . . . 13
269	5	mulid1i 9671	. . . . . . . . . . . . . 14
270	269	oveq2i 6326	. . . . . . . . . . . . 13
271	267, 268, 270	3eqtri 2488	. . . . . . . . . . . 12
272	260, 266, 271	3brtr4i 4445	. . . . . . . . . . 11
273	171, 173	remulcli 9683	. . . . . . . . . . . 12
274		6re 10718	. . . . . . . . . . . . 13
275	11, 274	remulcli 9683	. . . . . . . . . . . 12
276	168, 174	remulcli 9683	. . . . . . . . . . . 12
277	2, 96	nnmulcli 10661	. . . . . . . . . . . . 13
278	277	nngt0i 10671	. . . . . . . . . . . 12
279	273, 275, 276, 278	ltdiv1ii 10564	. . . . . . . . . . 11
280	272, 279	mpbi 213	. . . . . . . . . 10
281	121, 51, 112, 97, 75, 113	divmuldivi 10395	. . . . . . . . . 10
282		nnexpcl 12317	. . . . . . . . . . . . . 14 $/\$
283	33, 206, 282	mp2an 683	. . . . . . . . . . . . 13
284	283	nncni 10647	. . . . . . . . . . . 12
285	283	nnne0i 10672	. . . . . . . . . . . 12
286		divcan5 10337	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
287	32, 286	mp3an1 1360	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
288	5, 38, 284, 285, 287	mp4an 684	. . . . . . . . . . 11
289		df-4 10698	. . . . . . . . . . . . . . . 16
290	289	oveq2i 6326	. . . . . . . . . . . . . . 15
291		3nn0 10916	. . . . . . . . . . . . . . . 16
292		expp1 12311	. . . . . . . . . . . . . . . 16 $/\$
293	89, 291, 292	mp2an 683	. . . . . . . . . . . . . . 15
294	22	oveq1i 6325	. . . . . . . . . . . . . . 15
295	290, 293, 294	3eqtri 2488	. . . . . . . . . . . . . 14
296	295	oveq1i 6325	. . . . . . . . . . . . 13
297	5, 89, 32	mulassi 9678	. . . . . . . . . . . . 13
298	193	oveq2i 6326	. . . . . . . . . . . . 13
299	296, 297, 298	3eqtri 2488	. . . . . . . . . . . 12
300		4p3e7 10774	. . . . . . . . . . . . . . . 16
301		5p2e7 10776	. . . . . . . . . . . . . . . 16
302	112, 89	addcomi 9850	. . . . . . . . . . . . . . . 16
303	300, 301, 302	3eqtr2i 2490	. . . . . . . . . . . . . . 15
304	303	oveq2i 6326	. . . . . . . . . . . . . 14
305		expadd 12346	. . . . . . . . . . . . . . 15 $/\$ $/\$
306	89, 206, 291, 305	mp3an 1373	. . . . . . . . . . . . . 14
307		2nn0 10915	. . . . . . . . . . . . . . 15
308		expadd 12346	. . . . . . . . . . . . . . 15 $/\$ $/\$
309	89, 307, 90, 308	mp3an 1373	. . . . . . . . . . . . . 14
310	304, 306, 309	3eqtr3i 2492	. . . . . . . . . . . . 13
311	22	oveq2i 6326	. . . . . . . . . . . . 13
312		sq2 12403	. . . . . . . . . . . . . 14
313	312	oveq1i 6325	. . . . . . . . . . . . 13
314	310, 311, 313	3eqtr3i 2492	. . . . . . . . . . . 12
315	299, 314	oveq12i 6327	. . . . . . . . . . 11
316	288, 315	eqtr3i 2486	. . . . . . . . . 10
317	280, 281, 316	3brtr4i 4445	. . . . . . . . 9
318	167, 11, 38	redivcli 10402	. . . . . . . . . 10
319		1re 9668	. . . . . . . . . 10
320		ltsub2 10139	. . . . . . . . . 10 $/\$ $/\$
321	176, 318, 319, 320	mp3an 1373	. . . . . . . . 9
322	317, 321	mpbi 213	. . . . . . . 8
323	256, 322	eqbrtrri 4438	. . . . . . 7
324	243, 11, 38	redivcli 10402	. . . . . . . 8
325	173, 11, 38	redivcli 10402	. . . . . . . 8
326	319, 176	resubcli 9962	. . . . . . . 8
327	324, 325, 326	lttri 9786	. . . . . . 7 $/\$
328	245, 323, 327	mp2an 683	. . . . . 6
329	324, 176, 319	ltaddsubi 10203	. . . . . 6
330	328, 329	mpbir 214	. . . . 5
331	205, 330	eqbrtri 4436	. . . 4
332		1lt2 10805	. . . . . . 7
333		rplogcl 23602	. . . . . . 7 $/\$
334	53, 332, 333	mp2an 683	. . . . . 6
335		rpgt0 11342	. . . . . 6
336	334, 335	ax-mp 5	. . . . 5
337	180, 319, 36, 336	ltmul1ii 10563	. . . 4
338	331, 337	mpbi 213	. . 3
339	37	mulid2i 9672	. . . 4
340	339	eqcomi 2471	. . 3
341	338, 166, 340	3brtr4i 4445	. 2 ;
342	182, 341	pm3.2i 461	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 189 $/\$ wa 375

wceq 1455

wcel 1898

wne 2633 class class class wbr 4416

cmpt 4475

cfv 5601 (class class class)co 6315

cc 9563

cr 9564

cc0 9565

c1 9566

caddc 9568

cmul 9570

clt 9701

cle 9702

cmin 9886

cdiv 10297

cn 10637

c2 10687

c3 10688

c4 10689

c5 10690

c6 10691

c7 10692

c8 10693

c9 10694

c10 10695

cn0 10898

cz 10966 ;cdc 11080

crp 11331

cexp 12304

csqrt 13345

clog 23553

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4529 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-inf2 8172 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642 ax-pre-sup 9643 ax-addf 9644 ax-mulf 9645

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-fal 1461 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-iin 4295 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-of 6558 df-om 6720 df-1st 6820 df-2nd 6821 df-supp 6942 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-1o 7208 df-2o 7209 df-oadd 7212 df-er 7389 df-map 7500 df-pm 7501 df-ixp 7549 df-en 7596 df-dom 7597 df-sdom 7598 df-fin 7599 df-fsupp 7910 df-fi 7951 df-sup 7982 df-inf 7983 df-oi 8051 df-card 8399 df-cda 8624 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-div 10298 df-nn 10638 df-2 10696 df-3 10697 df-4 10698 df-5 10699 df-6 10700 df-7 10701 df-8 10702 df-9 10703 df-10 10704 df-n0 10899 df-z 10967 df-dec 11081 df-uz 11189 df-q 11294 df-rp 11332 df-xneg 11438 df-xadd 11439 df-xmul 11440 df-ioo 11668 df-ioc 11669 df-ico 11670 df-icc 11671 df-fz 11814 df-fzo 11947 df-fl 12060 df-mod 12129 df-seq 12246 df-exp 12305 df-fac 12492 df-bc 12520 df-hash 12548 df-shft 13179 df-cj 13211 df-re 13212 df-im 13213 df-sqrt 13347 df-abs 13348 df-limsup 13575 df-clim 13601 df-rlim 13602 df-sum 13802 df-ef 14170 df-sin 14172 df-cos 14173 df-pi 14175 df-struct 15172 df-ndx 15173 df-slot 15174 df-base 15175 df-sets 15176 df-ress 15177 df-plusg 15252 df-mulr 15253 df-starv 15254 df-sca 15255 df-vsca 15256 df-ip 15257 df-tset 15258 df-ple 15259 df-ds 15261 df-unif 15262 df-hom 15263 df-cco 15264 df-rest 15370 df-topn 15371 df-0g 15389 df-gsum 15390 df-topgen 15391 df-pt 15392 df-prds 15395 df-xrs 15449 df-qtop 15455 df-imas 15456 df-xps 15459 df-mre 15541 df-mrc 15542 df-acs 15544 df-mgm 16537 df-sgrp 16576 df-mnd 16586 df-submnd 16632 df-mulg 16725 df-cntz 17020 df-cmn 17481 df-psmet 19011 df-xmet 19012 df-met 19013 df-bl 19014 df-mopn 19015 df-fbas 19016 df-fg 19017 df-cnfld 19020 df-top 19970 df-bases 19971 df-topon 19972 df-topsp 19973 df-cld 20083 df-ntr 20084 df-cls 20085 df-nei 20163 df-lp 20201 df-perf 20202 df-cn 20292 df-cnp 20293 df-haus 20380 df-tx 20626 df-hmeo 20819 df-fil 20910 df-fm 21002 df-flim 21003 df-flf 21004 df-xms 21384 df-ms 21385 df-tms 21386 df-cncf 21959 df-limc 22870 df-dv 22871 df-log 23555

This theorem is referenced by: bposlem9 24269

W3C validator