bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 22762

Description: Lemma for bpos 22764. 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 10710	. . . . 5
2		4nn 10591	. . . . 5
3	1, 2	decnncl 10878	. . . 4 ;
4		fveq2 5798	. . . . . . . . . . . . . 14 ; ;
5		8cn 10517	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 12061	. . . . . . . . . . . . . . . . 17
7		8t8e64 10959	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2483	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5801	. . . . . . . . . . . . . . 15 ;
10		0re 9496	. . . . . . . . . . . . . . . . 17
11		8re 10516	. . . . . . . . . . . . . . . . 17
12		8pos 10532	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9607	. . . . . . . . . . . . . . . 16
14	11	sqrsqi 12979	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2485	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2511	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5802	. . . . . . . . . . . 12 ;
19		8nn 10595	. . . . . . . . . . . . 13
20		nnrp 11110	. . . . . . . . . . . . 13
21		fveq2 5798	. . . . . . . . . . . . . . . . 17
22		cu2 12080	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5801	. . . . . . . . . . . . . . . . . 18
24		2rp 11106	. . . . . . . . . . . . . . . . . . 19
25		3z 10789	. . . . . . . . . . . . . . . . . . 19
26		relogexp 22176	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2485	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2511	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6217	. . . . . . . . . . . . . . 15
32		3cn 10506	. . . . . . . . . . . . . . . 16
33		2nn 10589	. . . . . . . . . . . . . . . . . 18
34		nnrp 11110	. . . . . . . . . . . . . . . . . 18
35		relogcl 22159	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9508	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10466	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10199	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2511	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6224	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5882	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2511	. . . . . . . . . . 11 ;
46	45	oveq2d 6215	. . . . . . . . . 10 ;
47		sqr2re 13649	. . . . . . . . . . . . 13
48	47	recni 9508	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10183	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9505	. . . . . . . . . . 11
51		4cn 10509	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9674	. . . . . . . . . . . . . . 15
53		2re 10501	. . . . . . . . . . . . . . . . 17
54		0le2 10522	. . . . . . . . . . . . . . . . 17
55		remsqsqr 12863	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 672	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6210	. . . . . . . . . . . . . . 15
58		4t2e8 10585	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2487	. . . . . . . . . . . . . 14
60	59	oveq2i 6210	. . . . . . . . . . . . 13
61	51, 48	mulcli 9501	. . . . . . . . . . . . . . 15
62		nnrp 11110	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrcl 12871	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11122	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 672	. . . . . . . . . . . . . . . 16
68		rpne0 11116	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 11116	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10143	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1302	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 673	. . . . . . . . . . . . . 14
75		4ne0 10528	. . . . . . . . . . . . . . 15
76		divdiv1 10152	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1302	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 673	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2486	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10197	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2492	. . . . . . . . . . . 12
82	81	oveq1i 6209	. . . . . . . . . . 11
83	50, 82	eqtr3i 2485	. . . . . . . . . 10
84	46, 83	syl6eq 2511	. . . . . . . . 9 ;
85		oveq1 6206	. . . . . . . . . . . . . 14 ; ;
86		df-6 10494	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6210	. . . . . . . . . . . . . . . . 17
88		2exp6 14232	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10502	. . . . . . . . . . . . . . . . . 18
90		5nn0 10709	. . . . . . . . . . . . . . . . . 18
91		expp1 11988	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 672	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2491	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6209	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 11994	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 672	. . . . . . . . . . . . . . . . 17
97	96	nncni 10442	. . . . . . . . . . . . . . . 16
98		2ne0 10524	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10188	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2483	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2511	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5802	. . . . . . . . . . . 12 ;
103		nnrp 11110	. . . . . . . . . . . . 13
104		fveq2 5798	. . . . . . . . . . . . . . . . 17
105		5nn 10592	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10780	. . . . . . . . . . . . . . . . . 18
107		relogexp 22176	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 672	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2511	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6217	. . . . . . . . . . . . . . 15
112		5cn 10511	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10466	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10199	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2511	. . . . . . . . . . . . . 14
116		ovex 6224	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5882	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2511	. . . . . . . . . . 11 ;
120	119	oveq2d 6215	. . . . . . . . . 10 ;
121		9cn 10519	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10183	. . . . . . . . . . 11
123	112, 97, 113	divcli 10183	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9505	. . . . . . . . . 10
125	120, 124	syl6eqr 2513	. . . . . . . . 9 ;
126	84, 125	oveq12d 6217	. . . . . . . 8 ;
127	32, 51, 75	divcli 10183	. . . . . . . . . 10
128	127, 48, 71	divcli 10183	. . . . . . . . 9
129	122, 123	mulcli 9501	. . . . . . . . 9
130	128, 129, 37	adddiri 9507	. . . . . . . 8
131	126, 130	syl6eqr 2513	. . . . . . 7 ;
132		oveq2 6207	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5802	. . . . . . . . . 10 ; ;
134	3	nnrei 10441	. . . . . . . . . . . 12 ;
135	3	nngt0i 10465	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9607	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrmulii 12991	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6210	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2483	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2511	. . . . . . . . 9 ;
141	140	oveq2d 6215	. . . . . . . 8 ;
142	48, 5	mulcli 9501	. . . . . . . . . 10
143		rpmulcl 11122	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 663	. . . . . . . . . . 11
145		rpne0 11116	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 10121	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1315	. . . . . . . . 9
149	48, 5	mulcomi 9502	. . . . . . . . . . . 12
150	149	oveq2i 6210	. . . . . . . . . . 11
151		recdiv2 10154	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 673	. . . . . . . . . . 11
153	150, 152	eqtr4i 2486	. . . . . . . . . 10
154	153	oveq1i 6209	. . . . . . . . 9
155	148, 154	eqtri 2483	. . . . . . . 8
156	141, 155	syl6eq 2511	. . . . . . 7 ;
157	131, 156	oveq12d 6217	. . . . . 6 ;
158	128, 129	addcli 9500	. . . . . . 7
159	5, 38	reccli 10171	. . . . . . . 8
160	159, 48, 71	divcli 10183	. . . . . . 7
161	158, 160, 37	adddiri 9507	. . . . . 6
162	157, 161	syl6eqr 2513	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6224	. . . . 5
165	162, 163, 164	fvmpt 5882	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10505	. . . . . . . 8
168		4re 10508	. . . . . . . 8
169	167, 168, 75	redivcli 10208	. . . . . . 7
170	169, 47, 71	redivcli 10208	. . . . . 6
171		9re 10518	. . . . . . . 8
172	171, 168, 75	redivcli 10208	. . . . . . 7
173		5re 10510	. . . . . . . 8
174	96	nnrei 10441	. . . . . . . 8
175	173, 174, 113	redivcli 10208	. . . . . . 7
176	172, 175	remulcli 9510	. . . . . 6
177	170, 176	readdcli 9509	. . . . 5
178	11, 38	rereccli 10206	. . . . . 6
179	178, 47, 71	redivcli 10208	. . . . 5
180	177, 179	readdcli 9509	. . . 4
181	180, 36	remulcli 9510	. . 3
182	166, 181	eqeltri 2538	. 2 ;
183	128, 129, 160	add32i 9698	. . . . . 6
184		6cn 10513	. . . . . . . . . . 11
185		ax-1cn 9450	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10198	. . . . . . . . . 10
187		df-7 10495	. . . . . . . . . . 11
188	187	oveq1i 6209	. . . . . . . . . 10
189		divcan5 10143	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1302	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 673	. . . . . . . . . . . 12
192		3t2e6 10583	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9503	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9503	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6211	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2485	. . . . . . . . . . 11
197	196	oveq1i 6209	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2494	. . . . . . . . 9
199	198	oveq1i 6209	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10198	. . . . . . . 8
201		7cn 10515	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10196	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2491	. . . . . . 7
204	203	oveq1i 6209	. . . . . 6
205	183, 204	eqtri 2483	. . . . 5
206		4nn0 10708	. . . . . . . . . . . 12
207		9nn0 10713	. . . . . . . . . . . 12
208		0nn0 10704	. . . . . . . . . . . 12
209		9lt10 10634	. . . . . . . . . . . 12
210		4lt5 10604	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 10887	. . . . . . . . . . 11 ; ;
212		7t7e49 10952	. . . . . . . . . . 11 ;
213	56	oveq1i 6209	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9676	. . . . . . . . . . . 12
215		5t2e10 10586	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9503	. . . . . . . . . . . . . 14
217	216	oveq1i 6209	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9505	. . . . . . . . . . . . 13
219	90	dec0u 10880	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2491	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2491	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4427	. . . . . . . . . 10
223		7re 10514	. . . . . . . . . . . 12
224		7pos 10531	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9607	. . . . . . . . . . 11
226		nnrp 11110	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11122	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 672	. . . . . . . . . . . 12
230		rpge0 11113	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 11107	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10355	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 672	. . . . . . . . . 10
236	222, 235	mpbir 209	. . . . . . . . 9
237		rpgt0 11112	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10314	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1305	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 672	. . . . . . . . 9
242	236, 241	mpbir 209	. . . . . . . 8
243	223, 47, 71	redivcli 10208	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10372	. . . . . . . 8
245	242, 244	mpbi 208	. . . . . . 7
246		divsubdir 10137	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1305	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 672	. . . . . . . . 9
249		5p3e8 10570	. . . . . . . . . . . 12
250	249	oveq1i 6209	. . . . . . . . . . 11
251		pncan 9726	. . . . . . . . . . . 12 $/\$
252	112, 32, 251	mp2an 672	. . . . . . . . . . 11
253	250, 252	eqtr3i 2485	. . . . . . . . . 10
254	253	oveq1i 6209	. . . . . . . . 9
255	5, 38	dividi 10174	. . . . . . . . . 10
256	255	oveq1i 6209	. . . . . . . . 9
257	248, 254, 256	3eqtr3ri 2492	. . . . . . . 8
258		5lt8 10621	. . . . . . . . . . . . 13
259	11, 173	remulcli 9510	. . . . . . . . . . . . . 14
260	173, 11, 259	ltadd2i 9615	. . . . . . . . . . . . 13
261	258, 260	mpbi 208	. . . . . . . . . . . 12
262		df-9 10497	. . . . . . . . . . . . . 14
263	262	oveq1i 6209	. . . . . . . . . . . . 13
264	5, 185, 112	adddiri 9507	. . . . . . . . . . . . 13
265	112	mulid2i 9499	. . . . . . . . . . . . . 14
266	265	oveq2i 6210	. . . . . . . . . . . . 13
267	263, 264, 266	3eqtri 2487	. . . . . . . . . . . 12
268	86	oveq2i 6210	. . . . . . . . . . . . 13
269	5, 112, 185	adddii 9506	. . . . . . . . . . . . 13
270	5	mulid1i 9498	. . . . . . . . . . . . . 14
271	270	oveq2i 6210	. . . . . . . . . . . . 13
272	268, 269, 271	3eqtri 2487	. . . . . . . . . . . 12
273	261, 267, 272	3brtr4i 4427	. . . . . . . . . . 11
274	171, 173	remulcli 9510	. . . . . . . . . . . 12
275		6re 10512	. . . . . . . . . . . . 13
276	11, 275	remulcli 9510	. . . . . . . . . . . 12
277	168, 174	remulcli 9510	. . . . . . . . . . . 12
278	2, 96	nnmulcli 10456	. . . . . . . . . . . . 13
279	278	nngt0i 10465	. . . . . . . . . . . 12
280	274, 276, 277, 279	ltdiv1ii 10372	. . . . . . . . . . 11
281	273, 280	mpbi 208	. . . . . . . . . 10
282	121, 51, 112, 97, 75, 113	divmuldivi 10201	. . . . . . . . . 10
283		nnexpcl 11994	. . . . . . . . . . . . . 14 $/\$
284	33, 206, 283	mp2an 672	. . . . . . . . . . . . 13
285	284	nncni 10442	. . . . . . . . . . . 12
286	284	nnne0i 10466	. . . . . . . . . . . 12
287		divcan5 10143	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
288	32, 287	mp3an1 1302	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
289	5, 38, 285, 286, 288	mp4an 673	. . . . . . . . . . 11
290		df-4 10492	. . . . . . . . . . . . . . . 16
291	290	oveq2i 6210	. . . . . . . . . . . . . . 15
292		3nn0 10707	. . . . . . . . . . . . . . . 16
293		expp1 11988	. . . . . . . . . . . . . . . 16 $/\$
294	89, 292, 293	mp2an 672	. . . . . . . . . . . . . . 15
295	22	oveq1i 6209	. . . . . . . . . . . . . . 15
296	291, 294, 295	3eqtri 2487	. . . . . . . . . . . . . 14
297	296	oveq1i 6209	. . . . . . . . . . . . 13
298	5, 89, 32	mulassi 9505	. . . . . . . . . . . . 13
299	193	oveq2i 6210	. . . . . . . . . . . . 13
300	297, 298, 299	3eqtri 2487	. . . . . . . . . . . 12
301		4p3e7 10567	. . . . . . . . . . . . . . . 16
302		5p2e7 10569	. . . . . . . . . . . . . . . 16
303	112, 89	addcomi 9670	. . . . . . . . . . . . . . . 16
304	301, 302, 303	3eqtr2i 2489	. . . . . . . . . . . . . . 15
305	304	oveq2i 6210	. . . . . . . . . . . . . 14
306		expadd 12022	. . . . . . . . . . . . . . 15 $/\$ $/\$
307	89, 206, 292, 306	mp3an 1315	. . . . . . . . . . . . . 14
308		2nn0 10706	. . . . . . . . . . . . . . 15
309		expadd 12022	. . . . . . . . . . . . . . 15 $/\$ $/\$
310	89, 308, 90, 309	mp3an 1315	. . . . . . . . . . . . . 14
311	305, 307, 310	3eqtr3i 2491	. . . . . . . . . . . . 13
312	22	oveq2i 6210	. . . . . . . . . . . . 13
313		sq2 12078	. . . . . . . . . . . . . 14
314	313	oveq1i 6209	. . . . . . . . . . . . 13
315	311, 312, 314	3eqtr3i 2491	. . . . . . . . . . . 12
316	300, 315	oveq12i 6211	. . . . . . . . . . 11
317	289, 316	eqtr3i 2485	. . . . . . . . . 10
318	281, 282, 317	3brtr4i 4427	. . . . . . . . 9
319	167, 11, 38	redivcli 10208	. . . . . . . . . 10
320		1re 9495	. . . . . . . . . 10
321		ltsub2 9946	. . . . . . . . . 10 $/\$ $/\$
322	176, 319, 320, 321	mp3an 1315	. . . . . . . . 9
323	318, 322	mpbi 208	. . . . . . . 8
324	257, 323	eqbrtrri 4420	. . . . . . 7
325	243, 11, 38	redivcli 10208	. . . . . . . 8
326	173, 11, 38	redivcli 10208	. . . . . . . 8
327	320, 176	resubcli 9781	. . . . . . . 8
328	325, 326, 327	lttri 9610	. . . . . . 7 $/\$
329	245, 324, 328	mp2an 672	. . . . . 6
330	325, 176, 320	ltaddsubi 10011	. . . . . 6
331	329, 330	mpbir 209	. . . . 5
332	205, 331	eqbrtri 4418	. . . 4
333		1lt2 10598	. . . . . . 7
334		rplogcl 22185	. . . . . . 7 $/\$
335	53, 333, 334	mp2an 672	. . . . . 6
336		rpgt0 11112	. . . . . 6
337	335, 336	ax-mp 5	. . . . 5
338	180, 320, 36, 337	ltmul1ii 10371	. . . 4
339	332, 338	mpbi 208	. . 3
340	37	mulid2i 9499	. . . 4
341	340	eqcomi 2467	. . 3
342	339, 166, 341	3brtr4i 4427	. 2 ;
343	182, 342	pm3.2i 455	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 184 $/\$ wa 369

wceq 1370

wcel 1758

wne 2647 class class class wbr 4399

cmpt 4457

cfv 5525 (class class class)co 6199

cc 9390

cr 9391

cc0 9392

c1 9393

caddc 9395

cmul 9397

clt 9528

cle 9529

cmin 9705

cdiv 10103

cn 10432

c2 10481

c3 10482

c4 10483

c5 10484

c6 10485

c7 10486

c8 10487

c9 10488

c10 10489

cn0 10689

cz 10756 ;cdc 10865

crp 11101

cexp 11981

csqr 12839

clog 22138

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-inf2 7957 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 ax-pre-sup 9470 ax-addf 9471 ax-mulf 9472

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-iin 4281 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-se 4787 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-of 6429 df-om 6586 df-1st 6686 df-2nd 6687 df-supp 6800 df-recs 6941 df-rdg 6975 df-1o 7029 df-2o 7030 df-oadd 7033 df-er 7210 df-map 7325 df-pm 7326 df-ixp 7373 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-fsupp 7731 df-fi 7771 df-sup 7801 df-oi 7834 df-card 8219 df-cda 8447 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-div 10104 df-nn 10433 df-2 10490 df-3 10491 df-4 10492 df-5 10493 df-6 10494 df-7 10495 df-8 10496 df-9 10497 df-10 10498 df-n0 10690 df-z 10757 df-dec 10866 df-uz 10972 df-q 11064 df-rp 11102 df-xneg 11199 df-xadd 11200 df-xmul 11201 df-ioo 11414 df-ioc 11415 df-ico 11416 df-icc 11417 df-fz 11554 df-fzo 11665 df-fl 11758 df-mod 11825 df-seq 11923 df-exp 11982 df-fac 12168 df-bc 12195 df-hash 12220 df-shft 12673 df-cj 12705 df-re 12706 df-im 12707 df-sqr 12841 df-abs 12842 df-limsup 13066 df-clim 13083 df-rlim 13084 df-sum 13281 df-ef 13470 df-sin 13472 df-cos 13473 df-pi 13475 df-struct 14293 df-ndx 14294 df-slot 14295 df-base 14296 df-sets 14297 df-ress 14298 df-plusg 14369 df-mulr 14370 df-starv 14371 df-sca 14372 df-vsca 14373 df-ip 14374 df-tset 14375 df-ple 14376 df-ds 14378 df-unif 14379 df-hom 14380 df-cco 14381 df-rest 14479 df-topn 14480 df-0g 14498 df-gsum 14499 df-topgen 14500 df-pt 14501 df-prds 14504 df-xrs 14558 df-qtop 14563 df-imas 14564 df-xps 14566 df-mre 14642 df-mrc 14643 df-acs 14645 df-mnd 15533 df-submnd 15583 df-mulg 15666 df-cntz 15953 df-cmn 16399 df-psmet 17933 df-xmet 17934 df-met 17935 df-bl 17936 df-mopn 17937 df-fbas 17938 df-fg 17939 df-cnfld 17943 df-top 18634 df-bases 18636 df-topon 18637 df-topsp 18638 df-cld 18754 df-ntr 18755 df-cls 18756 df-nei 18833 df-lp 18871 df-perf 18872 df-cn 18962 df-cnp 18963 df-haus 19050 df-tx 19266 df-hmeo 19459 df-fil 19550 df-fm 19642 df-flim 19643 df-flf 19644 df-xms 20026 df-ms 20027 df-tms 20028 df-cncf 20585 df-limc 21473 df-dv 21474 df-log 22140

This theorem is referenced by: bposlem9 22763

W3C validator