bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 23542

Description: Lemma for bpos 23544. 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 10823	. . . . 5
2		4nn 10702	. . . . 5
3	1, 2	decnncl 10998	. . . 4 ;
4		fveq2 5856	. . . . . . . . . . . . . 14 ; ;
5		8cn 10628	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 12228	. . . . . . . . . . . . . . . . 17
7		8t8e64 11079	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2472	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5859	. . . . . . . . . . . . . . 15 ;
10		0re 9599	. . . . . . . . . . . . . . . . 17
11		8re 10627	. . . . . . . . . . . . . . . . 17
12		8pos 10643	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9710	. . . . . . . . . . . . . . . 16
14	11	sqrtsqi 13188	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2474	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2500	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5860	. . . . . . . . . . . 12 ;
19		8nn 10706	. . . . . . . . . . . . 13
20		nnrp 11239	. . . . . . . . . . . . 13
21		fveq2 5856	. . . . . . . . . . . . . . . . 17
22		cu2 12247	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5859	. . . . . . . . . . . . . . . . . 18
24		2rp 11235	. . . . . . . . . . . . . . . . . . 19
25		3z 10904	. . . . . . . . . . . . . . . . . . 19
26		relogexp 22956	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2474	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2500	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6299	. . . . . . . . . . . . . . 15
32		3cn 10617	. . . . . . . . . . . . . . . 16
33		2nn 10700	. . . . . . . . . . . . . . . . . 18
34		nnrp 11239	. . . . . . . . . . . . . . . . . 18
35		relogcl 22939	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9611	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10577	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10309	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2500	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6309	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5941	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2500	. . . . . . . . . . 11 ;
46	45	oveq2d 6297	. . . . . . . . . 10 ;
47		sqrt2re 13964	. . . . . . . . . . . . 13
48	47	recni 9611	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10293	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9608	. . . . . . . . . . 11
51		4cn 10620	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9778	. . . . . . . . . . . . . . 15
53		2re 10612	. . . . . . . . . . . . . . . . 17
54		0le2 10633	. . . . . . . . . . . . . . . . 17
55		remsqsqrt 13071	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 672	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6292	. . . . . . . . . . . . . . 15
58		4t2e8 10696	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2476	. . . . . . . . . . . . . 14
60	59	oveq2i 6292	. . . . . . . . . . . . 13
61	51, 48	mulcli 9604	. . . . . . . . . . . . . . 15
62		nnrp 11239	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrtcl 13079	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11251	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 672	. . . . . . . . . . . . . . . 16
68		rpne0 11245	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 11245	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10253	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1312	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 673	. . . . . . . . . . . . . 14
75		4ne0 10639	. . . . . . . . . . . . . . 15
76		divdiv1 10262	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1312	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 673	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2475	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10307	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2481	. . . . . . . . . . . 12
82	81	oveq1i 6291	. . . . . . . . . . 11
83	50, 82	eqtr3i 2474	. . . . . . . . . 10
84	46, 83	syl6eq 2500	. . . . . . . . 9 ;
85		oveq1 6288	. . . . . . . . . . . . . 14 ; ;
86		df-6 10605	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6292	. . . . . . . . . . . . . . . . 17
88		2exp6 14553	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10613	. . . . . . . . . . . . . . . . . 18
90		5nn0 10822	. . . . . . . . . . . . . . . . . 18
91		expp1 12154	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 672	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2480	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6291	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 12160	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 672	. . . . . . . . . . . . . . . . 17
97	96	nncni 10553	. . . . . . . . . . . . . . . 16
98		2ne0 10635	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10298	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2472	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2500	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5860	. . . . . . . . . . . 12 ;
103		nnrp 11239	. . . . . . . . . . . . 13
104		fveq2 5856	. . . . . . . . . . . . . . . . 17
105		5nn 10703	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10895	. . . . . . . . . . . . . . . . . 18
107		relogexp 22956	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 672	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2500	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6299	. . . . . . . . . . . . . . 15
112		5cn 10622	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10577	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10309	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2500	. . . . . . . . . . . . . 14
116		ovex 6309	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5941	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2500	. . . . . . . . . . 11 ;
120	119	oveq2d 6297	. . . . . . . . . 10 ;
121		9cn 10630	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10293	. . . . . . . . . . 11
123	112, 97, 113	divcli 10293	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9608	. . . . . . . . . 10
125	120, 124	syl6eqr 2502	. . . . . . . . 9 ;
126	84, 125	oveq12d 6299	. . . . . . . 8 ;
127	32, 51, 75	divcli 10293	. . . . . . . . . 10
128	127, 48, 71	divcli 10293	. . . . . . . . 9
129	122, 123	mulcli 9604	. . . . . . . . 9
130	128, 129, 37	adddiri 9610	. . . . . . . 8
131	126, 130	syl6eqr 2502	. . . . . . 7 ;
132		oveq2 6289	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5860	. . . . . . . . . 10 ; ;
134	3	nnrei 10552	. . . . . . . . . . . 12 ;
135	3	nngt0i 10576	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9710	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrtmulii 13200	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6292	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2472	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2500	. . . . . . . . 9 ;
141	140	oveq2d 6297	. . . . . . . 8 ;
142	48, 5	mulcli 9604	. . . . . . . . . 10
143		rpmulcl 11251	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 663	. . . . . . . . . . 11
145		rpne0 11245	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10231	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1325	. . . . . . . . 9
149	48, 5	mulcomi 9605	. . . . . . . . . . . 12
150	149	oveq2i 6292	. . . . . . . . . . 11
151		recdiv2 10264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 673	. . . . . . . . . . 11
153	150, 152	eqtr4i 2475	. . . . . . . . . 10
154	153	oveq1i 6291	. . . . . . . . 9
155	148, 154	eqtri 2472	. . . . . . . 8
156	141, 155	syl6eq 2500	. . . . . . 7 ;
157	131, 156	oveq12d 6299	. . . . . 6 ;
158	128, 129	addcli 9603	. . . . . . 7
159	5, 38	reccli 10281	. . . . . . . 8
160	159, 48, 71	divcli 10293	. . . . . . 7
161	158, 160, 37	adddiri 9610	. . . . . 6
162	157, 161	syl6eqr 2502	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6309	. . . . 5
165	162, 163, 164	fvmpt 5941	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10616	. . . . . . . 8
168		4re 10619	. . . . . . . 8
169	167, 168, 75	redivcli 10318	. . . . . . 7
170	169, 47, 71	redivcli 10318	. . . . . 6
171		9re 10629	. . . . . . . 8
172	171, 168, 75	redivcli 10318	. . . . . . 7
173		5re 10621	. . . . . . . 8
174	96	nnrei 10552	. . . . . . . 8
175	173, 174, 113	redivcli 10318	. . . . . . 7
176	172, 175	remulcli 9613	. . . . . 6
177	170, 176	readdcli 9612	. . . . 5
178	11, 38	rereccli 10316	. . . . . 6
179	178, 47, 71	redivcli 10318	. . . . 5
180	177, 179	readdcli 9612	. . . 4
181	180, 36	remulcli 9613	. . 3
182	166, 181	eqeltri 2527	. 2 ;
183	128, 129, 160	add32i 9802	. . . . . 6
184		6cn 10624	. . . . . . . . . . 11
185		ax-1cn 9553	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10308	. . . . . . . . . 10
187		df-7 10606	. . . . . . . . . . 11
188	187	oveq1i 6291	. . . . . . . . . 10
189		divcan5 10253	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1312	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 673	. . . . . . . . . . . 12
192		3t2e6 10694	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9606	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9606	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6293	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2474	. . . . . . . . . . 11
197	196	oveq1i 6291	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2483	. . . . . . . . 9
199	198	oveq1i 6291	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10308	. . . . . . . 8
201		7cn 10626	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10306	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2480	. . . . . . 7
204	203	oveq1i 6291	. . . . . 6
205	183, 204	eqtri 2472	. . . . 5
206		4nn0 10821	. . . . . . . . . . . 12
207		9nn0 10826	. . . . . . . . . . . 12
208		0nn0 10817	. . . . . . . . . . . 12
209		9lt10 10745	. . . . . . . . . . . 12
210		4lt5 10715	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 11007	. . . . . . . . . . 11 ; ;
212		7t7e49 11072	. . . . . . . . . . 11 ;
213	56	oveq1i 6291	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9780	. . . . . . . . . . . 12
215		5t2e10 10697	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9606	. . . . . . . . . . . . . 14
217	216	oveq1i 6291	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9608	. . . . . . . . . . . . 13
219	90	dec0u 11000	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2480	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2480	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4465	. . . . . . . . . 10
223		7re 10625	. . . . . . . . . . . 12
224		7pos 10642	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9710	. . . . . . . . . . 11
226		nnrp 11239	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11251	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 672	. . . . . . . . . . . 12
230		rpge0 11242	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 11236	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10465	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 672	. . . . . . . . . 10
236	222, 235	mpbir 209	. . . . . . . . 9
237		rpgt0 11241	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10424	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1315	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 672	. . . . . . . . 9
242	236, 241	mpbir 209	. . . . . . . 8
243	223, 47, 71	redivcli 10318	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10482	. . . . . . . 8
245	242, 244	mpbi 208	. . . . . . 7
246		divsubdir 10247	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1315	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 672	. . . . . . . . 9
249		5p3e8 10681	. . . . . . . . . . . 12
250	249	oveq1i 6291	. . . . . . . . . . 11
251	112, 32	pncan3oi 9841	. . . . . . . . . . 11
252	250, 251	eqtr3i 2474	. . . . . . . . . 10
253	252	oveq1i 6291	. . . . . . . . 9
254	5, 38	dividi 10284	. . . . . . . . . 10
255	254	oveq1i 6291	. . . . . . . . 9
256	248, 253, 255	3eqtr3ri 2481	. . . . . . . 8
257		5lt8 10732	. . . . . . . . . . . . 13
258	11, 173	remulcli 9613	. . . . . . . . . . . . . 14
259	173, 11, 258	ltadd2i 9718	. . . . . . . . . . . . 13
260	257, 259	mpbi 208	. . . . . . . . . . . 12
261		df-9 10608	. . . . . . . . . . . . . 14
262	261	oveq1i 6291	. . . . . . . . . . . . 13
263	5, 185, 112	adddiri 9610	. . . . . . . . . . . . 13
264	112	mulid2i 9602	. . . . . . . . . . . . . 14
265	264	oveq2i 6292	. . . . . . . . . . . . 13
266	262, 263, 265	3eqtri 2476	. . . . . . . . . . . 12
267	86	oveq2i 6292	. . . . . . . . . . . . 13
268	5, 112, 185	adddii 9609	. . . . . . . . . . . . 13
269	5	mulid1i 9601	. . . . . . . . . . . . . 14
270	269	oveq2i 6292	. . . . . . . . . . . . 13
271	267, 268, 270	3eqtri 2476	. . . . . . . . . . . 12
272	260, 266, 271	3brtr4i 4465	. . . . . . . . . . 11
273	171, 173	remulcli 9613	. . . . . . . . . . . 12
274		6re 10623	. . . . . . . . . . . . 13
275	11, 274	remulcli 9613	. . . . . . . . . . . 12
276	168, 174	remulcli 9613	. . . . . . . . . . . 12
277	2, 96	nnmulcli 10567	. . . . . . . . . . . . 13
278	277	nngt0i 10576	. . . . . . . . . . . 12
279	273, 275, 276, 278	ltdiv1ii 10482	. . . . . . . . . . 11
280	272, 279	mpbi 208	. . . . . . . . . 10
281	121, 51, 112, 97, 75, 113	divmuldivi 10311	. . . . . . . . . 10
282		nnexpcl 12160	. . . . . . . . . . . . . 14 $/\$
283	33, 206, 282	mp2an 672	. . . . . . . . . . . . 13
284	283	nncni 10553	. . . . . . . . . . . 12
285	283	nnne0i 10577	. . . . . . . . . . . 12
286		divcan5 10253	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
287	32, 286	mp3an1 1312	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
288	5, 38, 284, 285, 287	mp4an 673	. . . . . . . . . . 11
289		df-4 10603	. . . . . . . . . . . . . . . 16
290	289	oveq2i 6292	. . . . . . . . . . . . . . 15
291		3nn0 10820	. . . . . . . . . . . . . . . 16
292		expp1 12154	. . . . . . . . . . . . . . . 16 $/\$
293	89, 291, 292	mp2an 672	. . . . . . . . . . . . . . 15
294	22	oveq1i 6291	. . . . . . . . . . . . . . 15
295	290, 293, 294	3eqtri 2476	. . . . . . . . . . . . . 14
296	295	oveq1i 6291	. . . . . . . . . . . . 13
297	5, 89, 32	mulassi 9608	. . . . . . . . . . . . 13
298	193	oveq2i 6292	. . . . . . . . . . . . 13
299	296, 297, 298	3eqtri 2476	. . . . . . . . . . . 12
300		4p3e7 10678	. . . . . . . . . . . . . . . 16
301		5p2e7 10680	. . . . . . . . . . . . . . . 16
302	112, 89	addcomi 9774	. . . . . . . . . . . . . . . 16
303	300, 301, 302	3eqtr2i 2478	. . . . . . . . . . . . . . 15
304	303	oveq2i 6292	. . . . . . . . . . . . . 14
305		expadd 12189	. . . . . . . . . . . . . . 15 $/\$ $/\$
306	89, 206, 291, 305	mp3an 1325	. . . . . . . . . . . . . 14
307		2nn0 10819	. . . . . . . . . . . . . . 15
308		expadd 12189	. . . . . . . . . . . . . . 15 $/\$ $/\$
309	89, 307, 90, 308	mp3an 1325	. . . . . . . . . . . . . 14
310	304, 306, 309	3eqtr3i 2480	. . . . . . . . . . . . 13
311	22	oveq2i 6292	. . . . . . . . . . . . 13
312		sq2 12245	. . . . . . . . . . . . . 14
313	312	oveq1i 6291	. . . . . . . . . . . . 13
314	310, 311, 313	3eqtr3i 2480	. . . . . . . . . . . 12
315	299, 314	oveq12i 6293	. . . . . . . . . . 11
316	288, 315	eqtr3i 2474	. . . . . . . . . 10
317	280, 281, 316	3brtr4i 4465	. . . . . . . . 9
318	167, 11, 38	redivcli 10318	. . . . . . . . . 10
319		1re 9598	. . . . . . . . . 10
320		ltsub2 10056	. . . . . . . . . 10 $/\$ $/\$
321	176, 318, 319, 320	mp3an 1325	. . . . . . . . 9
322	317, 321	mpbi 208	. . . . . . . 8
323	256, 322	eqbrtrri 4458	. . . . . . 7
324	243, 11, 38	redivcli 10318	. . . . . . . 8
325	173, 11, 38	redivcli 10318	. . . . . . . 8
326	319, 176	resubcli 9886	. . . . . . . 8
327	324, 325, 326	lttri 9713	. . . . . . 7 $/\$
328	245, 323, 327	mp2an 672	. . . . . 6
329	324, 176, 319	ltaddsubi 10121	. . . . . 6
330	328, 329	mpbir 209	. . . . 5
331	205, 330	eqbrtri 4456	. . . 4
332		1lt2 10709	. . . . . . 7
333		rplogcl 22965	. . . . . . 7 $/\$
334	53, 332, 333	mp2an 672	. . . . . 6
335		rpgt0 11241	. . . . . 6
336	334, 335	ax-mp 5	. . . . 5
337	180, 319, 36, 336	ltmul1ii 10481	. . . 4
338	331, 337	mpbi 208	. . 3
339	37	mulid2i 9602	. . . 4
340	339	eqcomi 2456	. . 3
341	338, 166, 340	3brtr4i 4465	. 2 ;
342	182, 341	pm3.2i 455	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 184 $/\$ wa 369

wceq 1383

wcel 1804

wne 2638 class class class wbr 4437

cmpt 4495

cfv 5578 (class class class)co 6281

cc 9493

cr 9494

cc0 9495

c1 9496

caddc 9498

cmul 9500

clt 9631

cle 9632

cmin 9810

cdiv 10213

cn 10543

c2 10592

c3 10593

c4 10594

c5 10595

c6 10596

c7 10597

c8 10598

c9 10599

c10 10600

cn0 10802

cz 10871 ;cdc 10985

crp 11230

cexp 12147

csqrt 13047

clog 22918

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573 ax-addf 9574 ax-mulf 9575

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-iin 4318 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-of 6525 df-om 6686 df-1st 6785 df-2nd 6786 df-supp 6904 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-map 7424 df-pm 7425 df-ixp 7472 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-fsupp 7832 df-fi 7873 df-sup 7903 df-oi 7938 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10214 df-nn 10544 df-2 10601 df-3 10602 df-4 10603 df-5 10604 df-6 10605 df-7 10606 df-8 10607 df-9 10608 df-10 10609 df-n0 10803 df-z 10872 df-dec 10986 df-uz 11092 df-q 11193 df-rp 11231 df-xneg 11328 df-xadd 11329 df-xmul 11330 df-ioo 11543 df-ioc 11544 df-ico 11545 df-icc 11546 df-fz 11683 df-fzo 11806 df-fl 11910 df-mod 11978 df-seq 12089 df-exp 12148 df-fac 12335 df-bc 12362 df-hash 12387 df-shft 12881 df-cj 12913 df-re 12914 df-im 12915 df-sqrt 13049 df-abs 13050 df-limsup 13275 df-clim 13292 df-rlim 13293 df-sum 13490 df-ef 13784 df-sin 13786 df-cos 13787 df-pi 13789 df-struct 14615 df-ndx 14616 df-slot 14617 df-base 14618 df-sets 14619 df-ress 14620 df-plusg 14691 df-mulr 14692 df-starv 14693 df-sca 14694 df-vsca 14695 df-ip 14696 df-tset 14697 df-ple 14698 df-ds 14700 df-unif 14701 df-hom 14702 df-cco 14703 df-rest 14801 df-topn 14802 df-0g 14820 df-gsum 14821 df-topgen 14822 df-pt 14823 df-prds 14826 df-xrs 14880 df-qtop 14885 df-imas 14886 df-xps 14888 df-mre 14964 df-mrc 14965 df-acs 14967 df-mgm 15850 df-sgrp 15889 df-mnd 15899 df-submnd 15945 df-mulg 16038 df-cntz 16333 df-cmn 16778 df-psmet 18389 df-xmet 18390 df-met 18391 df-bl 18392 df-mopn 18393 df-fbas 18394 df-fg 18395 df-cnfld 18399 df-top 19376 df-bases 19378 df-topon 19379 df-topsp 19380 df-cld 19497 df-ntr 19498 df-cls 19499 df-nei 19576 df-lp 19614 df-perf 19615 df-cn 19705 df-cnp 19706 df-haus 19793 df-tx 20040 df-hmeo 20233 df-fil 20324 df-fm 20416 df-flim 20417 df-flf 20418 df-xms 20800 df-ms 20801 df-tms 20802 df-cncf 21359 df-limc 22247 df-dv 22248 df-log 22920

This theorem is referenced by: bposlem9 23543

W3C validator