bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 22605

Description: Lemma for bpos 22607. 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 10592	. . . . 5
2		4nn 10473	. . . . 5
3	1, 2	decnncl 10760	. . . 4 ;
4		fveq2 5686	. . . . . . . . . . . . . 14 ; ;
5		8cn 10399	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 11937	. . . . . . . . . . . . . . . . 17
7		8t8e64 10841	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2458	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5689	. . . . . . . . . . . . . . 15 ;
10		0re 9378	. . . . . . . . . . . . . . . . 17
11		8re 10398	. . . . . . . . . . . . . . . . 17
12		8pos 10414	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9489	. . . . . . . . . . . . . . . 16
14	11	sqrsqi 12854	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2460	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2486	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5690	. . . . . . . . . . . 12 ;
19		8nn 10477	. . . . . . . . . . . . 13
20		nnrp 10992	. . . . . . . . . . . . 13
21		fveq2 5686	. . . . . . . . . . . . . . . . 17
22		cu2 11956	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5689	. . . . . . . . . . . . . . . . . 18
24		2rp 10988	. . . . . . . . . . . . . . . . . . 19
25		3z 10671	. . . . . . . . . . . . . . . . . . 19
26		relogexp 22019	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2460	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2486	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6104	. . . . . . . . . . . . . . 15
32		3cn 10388	. . . . . . . . . . . . . . . 16
33		2nn 10471	. . . . . . . . . . . . . . . . . 18
34		nnrp 10992	. . . . . . . . . . . . . . . . . 18
35		relogcl 22002	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9390	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10348	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10081	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2486	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6111	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5769	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2486	. . . . . . . . . . 11 ;
46	45	oveq2d 6102	. . . . . . . . . 10 ;
47		sqr2re 13524	. . . . . . . . . . . . 13
48	47	recni 9390	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10065	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9387	. . . . . . . . . . 11
51		4cn 10391	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9556	. . . . . . . . . . . . . . 15
53		2re 10383	. . . . . . . . . . . . . . . . 17
54		0le2 10404	. . . . . . . . . . . . . . . . 17
55		remsqsqr 12738	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 672	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6097	. . . . . . . . . . . . . . 15
58		4t2e8 10467	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2462	. . . . . . . . . . . . . 14
60	59	oveq2i 6097	. . . . . . . . . . . . 13
61	51, 48	mulcli 9383	. . . . . . . . . . . . . . 15
62		nnrp 10992	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrcl 12746	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11004	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 672	. . . . . . . . . . . . . . . 16
68		rpne0 10998	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 10998	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10025	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1301	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 673	. . . . . . . . . . . . . 14
75		4ne0 10410	. . . . . . . . . . . . . . 15
76		divdiv1 10034	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1301	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 673	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2461	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10079	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2467	. . . . . . . . . . . 12
82	81	oveq1i 6096	. . . . . . . . . . 11
83	50, 82	eqtr3i 2460	. . . . . . . . . 10
84	46, 83	syl6eq 2486	. . . . . . . . 9 ;
85		oveq1 6093	. . . . . . . . . . . . . 14 ; ;
86		df-6 10376	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6097	. . . . . . . . . . . . . . . . 17
88		2exp6 14107	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10384	. . . . . . . . . . . . . . . . . 18
90		5nn0 10591	. . . . . . . . . . . . . . . . . 18
91		expp1 11864	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 672	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2466	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6096	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 11870	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 672	. . . . . . . . . . . . . . . . 17
97	96	nncni 10324	. . . . . . . . . . . . . . . 16
98		2ne0 10406	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10070	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2458	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2486	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5690	. . . . . . . . . . . 12 ;
103		nnrp 10992	. . . . . . . . . . . . 13
104		fveq2 5686	. . . . . . . . . . . . . . . . 17
105		5nn 10474	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10662	. . . . . . . . . . . . . . . . . 18
107		relogexp 22019	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 672	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2486	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6104	. . . . . . . . . . . . . . 15
112		5cn 10393	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10348	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10081	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2486	. . . . . . . . . . . . . 14
116		ovex 6111	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5769	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2486	. . . . . . . . . . 11 ;
120	119	oveq2d 6102	. . . . . . . . . 10 ;
121		9cn 10401	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10065	. . . . . . . . . . 11
123	112, 97, 113	divcli 10065	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9387	. . . . . . . . . 10
125	120, 124	syl6eqr 2488	. . . . . . . . 9 ;
126	84, 125	oveq12d 6104	. . . . . . . 8 ;
127	32, 51, 75	divcli 10065	. . . . . . . . . 10
128	127, 48, 71	divcli 10065	. . . . . . . . 9
129	122, 123	mulcli 9383	. . . . . . . . 9
130	128, 129, 37	adddiri 9389	. . . . . . . 8
131	126, 130	syl6eqr 2488	. . . . . . 7 ;
132		oveq2 6094	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5690	. . . . . . . . . 10 ; ;
134	3	nnrei 10323	. . . . . . . . . . . 12 ;
135	3	nngt0i 10347	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9489	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrmulii 12866	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6097	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2458	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2486	. . . . . . . . 9 ;
141	140	oveq2d 6102	. . . . . . . 8 ;
142	48, 5	mulcli 9383	. . . . . . . . . 10
143		rpmulcl 11004	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 663	. . . . . . . . . . 11
145		rpne0 10998	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10003	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1314	. . . . . . . . 9
149	48, 5	mulcomi 9384	. . . . . . . . . . . 12
150	149	oveq2i 6097	. . . . . . . . . . 11
151		recdiv2 10036	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 673	. . . . . . . . . . 11
153	150, 152	eqtr4i 2461	. . . . . . . . . 10
154	153	oveq1i 6096	. . . . . . . . 9
155	148, 154	eqtri 2458	. . . . . . . 8
156	141, 155	syl6eq 2486	. . . . . . 7 ;
157	131, 156	oveq12d 6104	. . . . . 6 ;
158	128, 129	addcli 9382	. . . . . . 7
159	5, 38	reccli 10053	. . . . . . . 8
160	159, 48, 71	divcli 10065	. . . . . . 7
161	158, 160, 37	adddiri 9389	. . . . . 6
162	157, 161	syl6eqr 2488	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6111	. . . . 5
165	162, 163, 164	fvmpt 5769	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10387	. . . . . . . 8
168		4re 10390	. . . . . . . 8
169	167, 168, 75	redivcli 10090	. . . . . . 7
170	169, 47, 71	redivcli 10090	. . . . . 6
171		9re 10400	. . . . . . . 8
172	171, 168, 75	redivcli 10090	. . . . . . 7
173		5re 10392	. . . . . . . 8
174	96	nnrei 10323	. . . . . . . 8
175	173, 174, 113	redivcli 10090	. . . . . . 7
176	172, 175	remulcli 9392	. . . . . 6
177	170, 176	readdcli 9391	. . . . 5
178	11, 38	rereccli 10088	. . . . . 6
179	178, 47, 71	redivcli 10090	. . . . 5
180	177, 179	readdcli 9391	. . . 4
181	180, 36	remulcli 9392	. . 3
182	166, 181	eqeltri 2508	. 2 ;
183	128, 129, 160	add32i 9580	. . . . . 6
184		6cn 10395	. . . . . . . . . . 11
185		ax-1cn 9332	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10080	. . . . . . . . . 10
187		df-7 10377	. . . . . . . . . . 11
188	187	oveq1i 6096	. . . . . . . . . 10
189		divcan5 10025	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1301	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 673	. . . . . . . . . . . 12
192		3t2e6 10465	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9385	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9385	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6098	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2460	. . . . . . . . . . 11
197	196	oveq1i 6096	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2469	. . . . . . . . 9
199	198	oveq1i 6096	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10080	. . . . . . . 8
201		7cn 10397	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10078	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2466	. . . . . . 7
204	203	oveq1i 6096	. . . . . 6
205	183, 204	eqtri 2458	. . . . 5
206		4nn0 10590	. . . . . . . . . . . 12
207		9nn0 10595	. . . . . . . . . . . 12
208		0nn0 10586	. . . . . . . . . . . 12
209		9lt10 10516	. . . . . . . . . . . 12
210		4lt5 10486	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 10769	. . . . . . . . . . 11 ; ;
212		7t7e49 10834	. . . . . . . . . . 11 ;
213	56	oveq1i 6096	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9558	. . . . . . . . . . . 12
215		5t2e10 10468	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9385	. . . . . . . . . . . . . 14
217	216	oveq1i 6096	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9387	. . . . . . . . . . . . 13
219	90	dec0u 10762	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2466	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2466	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4315	. . . . . . . . . 10
223		7re 10396	. . . . . . . . . . . 12
224		7pos 10413	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9489	. . . . . . . . . . 11
226		nnrp 10992	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11004	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 672	. . . . . . . . . . . 12
230		rpge0 10995	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 10989	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10237	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 672	. . . . . . . . . 10
236	222, 235	mpbir 209	. . . . . . . . 9
237		rpgt0 10994	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10196	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1304	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 672	. . . . . . . . 9
242	236, 241	mpbir 209	. . . . . . . 8
243	223, 47, 71	redivcli 10090	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10254	. . . . . . . 8
245	242, 244	mpbi 208	. . . . . . 7
246		divsubdir 10019	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1304	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 672	. . . . . . . . 9
249		5p3e8 10452	. . . . . . . . . . . 12
250	249	oveq1i 6096	. . . . . . . . . . 11
251		pncan 9608	. . . . . . . . . . . 12 $/\$
252	112, 32, 251	mp2an 672	. . . . . . . . . . 11
253	250, 252	eqtr3i 2460	. . . . . . . . . 10
254	253	oveq1i 6096	. . . . . . . . 9
255	5, 38	dividi 10056	. . . . . . . . . 10
256	255	oveq1i 6096	. . . . . . . . 9
257	248, 254, 256	3eqtr3ri 2467	. . . . . . . 8
258		5lt8 10503	. . . . . . . . . . . . 13
259	11, 173	remulcli 9392	. . . . . . . . . . . . . 14
260	173, 11, 259	ltadd2i 9497	. . . . . . . . . . . . 13
261	258, 260	mpbi 208	. . . . . . . . . . . 12
262		df-9 10379	. . . . . . . . . . . . . 14
263	262	oveq1i 6096	. . . . . . . . . . . . 13
264	5, 185, 112	adddiri 9389	. . . . . . . . . . . . 13
265	112	mulid2i 9381	. . . . . . . . . . . . . 14
266	265	oveq2i 6097	. . . . . . . . . . . . 13
267	263, 264, 266	3eqtri 2462	. . . . . . . . . . . 12
268	86	oveq2i 6097	. . . . . . . . . . . . 13
269	5, 112, 185	adddii 9388	. . . . . . . . . . . . 13
270	5	mulid1i 9380	. . . . . . . . . . . . . 14
271	270	oveq2i 6097	. . . . . . . . . . . . 13
272	268, 269, 271	3eqtri 2462	. . . . . . . . . . . 12
273	261, 267, 272	3brtr4i 4315	. . . . . . . . . . 11
274	171, 173	remulcli 9392	. . . . . . . . . . . 12
275		6re 10394	. . . . . . . . . . . . 13
276	11, 275	remulcli 9392	. . . . . . . . . . . 12
277	168, 174	remulcli 9392	. . . . . . . . . . . 12
278	2, 96	nnmulcli 10338	. . . . . . . . . . . . 13
279	278	nngt0i 10347	. . . . . . . . . . . 12
280	274, 276, 277, 279	ltdiv1ii 10254	. . . . . . . . . . 11
281	273, 280	mpbi 208	. . . . . . . . . 10
282	121, 51, 112, 97, 75, 113	divmuldivi 10083	. . . . . . . . . 10
283		nnexpcl 11870	. . . . . . . . . . . . . 14 $/\$
284	33, 206, 283	mp2an 672	. . . . . . . . . . . . 13
285	284	nncni 10324	. . . . . . . . . . . 12
286	284	nnne0i 10348	. . . . . . . . . . . 12
287		divcan5 10025	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
288	32, 287	mp3an1 1301	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
289	5, 38, 285, 286, 288	mp4an 673	. . . . . . . . . . 11
290		df-4 10374	. . . . . . . . . . . . . . . 16
291	290	oveq2i 6097	. . . . . . . . . . . . . . 15
292		3nn0 10589	. . . . . . . . . . . . . . . 16
293		expp1 11864	. . . . . . . . . . . . . . . 16 $/\$
294	89, 292, 293	mp2an 672	. . . . . . . . . . . . . . 15
295	22	oveq1i 6096	. . . . . . . . . . . . . . 15
296	291, 294, 295	3eqtri 2462	. . . . . . . . . . . . . 14
297	296	oveq1i 6096	. . . . . . . . . . . . 13
298	5, 89, 32	mulassi 9387	. . . . . . . . . . . . 13
299	193	oveq2i 6097	. . . . . . . . . . . . 13
300	297, 298, 299	3eqtri 2462	. . . . . . . . . . . 12
301		4p3e7 10449	. . . . . . . . . . . . . . . 16
302		5p2e7 10451	. . . . . . . . . . . . . . . 16
303	112, 89	addcomi 9552	. . . . . . . . . . . . . . . 16
304	301, 302, 303	3eqtr2i 2464	. . . . . . . . . . . . . . 15
305	304	oveq2i 6097	. . . . . . . . . . . . . 14
306		expadd 11898	. . . . . . . . . . . . . . 15 $/\$ $/\$
307	89, 206, 292, 306	mp3an 1314	. . . . . . . . . . . . . 14
308		2nn0 10588	. . . . . . . . . . . . . . 15
309		expadd 11898	. . . . . . . . . . . . . . 15 $/\$ $/\$
310	89, 308, 90, 309	mp3an 1314	. . . . . . . . . . . . . 14
311	305, 307, 310	3eqtr3i 2466	. . . . . . . . . . . . 13
312	22	oveq2i 6097	. . . . . . . . . . . . 13
313		sq2 11954	. . . . . . . . . . . . . 14
314	313	oveq1i 6096	. . . . . . . . . . . . 13
315	311, 312, 314	3eqtr3i 2466	. . . . . . . . . . . 12
316	300, 315	oveq12i 6098	. . . . . . . . . . 11
317	289, 316	eqtr3i 2460	. . . . . . . . . 10
318	281, 282, 317	3brtr4i 4315	. . . . . . . . 9
319	167, 11, 38	redivcli 10090	. . . . . . . . . 10
320		1re 9377	. . . . . . . . . 10
321		ltsub2 9828	. . . . . . . . . 10 $/\$ $/\$
322	176, 319, 320, 321	mp3an 1314	. . . . . . . . 9
323	318, 322	mpbi 208	. . . . . . . 8
324	257, 323	eqbrtrri 4308	. . . . . . 7
325	243, 11, 38	redivcli 10090	. . . . . . . 8
326	173, 11, 38	redivcli 10090	. . . . . . . 8
327	320, 176	resubcli 9663	. . . . . . . 8
328	325, 326, 327	lttri 9492	. . . . . . 7 $/\$
329	245, 324, 328	mp2an 672	. . . . . 6
330	325, 176, 320	ltaddsubi 9893	. . . . . 6
331	329, 330	mpbir 209	. . . . 5
332	205, 331	eqbrtri 4306	. . . 4
333		1lt2 10480	. . . . . . 7
334		rplogcl 22028	. . . . . . 7 $/\$
335	53, 333, 334	mp2an 672	. . . . . 6
336		rpgt0 10994	. . . . . 6
337	335, 336	ax-mp 5	. . . . 5
338	180, 320, 36, 337	ltmul1ii 10253	. . . 4
339	332, 338	mpbi 208	. . 3
340	37	mulid2i 9381	. . . 4
341	340	eqcomi 2442	. . 3
342	339, 166, 341	3brtr4i 4315	. 2 ;
343	182, 342	pm3.2i 455	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wne 2601 class class class wbr 4287

cmpt 4345

cfv 5413 (class class class)co 6086

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

clt 9410

cle 9411

cmin 9587

cdiv 9985

cn 10314

c2 10363

c3 10364

c4 10365

c5 10366

c6 10367

c7 10368

c8 10369

c9 10370

c10 10371

cn0 10571

cz 10638 ;cdc 10747

crp 10983

cexp 11857

csqr 12714

clog 21981

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-fac 12044 df-bc 12071 df-hash 12096 df-shft 12548 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-sum 13156 df-ef 13345 df-sin 13347 df-cos 13348 df-pi 13350 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-submnd 15457 df-mulg 15539 df-cntz 15826 df-cmn 16270 df-psmet 17784 df-xmet 17785 df-met 17786 df-bl 17787 df-mopn 17788 df-fbas 17789 df-fg 17790 df-cnfld 17794 df-top 18478 df-bases 18480 df-topon 18481 df-topsp 18482 df-cld 18598 df-ntr 18599 df-cls 18600 df-nei 18677 df-lp 18715 df-perf 18716 df-cn 18806 df-cnp 18807 df-haus 18894 df-tx 19110 df-hmeo 19303 df-fil 19394 df-fm 19486 df-flim 19487 df-flf 19488 df-xms 19870 df-ms 19871 df-tms 19872 df-cncf 20429 df-limc 21316 df-dv 21317 df-log 21983

This theorem is referenced by: bposlem9 22606

W3C validator