bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 24073

Description: Lemma for bpos 24075. 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 10890	. . . . 5
2		4nn 10769	. . . . 5
3	1, 2	decnncl 11064	. . . 4 ;
4		fveq2 5881	. . . . . . . . . . . . . 14 ; ;
5		8cn 10695	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 12351	. . . . . . . . . . . . . . . . 17
7		8t8e64 11145	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2458	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5884	. . . . . . . . . . . . . . 15 ;
10		0re 9642	. . . . . . . . . . . . . . . . 17
11		8re 10694	. . . . . . . . . . . . . . . . 17
12		8pos 10710	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9756	. . . . . . . . . . . . . . . 16
14	11	sqrtsqi 13416	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2460	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2486	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5885	. . . . . . . . . . . 12 ;
19		8nn 10773	. . . . . . . . . . . . 13
20		nnrp 11311	. . . . . . . . . . . . 13
21		fveq2 5881	. . . . . . . . . . . . . . . . 17
22		cu2 12370	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5884	. . . . . . . . . . . . . . . . . 18
24		2rp 11307	. . . . . . . . . . . . . . . . . . 19
25		3z 10970	. . . . . . . . . . . . . . . . . . 19
26		relogexp 23401	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 676	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2460	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2486	. . . . . . . . . . . . . . . 16
30		id 23	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6323	. . . . . . . . . . . . . . 15
32		3cn 10684	. . . . . . . . . . . . . . . 16
33		2nn 10767	. . . . . . . . . . . . . . . . . 18
34		nnrp 11311	. . . . . . . . . . . . . . . . . 18
35		relogcl 23381	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9654	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10644	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10364	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2486	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6333	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5964	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2486	. . . . . . . . . . 11 ;
46	45	oveq2d 6321	. . . . . . . . . 10 ;
47		sqrt2re 14280	. . . . . . . . . . . . 13
48	47	recni 9654	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10348	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9651	. . . . . . . . . . 11
51		4cn 10687	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9827	. . . . . . . . . . . . . . 15
53		2re 10679	. . . . . . . . . . . . . . . . 17
54		0le2 10700	. . . . . . . . . . . . . . . . 17
55		remsqsqrt 13299	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 676	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6316	. . . . . . . . . . . . . . 15
58		4t2e8 10763	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2462	. . . . . . . . . . . . . 14
60	59	oveq2i 6316	. . . . . . . . . . . . 13
61	51, 48	mulcli 9647	. . . . . . . . . . . . . . 15
62		nnrp 11311	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrtcl 13307	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11324	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 676	. . . . . . . . . . . . . . . 16
68		rpne0 11317	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 11317	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10308	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1347	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 677	. . . . . . . . . . . . . 14
75		4ne0 10706	. . . . . . . . . . . . . . 15
76		divdiv1 10317	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1347	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 677	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2461	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10362	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2467	. . . . . . . . . . . 12
82	81	oveq1i 6315	. . . . . . . . . . 11
83	50, 82	eqtr3i 2460	. . . . . . . . . 10
84	46, 83	syl6eq 2486	. . . . . . . . 9 ;
85		oveq1 6312	. . . . . . . . . . . . . 14 ; ;
86		df-6 10672	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6316	. . . . . . . . . . . . . . . . 17
88		2exp6 15012	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10680	. . . . . . . . . . . . . . . . . 18
90		5nn0 10889	. . . . . . . . . . . . . . . . . 18
91		expp1 12276	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 676	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2466	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6315	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 12282	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 676	. . . . . . . . . . . . . . . . 17
97	96	nncni 10619	. . . . . . . . . . . . . . . 16
98		2ne0 10702	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10353	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2458	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2486	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5885	. . . . . . . . . . . 12 ;
103		nnrp 11311	. . . . . . . . . . . . 13
104		fveq2 5881	. . . . . . . . . . . . . . . . 17
105		5nn 10770	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10961	. . . . . . . . . . . . . . . . . 18
107		relogexp 23401	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 676	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2486	. . . . . . . . . . . . . . . 16
110		id 23	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6323	. . . . . . . . . . . . . . 15
112		5cn 10689	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10644	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10364	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2486	. . . . . . . . . . . . . 14
116		ovex 6333	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5964	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2486	. . . . . . . . . . 11 ;
120	119	oveq2d 6321	. . . . . . . . . 10 ;
121		9cn 10697	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10348	. . . . . . . . . . 11
123	112, 97, 113	divcli 10348	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9651	. . . . . . . . . 10
125	120, 124	syl6eqr 2488	. . . . . . . . 9 ;
126	84, 125	oveq12d 6323	. . . . . . . 8 ;
127	32, 51, 75	divcli 10348	. . . . . . . . . 10
128	127, 48, 71	divcli 10348	. . . . . . . . 9
129	122, 123	mulcli 9647	. . . . . . . . 9
130	128, 129, 37	adddiri 9653	. . . . . . . 8
131	126, 130	syl6eqr 2488	. . . . . . 7 ;
132		oveq2 6313	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5885	. . . . . . . . . 10 ; ;
134	3	nnrei 10618	. . . . . . . . . . . 12 ;
135	3	nngt0i 10643	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9756	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrtmulii 13428	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6316	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2458	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2486	. . . . . . . . 9 ;
141	140	oveq2d 6321	. . . . . . . 8 ;
142	48, 5	mulcli 9647	. . . . . . . . . 10
143		rpmulcl 11324	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 667	. . . . . . . . . . 11
145		rpne0 11317	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10286	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1360	. . . . . . . . 9
149	48, 5	mulcomi 9648	. . . . . . . . . . . 12
150	149	oveq2i 6316	. . . . . . . . . . 11
151		recdiv2 10319	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 677	. . . . . . . . . . 11
153	150, 152	eqtr4i 2461	. . . . . . . . . 10
154	153	oveq1i 6315	. . . . . . . . 9
155	148, 154	eqtri 2458	. . . . . . . 8
156	141, 155	syl6eq 2486	. . . . . . 7 ;
157	131, 156	oveq12d 6323	. . . . . 6 ;
158	128, 129	addcli 9646	. . . . . . 7
159	5, 38	reccli 10336	. . . . . . . 8
160	159, 48, 71	divcli 10348	. . . . . . 7
161	158, 160, 37	adddiri 9653	. . . . . 6
162	157, 161	syl6eqr 2488	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6333	. . . . 5
165	162, 163, 164	fvmpt 5964	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10683	. . . . . . . 8
168		4re 10686	. . . . . . . 8
169	167, 168, 75	redivcli 10373	. . . . . . 7
170	169, 47, 71	redivcli 10373	. . . . . 6
171		9re 10696	. . . . . . . 8
172	171, 168, 75	redivcli 10373	. . . . . . 7
173		5re 10688	. . . . . . . 8
174	96	nnrei 10618	. . . . . . . 8
175	173, 174, 113	redivcli 10373	. . . . . . 7
176	172, 175	remulcli 9656	. . . . . 6
177	170, 176	readdcli 9655	. . . . 5
178	11, 38	rereccli 10371	. . . . . 6
179	178, 47, 71	redivcli 10373	. . . . 5
180	177, 179	readdcli 9655	. . . 4
181	180, 36	remulcli 9656	. . 3
182	166, 181	eqeltri 2513	. 2 ;
183	128, 129, 160	add32i 9851	. . . . . 6
184		6cn 10691	. . . . . . . . . . 11
185		ax-1cn 9596	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10363	. . . . . . . . . 10
187		df-7 10673	. . . . . . . . . . 11
188	187	oveq1i 6315	. . . . . . . . . 10
189		divcan5 10308	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1347	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 677	. . . . . . . . . . . 12
192		3t2e6 10761	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9649	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9649	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6317	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2460	. . . . . . . . . . 11
197	196	oveq1i 6315	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2469	. . . . . . . . 9
199	198	oveq1i 6315	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10363	. . . . . . . 8
201		7cn 10693	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10361	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2466	. . . . . . 7
204	203	oveq1i 6315	. . . . . 6
205	183, 204	eqtri 2458	. . . . 5
206		4nn0 10888	. . . . . . . . . . . 12
207		9nn0 10893	. . . . . . . . . . . 12
208		0nn0 10884	. . . . . . . . . . . 12
209		9lt10 10812	. . . . . . . . . . . 12
210		4lt5 10782	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 11073	. . . . . . . . . . 11 ; ;
212		7t7e49 11138	. . . . . . . . . . 11 ;
213	56	oveq1i 6315	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9829	. . . . . . . . . . . 12
215		5t2e10 10764	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9649	. . . . . . . . . . . . . 14
217	216	oveq1i 6315	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9651	. . . . . . . . . . . . 13
219	90	dec0u 11066	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2466	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2466	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4454	. . . . . . . . . 10
223		7re 10692	. . . . . . . . . . . 12
224		7pos 10709	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9756	. . . . . . . . . . 11
226		nnrp 11311	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11324	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 676	. . . . . . . . . . . 12
230		rpge0 11314	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 11308	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10519	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 676	. . . . . . . . . 10
236	222, 235	mpbir 212	. . . . . . . . 9
237		rpgt0 11313	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10479	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1350	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 676	. . . . . . . . 9
242	236, 241	mpbir 212	. . . . . . . 8
243	223, 47, 71	redivcli 10373	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10536	. . . . . . . 8
245	242, 244	mpbi 211	. . . . . . 7
246		divsubdir 10302	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1350	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 676	. . . . . . . . 9
249		5p3e8 10748	. . . . . . . . . . . 12
250	249	oveq1i 6315	. . . . . . . . . . 11
251	112, 32	pncan3oi 9890	. . . . . . . . . . 11
252	250, 251	eqtr3i 2460	. . . . . . . . . 10
253	252	oveq1i 6315	. . . . . . . . 9
254	5, 38	dividi 10339	. . . . . . . . . 10
255	254	oveq1i 6315	. . . . . . . . 9
256	248, 253, 255	3eqtr3ri 2467	. . . . . . . 8
257		5lt8 10799	. . . . . . . . . . . . 13
258	11, 173	remulcli 9656	. . . . . . . . . . . . . 14
259	173, 11, 258	ltadd2i 9764	. . . . . . . . . . . . 13
260	257, 259	mpbi 211	. . . . . . . . . . . 12
261		df-9 10675	. . . . . . . . . . . . . 14
262	261	oveq1i 6315	. . . . . . . . . . . . 13
263	5, 185, 112	adddiri 9653	. . . . . . . . . . . . 13
264	112	mulid2i 9645	. . . . . . . . . . . . . 14
265	264	oveq2i 6316	. . . . . . . . . . . . 13
266	262, 263, 265	3eqtri 2462	. . . . . . . . . . . 12
267	86	oveq2i 6316	. . . . . . . . . . . . 13
268	5, 112, 185	adddii 9652	. . . . . . . . . . . . 13
269	5	mulid1i 9644	. . . . . . . . . . . . . 14
270	269	oveq2i 6316	. . . . . . . . . . . . 13
271	267, 268, 270	3eqtri 2462	. . . . . . . . . . . 12
272	260, 266, 271	3brtr4i 4454	. . . . . . . . . . 11
273	171, 173	remulcli 9656	. . . . . . . . . . . 12
274		6re 10690	. . . . . . . . . . . . 13
275	11, 274	remulcli 9656	. . . . . . . . . . . 12
276	168, 174	remulcli 9656	. . . . . . . . . . . 12
277	2, 96	nnmulcli 10633	. . . . . . . . . . . . 13
278	277	nngt0i 10643	. . . . . . . . . . . 12
279	273, 275, 276, 278	ltdiv1ii 10536	. . . . . . . . . . 11
280	272, 279	mpbi 211	. . . . . . . . . 10
281	121, 51, 112, 97, 75, 113	divmuldivi 10366	. . . . . . . . . 10
282		nnexpcl 12282	. . . . . . . . . . . . . 14 $/\$
283	33, 206, 282	mp2an 676	. . . . . . . . . . . . 13
284	283	nncni 10619	. . . . . . . . . . . 12
285	283	nnne0i 10644	. . . . . . . . . . . 12
286		divcan5 10308	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
287	32, 286	mp3an1 1347	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
288	5, 38, 284, 285, 287	mp4an 677	. . . . . . . . . . 11
289		df-4 10670	. . . . . . . . . . . . . . . 16
290	289	oveq2i 6316	. . . . . . . . . . . . . . 15
291		3nn0 10887	. . . . . . . . . . . . . . . 16
292		expp1 12276	. . . . . . . . . . . . . . . 16 $/\$
293	89, 291, 292	mp2an 676	. . . . . . . . . . . . . . 15
294	22	oveq1i 6315	. . . . . . . . . . . . . . 15
295	290, 293, 294	3eqtri 2462	. . . . . . . . . . . . . 14
296	295	oveq1i 6315	. . . . . . . . . . . . 13
297	5, 89, 32	mulassi 9651	. . . . . . . . . . . . 13
298	193	oveq2i 6316	. . . . . . . . . . . . 13
299	296, 297, 298	3eqtri 2462	. . . . . . . . . . . 12
300		4p3e7 10745	. . . . . . . . . . . . . . . 16
301		5p2e7 10747	. . . . . . . . . . . . . . . 16
302	112, 89	addcomi 9823	. . . . . . . . . . . . . . . 16
303	300, 301, 302	3eqtr2i 2464	. . . . . . . . . . . . . . 15
304	303	oveq2i 6316	. . . . . . . . . . . . . 14
305		expadd 12311	. . . . . . . . . . . . . . 15 $/\$ $/\$
306	89, 206, 291, 305	mp3an 1360	. . . . . . . . . . . . . 14
307		2nn0 10886	. . . . . . . . . . . . . . 15
308		expadd 12311	. . . . . . . . . . . . . . 15 $/\$ $/\$
309	89, 307, 90, 308	mp3an 1360	. . . . . . . . . . . . . 14
310	304, 306, 309	3eqtr3i 2466	. . . . . . . . . . . . 13
311	22	oveq2i 6316	. . . . . . . . . . . . 13
312		sq2 12368	. . . . . . . . . . . . . 14
313	312	oveq1i 6315	. . . . . . . . . . . . 13
314	310, 311, 313	3eqtr3i 2466	. . . . . . . . . . . 12
315	299, 314	oveq12i 6317	. . . . . . . . . . 11
316	288, 315	eqtr3i 2460	. . . . . . . . . 10
317	280, 281, 316	3brtr4i 4454	. . . . . . . . 9
318	167, 11, 38	redivcli 10373	. . . . . . . . . 10
319		1re 9641	. . . . . . . . . 10
320		ltsub2 10110	. . . . . . . . . 10 $/\$ $/\$
321	176, 318, 319, 320	mp3an 1360	. . . . . . . . 9
322	317, 321	mpbi 211	. . . . . . . 8
323	256, 322	eqbrtrri 4447	. . . . . . 7
324	243, 11, 38	redivcli 10373	. . . . . . . 8
325	173, 11, 38	redivcli 10373	. . . . . . . 8
326	319, 176	resubcli 9935	. . . . . . . 8
327	324, 325, 326	lttri 9759	. . . . . . 7 $/\$
328	245, 323, 327	mp2an 676	. . . . . 6
329	324, 176, 319	ltaddsubi 10174	. . . . . 6
330	328, 329	mpbir 212	. . . . 5
331	205, 330	eqbrtri 4445	. . . 4
332		1lt2 10776	. . . . . . 7
333		rplogcl 23409	. . . . . . 7 $/\$
334	53, 332, 333	mp2an 676	. . . . . 6
335		rpgt0 11313	. . . . . 6
336	334, 335	ax-mp 5	. . . . 5
337	180, 319, 36, 336	ltmul1ii 10535	. . . 4
338	331, 337	mpbi 211	. . 3
339	37	mulid2i 9645	. . . 4
340	339	eqcomi 2442	. . 3
341	338, 166, 340	3brtr4i 4454	. 2 ;
342	182, 341	pm3.2i 456	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 187 $/\$ wa 370

wceq 1437

wcel 1870

wne 2625 class class class wbr 4426

cmpt 4484

cfv 5601 (class class class)co 6305

cc 9536

cr 9537

cc0 9538

c1 9539

caddc 9541

cmul 9543

clt 9674

cle 9675

cmin 9859

cdiv 10268

cn 10609

c2 10659

c3 10660

c4 10661

c5 10662

c6 10663

c7 10664

c8 10665

c9 10666

c10 10667

cn0 10869

cz 10937 ;cdc 11051

crp 11302

cexp 12269

csqrt 13275

clog 23360

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616 ax-addf 9617 ax-mulf 9618

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-iin 4305 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 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 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-supp 6926 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-map 7482 df-pm 7483 df-ixp 7531 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-fsupp 7890 df-fi 7931 df-sup 7962 df-inf 7963 df-oi 8025 df-card 8372 df-cda 8596 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11783 df-fzo 11914 df-fl 12025 df-mod 12094 df-seq 12211 df-exp 12270 df-fac 12457 df-bc 12485 df-hash 12513 df-shft 13109 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-limsup 13504 df-clim 13530 df-rlim 13531 df-sum 13731 df-ef 14099 df-sin 14101 df-cos 14102 df-pi 14104 df-struct 15077 df-ndx 15078 df-slot 15079 df-base 15080 df-sets 15081 df-ress 15082 df-plusg 15156 df-mulr 15157 df-starv 15158 df-sca 15159 df-vsca 15160 df-ip 15161 df-tset 15162 df-ple 15163 df-ds 15165 df-unif 15166 df-hom 15167 df-cco 15168 df-rest 15271 df-topn 15272 df-0g 15290 df-gsum 15291 df-topgen 15292 df-pt 15293 df-prds 15296 df-xrs 15350 df-qtop 15355 df-imas 15356 df-xps 15358 df-mre 15434 df-mrc 15435 df-acs 15437 df-mgm 16430 df-sgrp 16469 df-mnd 16479 df-submnd 16525 df-mulg 16618 df-cntz 16913 df-cmn 17358 df-psmet 18888 df-xmet 18889 df-met 18890 df-bl 18891 df-mopn 18892 df-fbas 18893 df-fg 18894 df-cnfld 18897 df-top 19843 df-bases 19844 df-topon 19845 df-topsp 19846 df-cld 19956 df-ntr 19957 df-cls 19958 df-nei 20036 df-lp 20074 df-perf 20075 df-cn 20165 df-cnp 20166 df-haus 20253 df-tx 20499 df-hmeo 20692 df-fil 20783 df-fm 20875 df-flim 20876 df-flf 20877 df-xms 21257 df-ms 21258 df-tms 21259 df-cncf 21797 df-limc 22689 df-dv 22690 df-log 23362

This theorem is referenced by: bposlem9 24074

W3C validator