bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 23683

Description: Lemma for bpos 23685. 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 10733	. . . . 5
2		4nn 10612	. . . . 5
3	1, 2	decnncl 10908	. . . 4 ;
4		fveq2 5774	. . . . . . . . . . . . . 14 ; ;
5		8cn 10538	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 12150	. . . . . . . . . . . . . . . . 17
7		8t8e64 10989	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2411	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5777	. . . . . . . . . . . . . . 15 ;
10		0re 9507	. . . . . . . . . . . . . . . . 17
11		8re 10537	. . . . . . . . . . . . . . . . 17
12		8pos 10553	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9618	. . . . . . . . . . . . . . . 16
14	11	sqrtsqi 13209	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2413	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2439	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5778	. . . . . . . . . . . 12 ;
19		8nn 10616	. . . . . . . . . . . . 13
20		nnrp 11148	. . . . . . . . . . . . 13
21		fveq2 5774	. . . . . . . . . . . . . . . . 17
22		cu2 12169	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5777	. . . . . . . . . . . . . . . . . 18
24		2rp 11144	. . . . . . . . . . . . . . . . . . 19
25		3z 10814	. . . . . . . . . . . . . . . . . . 19
26		relogexp 23068	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 670	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2413	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2439	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6214	. . . . . . . . . . . . . . 15
32		3cn 10527	. . . . . . . . . . . . . . . 16
33		2nn 10610	. . . . . . . . . . . . . . . . . 18
34		nnrp 11148	. . . . . . . . . . . . . . . . . 18
35		relogcl 23048	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9519	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10487	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10219	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2439	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6224	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5857	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2439	. . . . . . . . . . 11 ;
46	45	oveq2d 6212	. . . . . . . . . 10 ;
47		sqrt2re 13985	. . . . . . . . . . . . 13
48	47	recni 9519	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10203	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9516	. . . . . . . . . . 11
51		4cn 10530	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9686	. . . . . . . . . . . . . . 15
53		2re 10522	. . . . . . . . . . . . . . . . 17
54		0le2 10543	. . . . . . . . . . . . . . . . 17
55		remsqsqrt 13092	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 670	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6207	. . . . . . . . . . . . . . 15
58		4t2e8 10606	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2415	. . . . . . . . . . . . . 14
60	59	oveq2i 6207	. . . . . . . . . . . . 13
61	51, 48	mulcli 9512	. . . . . . . . . . . . . . 15
62		nnrp 11148	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrtcl 13100	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11161	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 670	. . . . . . . . . . . . . . . 16
68		rpne0 11154	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 11154	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10163	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1309	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 671	. . . . . . . . . . . . . 14
75		4ne0 10549	. . . . . . . . . . . . . . 15
76		divdiv1 10172	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1309	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 671	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2414	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10217	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2420	. . . . . . . . . . . 12
82	81	oveq1i 6206	. . . . . . . . . . 11
83	50, 82	eqtr3i 2413	. . . . . . . . . 10
84	46, 83	syl6eq 2439	. . . . . . . . 9 ;
85		oveq1 6203	. . . . . . . . . . . . . 14 ; ;
86		df-6 10515	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6207	. . . . . . . . . . . . . . . . 17
88		2exp6 14574	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10523	. . . . . . . . . . . . . . . . . 18
90		5nn0 10732	. . . . . . . . . . . . . . . . . 18
91		expp1 12076	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 670	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2419	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6206	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 12082	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 670	. . . . . . . . . . . . . . . . 17
97	96	nncni 10462	. . . . . . . . . . . . . . . 16
98		2ne0 10545	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10208	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2411	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2439	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5778	. . . . . . . . . . . 12 ;
103		nnrp 11148	. . . . . . . . . . . . 13
104		fveq2 5774	. . . . . . . . . . . . . . . . 17
105		5nn 10613	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10805	. . . . . . . . . . . . . . . . . 18
107		relogexp 23068	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 670	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2439	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6214	. . . . . . . . . . . . . . 15
112		5cn 10532	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10487	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10219	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2439	. . . . . . . . . . . . . 14
116		ovex 6224	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5857	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2439	. . . . . . . . . . 11 ;
120	119	oveq2d 6212	. . . . . . . . . 10 ;
121		9cn 10540	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10203	. . . . . . . . . . 11
123	112, 97, 113	divcli 10203	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9516	. . . . . . . . . 10
125	120, 124	syl6eqr 2441	. . . . . . . . 9 ;
126	84, 125	oveq12d 6214	. . . . . . . 8 ;
127	32, 51, 75	divcli 10203	. . . . . . . . . 10
128	127, 48, 71	divcli 10203	. . . . . . . . 9
129	122, 123	mulcli 9512	. . . . . . . . 9
130	128, 129, 37	adddiri 9518	. . . . . . . 8
131	126, 130	syl6eqr 2441	. . . . . . 7 ;
132		oveq2 6204	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5778	. . . . . . . . . 10 ; ;
134	3	nnrei 10461	. . . . . . . . . . . 12 ;
135	3	nngt0i 10486	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9618	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrtmulii 13221	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6207	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2411	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2439	. . . . . . . . 9 ;
141	140	oveq2d 6212	. . . . . . . 8 ;
142	48, 5	mulcli 9512	. . . . . . . . . 10
143		rpmulcl 11161	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 661	. . . . . . . . . . 11
145		rpne0 11154	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10141	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1322	. . . . . . . . 9
149	48, 5	mulcomi 9513	. . . . . . . . . . . 12
150	149	oveq2i 6207	. . . . . . . . . . 11
151		recdiv2 10174	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 671	. . . . . . . . . . 11
153	150, 152	eqtr4i 2414	. . . . . . . . . 10
154	153	oveq1i 6206	. . . . . . . . 9
155	148, 154	eqtri 2411	. . . . . . . 8
156	141, 155	syl6eq 2439	. . . . . . 7 ;
157	131, 156	oveq12d 6214	. . . . . 6 ;
158	128, 129	addcli 9511	. . . . . . 7
159	5, 38	reccli 10191	. . . . . . . 8
160	159, 48, 71	divcli 10203	. . . . . . 7
161	158, 160, 37	adddiri 9518	. . . . . 6
162	157, 161	syl6eqr 2441	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6224	. . . . 5
165	162, 163, 164	fvmpt 5857	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10526	. . . . . . . 8
168		4re 10529	. . . . . . . 8
169	167, 168, 75	redivcli 10228	. . . . . . 7
170	169, 47, 71	redivcli 10228	. . . . . 6
171		9re 10539	. . . . . . . 8
172	171, 168, 75	redivcli 10228	. . . . . . 7
173		5re 10531	. . . . . . . 8
174	96	nnrei 10461	. . . . . . . 8
175	173, 174, 113	redivcli 10228	. . . . . . 7
176	172, 175	remulcli 9521	. . . . . 6
177	170, 176	readdcli 9520	. . . . 5
178	11, 38	rereccli 10226	. . . . . 6
179	178, 47, 71	redivcli 10228	. . . . 5
180	177, 179	readdcli 9520	. . . 4
181	180, 36	remulcli 9521	. . 3
182	166, 181	eqeltri 2466	. 2 ;
183	128, 129, 160	add32i 9710	. . . . . 6
184		6cn 10534	. . . . . . . . . . 11
185		ax-1cn 9461	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10218	. . . . . . . . . 10
187		df-7 10516	. . . . . . . . . . 11
188	187	oveq1i 6206	. . . . . . . . . 10
189		divcan5 10163	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 671	. . . . . . . . . . . 12
192		3t2e6 10604	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9514	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9514	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6208	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2413	. . . . . . . . . . 11
197	196	oveq1i 6206	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2422	. . . . . . . . 9
199	198	oveq1i 6206	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10218	. . . . . . . 8
201		7cn 10536	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10216	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2419	. . . . . . 7
204	203	oveq1i 6206	. . . . . 6
205	183, 204	eqtri 2411	. . . . 5
206		4nn0 10731	. . . . . . . . . . . 12
207		9nn0 10736	. . . . . . . . . . . 12
208		0nn0 10727	. . . . . . . . . . . 12
209		9lt10 10655	. . . . . . . . . . . 12
210		4lt5 10625	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 10917	. . . . . . . . . . 11 ; ;
212		7t7e49 10982	. . . . . . . . . . 11 ;
213	56	oveq1i 6206	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9688	. . . . . . . . . . . 12
215		5t2e10 10607	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9514	. . . . . . . . . . . . . 14
217	216	oveq1i 6206	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9516	. . . . . . . . . . . . 13
219	90	dec0u 10910	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2419	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2419	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4395	. . . . . . . . . 10
223		7re 10535	. . . . . . . . . . . 12
224		7pos 10552	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9618	. . . . . . . . . . 11
226		nnrp 11148	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11161	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 670	. . . . . . . . . . . 12
230		rpge0 11151	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 11145	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10374	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 670	. . . . . . . . . 10
236	222, 235	mpbir 209	. . . . . . . . 9
237		rpgt0 11150	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10334	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1312	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 670	. . . . . . . . 9
242	236, 241	mpbir 209	. . . . . . . 8
243	223, 47, 71	redivcli 10228	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10391	. . . . . . . 8
245	242, 244	mpbi 208	. . . . . . 7
246		divsubdir 10157	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1312	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 670	. . . . . . . . 9
249		5p3e8 10591	. . . . . . . . . . . 12
250	249	oveq1i 6206	. . . . . . . . . . 11
251	112, 32	pncan3oi 9749	. . . . . . . . . . 11
252	250, 251	eqtr3i 2413	. . . . . . . . . 10
253	252	oveq1i 6206	. . . . . . . . 9
254	5, 38	dividi 10194	. . . . . . . . . 10
255	254	oveq1i 6206	. . . . . . . . 9
256	248, 253, 255	3eqtr3ri 2420	. . . . . . . 8
257		5lt8 10642	. . . . . . . . . . . . 13
258	11, 173	remulcli 9521	. . . . . . . . . . . . . 14
259	173, 11, 258	ltadd2i 9626	. . . . . . . . . . . . 13
260	257, 259	mpbi 208	. . . . . . . . . . . 12
261		df-9 10518	. . . . . . . . . . . . . 14
262	261	oveq1i 6206	. . . . . . . . . . . . 13
263	5, 185, 112	adddiri 9518	. . . . . . . . . . . . 13
264	112	mulid2i 9510	. . . . . . . . . . . . . 14
265	264	oveq2i 6207	. . . . . . . . . . . . 13
266	262, 263, 265	3eqtri 2415	. . . . . . . . . . . 12
267	86	oveq2i 6207	. . . . . . . . . . . . 13
268	5, 112, 185	adddii 9517	. . . . . . . . . . . . 13
269	5	mulid1i 9509	. . . . . . . . . . . . . 14
270	269	oveq2i 6207	. . . . . . . . . . . . 13
271	267, 268, 270	3eqtri 2415	. . . . . . . . . . . 12
272	260, 266, 271	3brtr4i 4395	. . . . . . . . . . 11
273	171, 173	remulcli 9521	. . . . . . . . . . . 12
274		6re 10533	. . . . . . . . . . . . 13
275	11, 274	remulcli 9521	. . . . . . . . . . . 12
276	168, 174	remulcli 9521	. . . . . . . . . . . 12
277	2, 96	nnmulcli 10476	. . . . . . . . . . . . 13
278	277	nngt0i 10486	. . . . . . . . . . . 12
279	273, 275, 276, 278	ltdiv1ii 10391	. . . . . . . . . . 11
280	272, 279	mpbi 208	. . . . . . . . . 10
281	121, 51, 112, 97, 75, 113	divmuldivi 10221	. . . . . . . . . 10
282		nnexpcl 12082	. . . . . . . . . . . . . 14 $/\$
283	33, 206, 282	mp2an 670	. . . . . . . . . . . . 13
284	283	nncni 10462	. . . . . . . . . . . 12
285	283	nnne0i 10487	. . . . . . . . . . . 12
286		divcan5 10163	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
287	32, 286	mp3an1 1309	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
288	5, 38, 284, 285, 287	mp4an 671	. . . . . . . . . . 11
289		df-4 10513	. . . . . . . . . . . . . . . 16
290	289	oveq2i 6207	. . . . . . . . . . . . . . 15
291		3nn0 10730	. . . . . . . . . . . . . . . 16
292		expp1 12076	. . . . . . . . . . . . . . . 16 $/\$
293	89, 291, 292	mp2an 670	. . . . . . . . . . . . . . 15
294	22	oveq1i 6206	. . . . . . . . . . . . . . 15
295	290, 293, 294	3eqtri 2415	. . . . . . . . . . . . . 14
296	295	oveq1i 6206	. . . . . . . . . . . . 13
297	5, 89, 32	mulassi 9516	. . . . . . . . . . . . 13
298	193	oveq2i 6207	. . . . . . . . . . . . 13
299	296, 297, 298	3eqtri 2415	. . . . . . . . . . . 12
300		4p3e7 10588	. . . . . . . . . . . . . . . 16
301		5p2e7 10590	. . . . . . . . . . . . . . . 16
302	112, 89	addcomi 9682	. . . . . . . . . . . . . . . 16
303	300, 301, 302	3eqtr2i 2417	. . . . . . . . . . . . . . 15
304	303	oveq2i 6207	. . . . . . . . . . . . . 14
305		expadd 12111	. . . . . . . . . . . . . . 15 $/\$ $/\$
306	89, 206, 291, 305	mp3an 1322	. . . . . . . . . . . . . 14
307		2nn0 10729	. . . . . . . . . . . . . . 15
308		expadd 12111	. . . . . . . . . . . . . . 15 $/\$ $/\$
309	89, 307, 90, 308	mp3an 1322	. . . . . . . . . . . . . 14
310	304, 306, 309	3eqtr3i 2419	. . . . . . . . . . . . 13
311	22	oveq2i 6207	. . . . . . . . . . . . 13
312		sq2 12167	. . . . . . . . . . . . . 14
313	312	oveq1i 6206	. . . . . . . . . . . . 13
314	310, 311, 313	3eqtr3i 2419	. . . . . . . . . . . 12
315	299, 314	oveq12i 6208	. . . . . . . . . . 11
316	288, 315	eqtr3i 2413	. . . . . . . . . 10
317	280, 281, 316	3brtr4i 4395	. . . . . . . . 9
318	167, 11, 38	redivcli 10228	. . . . . . . . . 10
319		1re 9506	. . . . . . . . . 10
320		ltsub2 9967	. . . . . . . . . 10 $/\$ $/\$
321	176, 318, 319, 320	mp3an 1322	. . . . . . . . 9
322	317, 321	mpbi 208	. . . . . . . 8
323	256, 322	eqbrtrri 4388	. . . . . . 7
324	243, 11, 38	redivcli 10228	. . . . . . . 8
325	173, 11, 38	redivcli 10228	. . . . . . . 8
326	319, 176	resubcli 9794	. . . . . . . 8
327	324, 325, 326	lttri 9621	. . . . . . 7 $/\$
328	245, 323, 327	mp2an 670	. . . . . 6
329	324, 176, 319	ltaddsubi 10031	. . . . . 6
330	328, 329	mpbir 209	. . . . 5
331	205, 330	eqbrtri 4386	. . . 4
332		1lt2 10619	. . . . . . 7
333		rplogcl 23076	. . . . . . 7 $/\$
334	53, 332, 333	mp2an 670	. . . . . 6
335		rpgt0 11150	. . . . . 6
336	334, 335	ax-mp 5	. . . . 5
337	180, 319, 36, 336	ltmul1ii 10390	. . . 4
338	331, 337	mpbi 208	. . 3
339	37	mulid2i 9510	. . . 4
340	339	eqcomi 2395	. . 3
341	338, 166, 340	3brtr4i 4395	. 2 ;
342	182, 341	pm3.2i 453	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 184 $/\$ wa 367

wceq 1399

wcel 1826

wne 2577 class class class wbr 4367

cmpt 4425

cfv 5496 (class class class)co 6196

cc 9401

cr 9402

cc0 9403

c1 9404

caddc 9406

cmul 9408

clt 9539

cle 9540

cmin 9718

cdiv 10123

cn 10452

c2 10502

c3 10503

c4 10504

c5 10505

c6 10506

c7 10507

c8 10508

c9 10509

c10 10510

cn0 10712

cz 10781 ;cdc 10895

crp 11139

cexp 12069

csqrt 13068

clog 23027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481 ax-addf 9482 ax-mulf 9483

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-iin 4246 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-of 6439 df-om 6600 df-1st 6699 df-2nd 6700 df-supp 6818 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-er 7229 df-map 7340 df-pm 7341 df-ixp 7389 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-fsupp 7745 df-fi 7786 df-sup 7816 df-oi 7850 df-card 8233 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-5 10514 df-6 10515 df-7 10516 df-8 10517 df-9 10518 df-10 10519 df-n0 10713 df-z 10782 df-dec 10896 df-uz 11002 df-q 11102 df-rp 11140 df-xneg 11239 df-xadd 11240 df-xmul 11241 df-ioo 11454 df-ioc 11455 df-ico 11456 df-icc 11457 df-fz 11594 df-fzo 11718 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-fac 12256 df-bc 12283 df-hash 12308 df-shft 12902 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-limsup 13296 df-clim 13313 df-rlim 13314 df-sum 13511 df-ef 13805 df-sin 13807 df-cos 13808 df-pi 13810 df-struct 14636 df-ndx 14637 df-slot 14638 df-base 14639 df-sets 14640 df-ress 14641 df-plusg 14715 df-mulr 14716 df-starv 14717 df-sca 14718 df-vsca 14719 df-ip 14720 df-tset 14721 df-ple 14722 df-ds 14724 df-unif 14725 df-hom 14726 df-cco 14727 df-rest 14830 df-topn 14831 df-0g 14849 df-gsum 14850 df-topgen 14851 df-pt 14852 df-prds 14855 df-xrs 14909 df-qtop 14914 df-imas 14915 df-xps 14917 df-mre 14993 df-mrc 14994 df-acs 14996 df-mgm 15989 df-sgrp 16028 df-mnd 16038 df-submnd 16084 df-mulg 16177 df-cntz 16472 df-cmn 16917 df-psmet 18524 df-xmet 18525 df-met 18526 df-bl 18527 df-mopn 18528 df-fbas 18529 df-fg 18530 df-cnfld 18534 df-top 19484 df-bases 19486 df-topon 19487 df-topsp 19488 df-cld 19605 df-ntr 19606 df-cls 19607 df-nei 19685 df-lp 19723 df-perf 19724 df-cn 19814 df-cnp 19815 df-haus 19902 df-tx 20148 df-hmeo 20341 df-fil 20432 df-fm 20524 df-flim 20525 df-flf 20526 df-xms 20908 df-ms 20909 df-tms 20910 df-cncf 21467 df-limc 22355 df-dv 22356 df-log 23029

This theorem is referenced by: bposlem9 23684

W3C validator