bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 23322

Description: Lemma for bpos 23324. 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 10816	. . . . 5
2		4nn 10695	. . . . 5
3	1, 2	decnncl 10989	. . . 4 ;
4		fveq2 5866	. . . . . . . . . . . . . 14 ; ;
5		8cn 10621	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 12215	. . . . . . . . . . . . . . . . 17
7		8t8e64 11070	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2496	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5869	. . . . . . . . . . . . . . 15 ;
10		0re 9596	. . . . . . . . . . . . . . . . 17
11		8re 10620	. . . . . . . . . . . . . . . . 17
12		8pos 10636	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9707	. . . . . . . . . . . . . . . 16
14	11	sqrtsqi 13170	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2498	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2524	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5870	. . . . . . . . . . . 12 ;
19		8nn 10699	. . . . . . . . . . . . 13
20		nnrp 11229	. . . . . . . . . . . . 13
21		fveq2 5866	. . . . . . . . . . . . . . . . 17
22		cu2 12234	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5869	. . . . . . . . . . . . . . . . . 18
24		2rp 11225	. . . . . . . . . . . . . . . . . . 19
25		3z 10897	. . . . . . . . . . . . . . . . . . 19
26		relogexp 22736	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2498	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2524	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6302	. . . . . . . . . . . . . . 15
32		3cn 10610	. . . . . . . . . . . . . . . 16
33		2nn 10693	. . . . . . . . . . . . . . . . . 18
34		nnrp 11229	. . . . . . . . . . . . . . . . . 18
35		relogcl 22719	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9608	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10570	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10302	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2524	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6309	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5950	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2524	. . . . . . . . . . 11 ;
46	45	oveq2d 6300	. . . . . . . . . 10 ;
47		sqrt2re 13844	. . . . . . . . . . . . 13
48	47	recni 9608	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10286	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9605	. . . . . . . . . . 11
51		4cn 10613	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9774	. . . . . . . . . . . . . . 15
53		2re 10605	. . . . . . . . . . . . . . . . 17
54		0le2 10626	. . . . . . . . . . . . . . . . 17
55		remsqsqrt 13053	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 672	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6295	. . . . . . . . . . . . . . 15
58		4t2e8 10689	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2500	. . . . . . . . . . . . . 14
60	59	oveq2i 6295	. . . . . . . . . . . . 13
61	51, 48	mulcli 9601	. . . . . . . . . . . . . . 15
62		nnrp 11229	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrtcl 13061	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11241	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 672	. . . . . . . . . . . . . . . 16
68		rpne0 11235	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 11235	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10246	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1311	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 673	. . . . . . . . . . . . . 14
75		4ne0 10632	. . . . . . . . . . . . . . 15
76		divdiv1 10255	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1311	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 673	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2499	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10300	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2505	. . . . . . . . . . . 12
82	81	oveq1i 6294	. . . . . . . . . . 11
83	50, 82	eqtr3i 2498	. . . . . . . . . 10
84	46, 83	syl6eq 2524	. . . . . . . . 9 ;
85		oveq1 6291	. . . . . . . . . . . . . 14 ; ;
86		df-6 10598	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6295	. . . . . . . . . . . . . . . . 17
88		2exp6 14431	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10606	. . . . . . . . . . . . . . . . . 18
90		5nn0 10815	. . . . . . . . . . . . . . . . . 18
91		expp1 12141	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 672	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2504	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6294	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 12147	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 672	. . . . . . . . . . . . . . . . 17
97	96	nncni 10546	. . . . . . . . . . . . . . . 16
98		2ne0 10628	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10291	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2496	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2524	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5870	. . . . . . . . . . . 12 ;
103		nnrp 11229	. . . . . . . . . . . . 13
104		fveq2 5866	. . . . . . . . . . . . . . . . 17
105		5nn 10696	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10888	. . . . . . . . . . . . . . . . . 18
107		relogexp 22736	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 672	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2524	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6302	. . . . . . . . . . . . . . 15
112		5cn 10615	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10570	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10302	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2524	. . . . . . . . . . . . . 14
116		ovex 6309	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5950	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2524	. . . . . . . . . . 11 ;
120	119	oveq2d 6300	. . . . . . . . . 10 ;
121		9cn 10623	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10286	. . . . . . . . . . 11
123	112, 97, 113	divcli 10286	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9605	. . . . . . . . . 10
125	120, 124	syl6eqr 2526	. . . . . . . . 9 ;
126	84, 125	oveq12d 6302	. . . . . . . 8 ;
127	32, 51, 75	divcli 10286	. . . . . . . . . 10
128	127, 48, 71	divcli 10286	. . . . . . . . 9
129	122, 123	mulcli 9601	. . . . . . . . 9
130	128, 129, 37	adddiri 9607	. . . . . . . 8
131	126, 130	syl6eqr 2526	. . . . . . 7 ;
132		oveq2 6292	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5870	. . . . . . . . . 10 ; ;
134	3	nnrei 10545	. . . . . . . . . . . 12 ;
135	3	nngt0i 10569	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9707	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrtmulii 13182	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6295	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2496	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2524	. . . . . . . . 9 ;
141	140	oveq2d 6300	. . . . . . . 8 ;
142	48, 5	mulcli 9601	. . . . . . . . . 10
143		rpmulcl 11241	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 663	. . . . . . . . . . 11
145		rpne0 11235	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10224	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1324	. . . . . . . . 9
149	48, 5	mulcomi 9602	. . . . . . . . . . . 12
150	149	oveq2i 6295	. . . . . . . . . . 11
151		recdiv2 10257	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 673	. . . . . . . . . . 11
153	150, 152	eqtr4i 2499	. . . . . . . . . 10
154	153	oveq1i 6294	. . . . . . . . 9
155	148, 154	eqtri 2496	. . . . . . . 8
156	141, 155	syl6eq 2524	. . . . . . 7 ;
157	131, 156	oveq12d 6302	. . . . . 6 ;
158	128, 129	addcli 9600	. . . . . . 7
159	5, 38	reccli 10274	. . . . . . . 8
160	159, 48, 71	divcli 10286	. . . . . . 7
161	158, 160, 37	adddiri 9607	. . . . . 6
162	157, 161	syl6eqr 2526	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6309	. . . . 5
165	162, 163, 164	fvmpt 5950	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10609	. . . . . . . 8
168		4re 10612	. . . . . . . 8
169	167, 168, 75	redivcli 10311	. . . . . . 7
170	169, 47, 71	redivcli 10311	. . . . . 6
171		9re 10622	. . . . . . . 8
172	171, 168, 75	redivcli 10311	. . . . . . 7
173		5re 10614	. . . . . . . 8
174	96	nnrei 10545	. . . . . . . 8
175	173, 174, 113	redivcli 10311	. . . . . . 7
176	172, 175	remulcli 9610	. . . . . 6
177	170, 176	readdcli 9609	. . . . 5
178	11, 38	rereccli 10309	. . . . . 6
179	178, 47, 71	redivcli 10311	. . . . 5
180	177, 179	readdcli 9609	. . . 4
181	180, 36	remulcli 9610	. . 3
182	166, 181	eqeltri 2551	. 2 ;
183	128, 129, 160	add32i 9798	. . . . . 6
184		6cn 10617	. . . . . . . . . . 11
185		ax-1cn 9550	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10301	. . . . . . . . . 10
187		df-7 10599	. . . . . . . . . . 11
188	187	oveq1i 6294	. . . . . . . . . 10
189		divcan5 10246	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1311	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 673	. . . . . . . . . . . 12
192		3t2e6 10687	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9603	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9603	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6296	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2498	. . . . . . . . . . 11
197	196	oveq1i 6294	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2507	. . . . . . . . 9
199	198	oveq1i 6294	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10301	. . . . . . . 8
201		7cn 10619	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10299	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2504	. . . . . . 7
204	203	oveq1i 6294	. . . . . 6
205	183, 204	eqtri 2496	. . . . 5
206		4nn0 10814	. . . . . . . . . . . 12
207		9nn0 10819	. . . . . . . . . . . 12
208		0nn0 10810	. . . . . . . . . . . 12
209		9lt10 10738	. . . . . . . . . . . 12
210		4lt5 10708	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 10998	. . . . . . . . . . 11 ; ;
212		7t7e49 11063	. . . . . . . . . . 11 ;
213	56	oveq1i 6294	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9776	. . . . . . . . . . . 12
215		5t2e10 10690	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9603	. . . . . . . . . . . . . 14
217	216	oveq1i 6294	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9605	. . . . . . . . . . . . 13
219	90	dec0u 10991	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2504	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2504	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4475	. . . . . . . . . 10
223		7re 10618	. . . . . . . . . . . 12
224		7pos 10635	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9707	. . . . . . . . . . 11
226		nnrp 11229	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11241	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 672	. . . . . . . . . . . 12
230		rpge0 11232	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 11226	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10458	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 672	. . . . . . . . . 10
236	222, 235	mpbir 209	. . . . . . . . 9
237		rpgt0 11231	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10417	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1314	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 672	. . . . . . . . 9
242	236, 241	mpbir 209	. . . . . . . 8
243	223, 47, 71	redivcli 10311	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10475	. . . . . . . 8
245	242, 244	mpbi 208	. . . . . . 7
246		divsubdir 10240	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1314	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 672	. . . . . . . . 9
249		5p3e8 10674	. . . . . . . . . . . 12
250	249	oveq1i 6294	. . . . . . . . . . 11
251		pncan 9826	. . . . . . . . . . . 12 $/\$
252	112, 32, 251	mp2an 672	. . . . . . . . . . 11
253	250, 252	eqtr3i 2498	. . . . . . . . . 10
254	253	oveq1i 6294	. . . . . . . . 9
255	5, 38	dividi 10277	. . . . . . . . . 10
256	255	oveq1i 6294	. . . . . . . . 9
257	248, 254, 256	3eqtr3ri 2505	. . . . . . . 8
258		5lt8 10725	. . . . . . . . . . . . 13
259	11, 173	remulcli 9610	. . . . . . . . . . . . . 14
260	173, 11, 259	ltadd2i 9715	. . . . . . . . . . . . 13
261	258, 260	mpbi 208	. . . . . . . . . . . 12
262		df-9 10601	. . . . . . . . . . . . . 14
263	262	oveq1i 6294	. . . . . . . . . . . . 13
264	5, 185, 112	adddiri 9607	. . . . . . . . . . . . 13
265	112	mulid2i 9599	. . . . . . . . . . . . . 14
266	265	oveq2i 6295	. . . . . . . . . . . . 13
267	263, 264, 266	3eqtri 2500	. . . . . . . . . . . 12
268	86	oveq2i 6295	. . . . . . . . . . . . 13
269	5, 112, 185	adddii 9606	. . . . . . . . . . . . 13
270	5	mulid1i 9598	. . . . . . . . . . . . . 14
271	270	oveq2i 6295	. . . . . . . . . . . . 13
272	268, 269, 271	3eqtri 2500	. . . . . . . . . . . 12
273	261, 267, 272	3brtr4i 4475	. . . . . . . . . . 11
274	171, 173	remulcli 9610	. . . . . . . . . . . 12
275		6re 10616	. . . . . . . . . . . . 13
276	11, 275	remulcli 9610	. . . . . . . . . . . 12
277	168, 174	remulcli 9610	. . . . . . . . . . . 12
278	2, 96	nnmulcli 10560	. . . . . . . . . . . . 13
279	278	nngt0i 10569	. . . . . . . . . . . 12
280	274, 276, 277, 279	ltdiv1ii 10475	. . . . . . . . . . 11
281	273, 280	mpbi 208	. . . . . . . . . 10
282	121, 51, 112, 97, 75, 113	divmuldivi 10304	. . . . . . . . . 10
283		nnexpcl 12147	. . . . . . . . . . . . . 14 $/\$
284	33, 206, 283	mp2an 672	. . . . . . . . . . . . 13
285	284	nncni 10546	. . . . . . . . . . . 12
286	284	nnne0i 10570	. . . . . . . . . . . 12
287		divcan5 10246	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
288	32, 287	mp3an1 1311	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
289	5, 38, 285, 286, 288	mp4an 673	. . . . . . . . . . 11
290		df-4 10596	. . . . . . . . . . . . . . . 16
291	290	oveq2i 6295	. . . . . . . . . . . . . . 15
292		3nn0 10813	. . . . . . . . . . . . . . . 16
293		expp1 12141	. . . . . . . . . . . . . . . 16 $/\$
294	89, 292, 293	mp2an 672	. . . . . . . . . . . . . . 15
295	22	oveq1i 6294	. . . . . . . . . . . . . . 15
296	291, 294, 295	3eqtri 2500	. . . . . . . . . . . . . 14
297	296	oveq1i 6294	. . . . . . . . . . . . 13
298	5, 89, 32	mulassi 9605	. . . . . . . . . . . . 13
299	193	oveq2i 6295	. . . . . . . . . . . . 13
300	297, 298, 299	3eqtri 2500	. . . . . . . . . . . 12
301		4p3e7 10671	. . . . . . . . . . . . . . . 16
302		5p2e7 10673	. . . . . . . . . . . . . . . 16
303	112, 89	addcomi 9770	. . . . . . . . . . . . . . . 16
304	301, 302, 303	3eqtr2i 2502	. . . . . . . . . . . . . . 15
305	304	oveq2i 6295	. . . . . . . . . . . . . 14
306		expadd 12176	. . . . . . . . . . . . . . 15 $/\$ $/\$
307	89, 206, 292, 306	mp3an 1324	. . . . . . . . . . . . . 14
308		2nn0 10812	. . . . . . . . . . . . . . 15
309		expadd 12176	. . . . . . . . . . . . . . 15 $/\$ $/\$
310	89, 308, 90, 309	mp3an 1324	. . . . . . . . . . . . . 14
311	305, 307, 310	3eqtr3i 2504	. . . . . . . . . . . . 13
312	22	oveq2i 6295	. . . . . . . . . . . . 13
313		sq2 12232	. . . . . . . . . . . . . 14
314	313	oveq1i 6294	. . . . . . . . . . . . 13
315	311, 312, 314	3eqtr3i 2504	. . . . . . . . . . . 12
316	300, 315	oveq12i 6296	. . . . . . . . . . 11
317	289, 316	eqtr3i 2498	. . . . . . . . . 10
318	281, 282, 317	3brtr4i 4475	. . . . . . . . 9
319	167, 11, 38	redivcli 10311	. . . . . . . . . 10
320		1re 9595	. . . . . . . . . 10
321		ltsub2 10049	. . . . . . . . . 10 $/\$ $/\$
322	176, 319, 320, 321	mp3an 1324	. . . . . . . . 9
323	318, 322	mpbi 208	. . . . . . . 8
324	257, 323	eqbrtrri 4468	. . . . . . 7
325	243, 11, 38	redivcli 10311	. . . . . . . 8
326	173, 11, 38	redivcli 10311	. . . . . . . 8
327	320, 176	resubcli 9881	. . . . . . . 8
328	325, 326, 327	lttri 9710	. . . . . . 7 $/\$
329	245, 324, 328	mp2an 672	. . . . . 6
330	325, 176, 320	ltaddsubi 10114	. . . . . 6
331	329, 330	mpbir 209	. . . . 5
332	205, 331	eqbrtri 4466	. . . 4
333		1lt2 10702	. . . . . . 7
334		rplogcl 22745	. . . . . . 7 $/\$
335	53, 333, 334	mp2an 672	. . . . . 6
336		rpgt0 11231	. . . . . 6
337	335, 336	ax-mp 5	. . . . 5
338	180, 320, 36, 337	ltmul1ii 10474	. . . 4
339	332, 338	mpbi 208	. . 3
340	37	mulid2i 9599	. . . 4
341	340	eqcomi 2480	. . 3
342	339, 166, 341	3brtr4i 4475	. 2 ;
343	182, 342	pm3.2i 455	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662 class class class wbr 4447

cmpt 4505

cfv 5588 (class class class)co 6284

cc 9490

cr 9491

cc0 9492

c1 9493

caddc 9495

cmul 9497

clt 9628

cle 9629

cmin 9805

cdiv 10206

cn 10536

c2 10585

c3 10586

c4 10587

c5 10588

c6 10589

c7 10590

c8 10591

c9 10592

c10 10593

cn0 10795

cz 10864 ;cdc 10976

crp 11220

cexp 12134

csqrt 13029

clog 22698

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570 ax-addf 9571 ax-mulf 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-of 6524 df-om 6685 df-1st 6784 df-2nd 6785 df-supp 6902 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-ixp 7470 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fsupp 7830 df-fi 7871 df-sup 7901 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-4 10596 df-5 10597 df-6 10598 df-7 10599 df-8 10600 df-9 10601 df-10 10602 df-n0 10796 df-z 10865 df-dec 10977 df-uz 11083 df-q 11183 df-rp 11221 df-xneg 11318 df-xadd 11319 df-xmul 11320 df-ioo 11533 df-ioc 11534 df-ico 11535 df-icc 11536 df-fz 11673 df-fzo 11793 df-fl 11897 df-mod 11965 df-seq 12076 df-exp 12135 df-fac 12322 df-bc 12349 df-hash 12374 df-shft 12863 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-limsup 13257 df-clim 13274 df-rlim 13275 df-sum 13472 df-ef 13665 df-sin 13667 df-cos 13668 df-pi 13670 df-struct 14492 df-ndx 14493 df-slot 14494 df-base 14495 df-sets 14496 df-ress 14497 df-plusg 14568 df-mulr 14569 df-starv 14570 df-sca 14571 df-vsca 14572 df-ip 14573 df-tset 14574 df-ple 14575 df-ds 14577 df-unif 14578 df-hom 14579 df-cco 14580 df-rest 14678 df-topn 14679 df-0g 14697 df-gsum 14698 df-topgen 14699 df-pt 14700 df-prds 14703 df-xrs 14757 df-qtop 14762 df-imas 14763 df-xps 14765 df-mre 14841 df-mrc 14842 df-acs 14844 df-mnd 15732 df-submnd 15787 df-mulg 15870 df-cntz 16160 df-cmn 16606 df-psmet 18210 df-xmet 18211 df-met 18212 df-bl 18213 df-mopn 18214 df-fbas 18215 df-fg 18216 df-cnfld 18220 df-top 19194 df-bases 19196 df-topon 19197 df-topsp 19198 df-cld 19314 df-ntr 19315 df-cls 19316 df-nei 19393 df-lp 19431 df-perf 19432 df-cn 19522 df-cnp 19523 df-haus 19610 df-tx 19826 df-hmeo 20019 df-fil 20110 df-fm 20202 df-flim 20203 df-flf 20204 df-xms 20586 df-ms 20587 df-tms 20588 df-cncf 21145 df-limc 22033 df-dv 22034 df-log 22700

This theorem is referenced by: bposlem9 23323

W3C validator