bposlem8 - Metamath Proof Explorer

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

Theorem bposlem8 22515

Description: Lemma for bpos 22517. 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 10588	. . . . 5
2		4nn 10469	. . . . 5
3	1, 2	decnncl 10756	. . . 4 ;
4		fveq2 5679	. . . . . . . . . . . . . 14 ; ;
5		8cn 10395	. . . . . . . . . . . . . . . . . 18
6	5	sqvali 11929	. . . . . . . . . . . . . . . . 17
7		8t8e64 10837	. . . . . . . . . . . . . . . . 17 ;
8	6, 7	eqtri 2453	. . . . . . . . . . . . . . . 16 ;
9	8	fveq2i 5682	. . . . . . . . . . . . . . 15 ;
10		0re 9374	. . . . . . . . . . . . . . . . 17
11		8re 10394	. . . . . . . . . . . . . . . . 17
12		8pos 10410	. . . . . . . . . . . . . . . . 17
13	10, 11, 12	ltleii 9485	. . . . . . . . . . . . . . . 16
14	11	sqrsqi 12846	. . . . . . . . . . . . . . . 16
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15
16	9, 15	eqtr3i 2455	. . . . . . . . . . . . . 14 ;
17	4, 16	syl6eq 2481	. . . . . . . . . . . . 13 ;
18	17	fveq2d 5683	. . . . . . . . . . . 12 ;
19		8nn 10473	. . . . . . . . . . . . 13
20		nnrp 10988	. . . . . . . . . . . . 13
21		fveq2 5679	. . . . . . . . . . . . . . . . 17
22		cu2 11948	. . . . . . . . . . . . . . . . . . 19
23	22	fveq2i 5682	. . . . . . . . . . . . . . . . . 18
24		2rp 10984	. . . . . . . . . . . . . . . . . . 19
25		3z 10667	. . . . . . . . . . . . . . . . . . 19
26		relogexp 21929	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	mp2an 665	. . . . . . . . . . . . . . . . . 18
28	23, 27	eqtr3i 2455	. . . . . . . . . . . . . . . . 17
29	21, 28	syl6eq 2481	. . . . . . . . . . . . . . . 16
30		id 22	. . . . . . . . . . . . . . . 16
31	29, 30	oveq12d 6098	. . . . . . . . . . . . . . 15
32		3cn 10384	. . . . . . . . . . . . . . . 16
33		2nn 10467	. . . . . . . . . . . . . . . . . 18
34		nnrp 10988	. . . . . . . . . . . . . . . . . 18
35		relogcl 21912	. . . . . . . . . . . . . . . . . 18
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17
37	36	recni 9386	. . . . . . . . . . . . . . . 16
38	19	nnne0i 10344	. . . . . . . . . . . . . . . 16
39	32, 37, 5, 38	div23i 10077	. . . . . . . . . . . . . . 15
40	31, 39	syl6eq 2481	. . . . . . . . . . . . . 14
41		bposlem7.2	. . . . . . . . . . . . . 14
42		ovex 6105	. . . . . . . . . . . . . 14
43	40, 41, 42	fvmpt 5762	. . . . . . . . . . . . 13
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12
45	18, 44	syl6eq 2481	. . . . . . . . . . 11 ;
46	45	oveq2d 6096	. . . . . . . . . 10 ;
47		sqr2re 13515	. . . . . . . . . . . . 13
48	47	recni 9386	. . . . . . . . . . . 12
49	32, 5, 38	divcli 10061	. . . . . . . . . . . 12
50	48, 49, 37	mulassi 9383	. . . . . . . . . . 11
51		4cn 10387	. . . . . . . . . . . . . . . 16
52	48, 51, 48	mul12i 9552	. . . . . . . . . . . . . . 15
53		2re 10379	. . . . . . . . . . . . . . . . 17
54		0le2 10400	. . . . . . . . . . . . . . . . 17
55		remsqsqr 12730	. . . . . . . . . . . . . . . . 17 $/\$
56	53, 54, 55	mp2an 665	. . . . . . . . . . . . . . . 16
57	56	oveq2i 6091	. . . . . . . . . . . . . . 15
58		4t2e8 10463	. . . . . . . . . . . . . . 15
59	52, 57, 58	3eqtri 2457	. . . . . . . . . . . . . 14
60	59	oveq2i 6091	. . . . . . . . . . . . 13
61	51, 48	mulcli 9379	. . . . . . . . . . . . . . 15
62		nnrp 10988	. . . . . . . . . . . . . . . . . 18
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17
64		rpsqrcl 12738	. . . . . . . . . . . . . . . . . 18
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17
66		rpmulcl 11000	. . . . . . . . . . . . . . . . 17 $/\$
67	63, 65, 66	mp2an 665	. . . . . . . . . . . . . . . 16
68		rpne0 10994	. . . . . . . . . . . . . . . 16
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15
70		rpne0 10994	. . . . . . . . . . . . . . . 16
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15
72		divcan5 10021	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
73	32, 72	mp3an1 1294	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	61, 69, 48, 71, 73	mp4an 666	. . . . . . . . . . . . . 14
75		4ne0 10406	. . . . . . . . . . . . . . 15
76		divdiv1 10030	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
77	32, 76	mp3an1 1294	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78	51, 75, 48, 71, 77	mp4an 666	. . . . . . . . . . . . . 14
79	74, 78	eqtr4i 2456	. . . . . . . . . . . . 13
80	48, 32, 5, 38	divassi 10075	. . . . . . . . . . . . 13
81	60, 79, 80	3eqtr3ri 2462	. . . . . . . . . . . 12
82	81	oveq1i 6090	. . . . . . . . . . 11
83	50, 82	eqtr3i 2455	. . . . . . . . . 10
84	46, 83	syl6eq 2481	. . . . . . . . 9 ;
85		oveq1 6087	. . . . . . . . . . . . . 14 ; ;
86		df-6 10372	. . . . . . . . . . . . . . . . . 18
87	86	oveq2i 6091	. . . . . . . . . . . . . . . . 17
88		2exp6 14098	. . . . . . . . . . . . . . . . 17 ;
89		2cn 10380	. . . . . . . . . . . . . . . . . 18
90		5nn0 10587	. . . . . . . . . . . . . . . . . 18
91		expp1 11856	. . . . . . . . . . . . . . . . . 18 $/\$
92	89, 90, 91	mp2an 665	. . . . . . . . . . . . . . . . 17
93	87, 88, 92	3eqtr3i 2461	. . . . . . . . . . . . . . . 16 ;
94	93	oveq1i 6090	. . . . . . . . . . . . . . 15 ;
95		nnexpcl 11862	. . . . . . . . . . . . . . . . . 18 $/\$
96	33, 90, 95	mp2an 665	. . . . . . . . . . . . . . . . 17
97	96	nncni 10320	. . . . . . . . . . . . . . . 16
98		2ne0 10402	. . . . . . . . . . . . . . . 16
99	97, 89, 98	divcan4i 10066	. . . . . . . . . . . . . . 15
100	94, 99	eqtri 2453	. . . . . . . . . . . . . 14 ;
101	85, 100	syl6eq 2481	. . . . . . . . . . . . 13 ;
102	101	fveq2d 5683	. . . . . . . . . . . 12 ;
103		nnrp 10988	. . . . . . . . . . . . 13
104		fveq2 5679	. . . . . . . . . . . . . . . . 17
105		5nn 10470	. . . . . . . . . . . . . . . . . . 19
106	105	nnzi 10658	. . . . . . . . . . . . . . . . . 18
107		relogexp 21929	. . . . . . . . . . . . . . . . . 18 $/\$
108	24, 106, 107	mp2an 665	. . . . . . . . . . . . . . . . 17
109	104, 108	syl6eq 2481	. . . . . . . . . . . . . . . 16
110		id 22	. . . . . . . . . . . . . . . 16
111	109, 110	oveq12d 6098	. . . . . . . . . . . . . . 15
112		5cn 10389	. . . . . . . . . . . . . . . 16
113	96	nnne0i 10344	. . . . . . . . . . . . . . . 16
114	112, 37, 97, 113	div23i 10077	. . . . . . . . . . . . . . 15
115	111, 114	syl6eq 2481	. . . . . . . . . . . . . 14
116		ovex 6105	. . . . . . . . . . . . . 14
117	115, 41, 116	fvmpt 5762	. . . . . . . . . . . . 13
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12
119	102, 118	syl6eq 2481	. . . . . . . . . . 11 ;
120	119	oveq2d 6096	. . . . . . . . . 10 ;
121		9cn 10397	. . . . . . . . . . . 12
122	121, 51, 75	divcli 10061	. . . . . . . . . . 11
123	112, 97, 113	divcli 10061	. . . . . . . . . . 11
124	122, 123, 37	mulassi 9383	. . . . . . . . . 10
125	120, 124	syl6eqr 2483	. . . . . . . . 9 ;
126	84, 125	oveq12d 6098	. . . . . . . 8 ;
127	32, 51, 75	divcli 10061	. . . . . . . . . 10
128	127, 48, 71	divcli 10061	. . . . . . . . 9
129	122, 123	mulcli 9379	. . . . . . . . 9
130	128, 129, 37	adddiri 9385	. . . . . . . 8
131	126, 130	syl6eqr 2483	. . . . . . 7 ;
132		oveq2 6088	. . . . . . . . . . 11 ; ;
133	132	fveq2d 5683	. . . . . . . . . 10 ; ;
134	3	nnrei 10319	. . . . . . . . . . . 12 ;
135	3	nngt0i 10343	. . . . . . . . . . . . 13 ;
136	10, 134, 135	ltleii 9485	. . . . . . . . . . . 12 ;
137	53, 134, 54, 136	sqrmulii 12858	. . . . . . . . . . 11 ; ;
138	16	oveq2i 6091	. . . . . . . . . . 11 ;
139	137, 138	eqtri 2453	. . . . . . . . . 10 ;
140	133, 139	syl6eq 2481	. . . . . . . . 9 ;
141	140	oveq2d 6096	. . . . . . . 8 ;
142	48, 5	mulcli 9379	. . . . . . . . . 10
143		rpmulcl 11000	. . . . . . . . . . . 12 $/\$
144	65, 20, 143	sylancr 656	. . . . . . . . . . 11
145		rpne0 10994	. . . . . . . . . . 11
146	19, 144, 145	mp2b 10	. . . . . . . . . 10
147		divrec2 9999	. . . . . . . . . 10 $/\$ $/\$
148	37, 142, 146, 147	mp3an 1307	. . . . . . . . 9
149	48, 5	mulcomi 9380	. . . . . . . . . . . 12
150	149	oveq2i 6091	. . . . . . . . . . 11
151		recdiv2 10032	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	5, 38, 48, 71, 151	mp4an 666	. . . . . . . . . . 11
153	150, 152	eqtr4i 2456	. . . . . . . . . 10
154	153	oveq1i 6090	. . . . . . . . 9
155	148, 154	eqtri 2453	. . . . . . . 8
156	141, 155	syl6eq 2481	. . . . . . 7 ;
157	131, 156	oveq12d 6098	. . . . . 6 ;
158	128, 129	addcli 9378	. . . . . . 7
159	5, 38	reccli 10049	. . . . . . . 8
160	159, 48, 71	divcli 10061	. . . . . . 7
161	158, 160, 37	adddiri 9385	. . . . . 6
162	157, 161	syl6eqr 2483	. . . . 5 ;
163		bposlem7.1	. . . . 5
164		ovex 6105	. . . . 5
165	162, 163, 164	fvmpt 5762	. . . 4 ; ;
166	3, 165	ax-mp 5	. . 3 ;
167		3re 10383	. . . . . . . 8
168		4re 10386	. . . . . . . 8
169	167, 168, 75	redivcli 10086	. . . . . . 7
170	169, 47, 71	redivcli 10086	. . . . . 6
171		9re 10396	. . . . . . . 8
172	171, 168, 75	redivcli 10086	. . . . . . 7
173		5re 10388	. . . . . . . 8
174	96	nnrei 10319	. . . . . . . 8
175	173, 174, 113	redivcli 10086	. . . . . . 7
176	172, 175	remulcli 9388	. . . . . 6
177	170, 176	readdcli 9387	. . . . 5
178	11, 38	rereccli 10084	. . . . . 6
179	178, 47, 71	redivcli 10086	. . . . 5
180	177, 179	readdcli 9387	. . . 4
181	180, 36	remulcli 9388	. . 3
182	166, 181	eqeltri 2503	. 2 ;
183	128, 129, 160	add32i 9576	. . . . . 6
184		6cn 10391	. . . . . . . . . . 11
185		ax-1cn 9328	. . . . . . . . . . 11
186	184, 185, 5, 38	divdiri 10076	. . . . . . . . . 10
187		df-7 10373	. . . . . . . . . . 11
188	187	oveq1i 6090	. . . . . . . . . 10
189		divcan5 10021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
190	32, 189	mp3an1 1294	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191	51, 75, 89, 98, 190	mp4an 666	. . . . . . . . . . . 12
192		3t2e6 10461	. . . . . . . . . . . . . 14
193	32, 89, 192	mulcomli 9381	. . . . . . . . . . . . 13
194	51, 89, 58	mulcomli 9381	. . . . . . . . . . . . 13
195	193, 194	oveq12i 6092	. . . . . . . . . . . 12
196	191, 195	eqtr3i 2455	. . . . . . . . . . 11
197	196	oveq1i 6090	. . . . . . . . . 10
198	186, 188, 197	3eqtr4ri 2464	. . . . . . . . 9
199	198	oveq1i 6090	. . . . . . . 8
200	127, 159, 48, 71	divdiri 10076	. . . . . . . 8
201		7cn 10393	. . . . . . . . 9
202	201, 5, 48, 38, 71	divdiv32i 10074	. . . . . . . 8
203	199, 200, 202	3eqtr3i 2461	. . . . . . 7
204	203	oveq1i 6090	. . . . . 6
205	183, 204	eqtri 2453	. . . . 5
206		4nn0 10586	. . . . . . . . . . . 12
207		9nn0 10591	. . . . . . . . . . . 12
208		0nn0 10582	. . . . . . . . . . . 12
209		9lt10 10512	. . . . . . . . . . . 12
210		4lt5 10482	. . . . . . . . . . . 12
211	206, 90, 207, 208, 209, 210	decltc 10765	. . . . . . . . . . 11 ; ;
212		7t7e49 10830	. . . . . . . . . . 11 ;
213	56	oveq1i 6090	. . . . . . . . . . . 12
214	48, 48, 112, 112	mul4i 9554	. . . . . . . . . . . 12
215		5t2e10 10464	. . . . . . . . . . . . . . 15
216	112, 89, 215	mulcomli 9381	. . . . . . . . . . . . . 14
217	216	oveq1i 6090	. . . . . . . . . . . . 13
218	89, 112, 112	mulassi 9383	. . . . . . . . . . . . 13
219	90	dec0u 10758	. . . . . . . . . . . . 13 ;
220	217, 218, 219	3eqtr3i 2461	. . . . . . . . . . . 12 ;
221	213, 214, 220	3eqtr3i 2461	. . . . . . . . . . 11 ;
222	211, 212, 221	3brtr4i 4308	. . . . . . . . . 10
223		7re 10392	. . . . . . . . . . . 12
224		7pos 10409	. . . . . . . . . . . 12
225	10, 223, 224	ltleii 9485	. . . . . . . . . . 11
226		nnrp 10988	. . . . . . . . . . . . . 14
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13
228		rpmulcl 11000	. . . . . . . . . . . . 13 $/\$
229	65, 227, 228	mp2an 665	. . . . . . . . . . . 12
230		rpge0 10991	. . . . . . . . . . . 12
231	229, 230	ax-mp 5	. . . . . . . . . . 11
232		rpre 10985	. . . . . . . . . . . . 13
233	229, 232	ax-mp 5	. . . . . . . . . . . 12
234	223, 233	lt2msqi 10233	. . . . . . . . . . 11 $/\$
235	225, 231, 234	mp2an 665	. . . . . . . . . 10
236	222, 235	mpbir 209	. . . . . . . . 9
237		rpgt0 10990	. . . . . . . . . . 11
238	24, 64, 237	mp2b 10	. . . . . . . . . 10
239		ltdivmul 10192	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	223, 173, 239	mp3an12 1297	. . . . . . . . . 10 $/\$
241	47, 238, 240	mp2an 665	. . . . . . . . 9
242	236, 241	mpbir 209	. . . . . . . 8
243	223, 47, 71	redivcli 10086	. . . . . . . . 9
244	243, 173, 11, 12	ltdiv1ii 10250	. . . . . . . 8
245	242, 244	mpbi 208	. . . . . . 7
246		divsubdir 10015	. . . . . . . . . . 11 $/\$ $/\$ $/\$
247	5, 32, 246	mp3an12 1297	. . . . . . . . . 10 $/\$
248	5, 38, 247	mp2an 665	. . . . . . . . 9
249		5p3e8 10448	. . . . . . . . . . . 12
250	249	oveq1i 6090	. . . . . . . . . . 11
251		pncan 9604	. . . . . . . . . . . 12 $/\$
252	112, 32, 251	mp2an 665	. . . . . . . . . . 11
253	250, 252	eqtr3i 2455	. . . . . . . . . 10
254	253	oveq1i 6090	. . . . . . . . 9
255	5, 38	dividi 10052	. . . . . . . . . 10
256	255	oveq1i 6090	. . . . . . . . 9
257	248, 254, 256	3eqtr3ri 2462	. . . . . . . 8
258		5lt8 10499	. . . . . . . . . . . . 13
259	11, 173	remulcli 9388	. . . . . . . . . . . . . 14
260	173, 11, 259	ltadd2i 9493	. . . . . . . . . . . . 13
261	258, 260	mpbi 208	. . . . . . . . . . . 12
262		df-9 10375	. . . . . . . . . . . . . 14
263	262	oveq1i 6090	. . . . . . . . . . . . 13
264	5, 185, 112	adddiri 9385	. . . . . . . . . . . . 13
265	112	mulid2i 9377	. . . . . . . . . . . . . 14
266	265	oveq2i 6091	. . . . . . . . . . . . 13
267	263, 264, 266	3eqtri 2457	. . . . . . . . . . . 12
268	86	oveq2i 6091	. . . . . . . . . . . . 13
269	5, 112, 185	adddii 9384	. . . . . . . . . . . . 13
270	5	mulid1i 9376	. . . . . . . . . . . . . 14
271	270	oveq2i 6091	. . . . . . . . . . . . 13
272	268, 269, 271	3eqtri 2457	. . . . . . . . . . . 12
273	261, 267, 272	3brtr4i 4308	. . . . . . . . . . 11
274	171, 173	remulcli 9388	. . . . . . . . . . . 12
275		6re 10390	. . . . . . . . . . . . 13
276	11, 275	remulcli 9388	. . . . . . . . . . . 12
277	168, 174	remulcli 9388	. . . . . . . . . . . 12
278	2, 96	nnmulcli 10334	. . . . . . . . . . . . 13
279	278	nngt0i 10343	. . . . . . . . . . . 12
280	274, 276, 277, 279	ltdiv1ii 10250	. . . . . . . . . . 11
281	273, 280	mpbi 208	. . . . . . . . . 10
282	121, 51, 112, 97, 75, 113	divmuldivi 10079	. . . . . . . . . 10
283		nnexpcl 11862	. . . . . . . . . . . . . 14 $/\$
284	33, 206, 283	mp2an 665	. . . . . . . . . . . . 13
285	284	nncni 10320	. . . . . . . . . . . 12
286	284	nnne0i 10344	. . . . . . . . . . . 12
287		divcan5 10021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
288	32, 287	mp3an1 1294	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
289	5, 38, 285, 286, 288	mp4an 666	. . . . . . . . . . 11
290		df-4 10370	. . . . . . . . . . . . . . . 16
291	290	oveq2i 6091	. . . . . . . . . . . . . . 15
292		3nn0 10585	. . . . . . . . . . . . . . . 16
293		expp1 11856	. . . . . . . . . . . . . . . 16 $/\$
294	89, 292, 293	mp2an 665	. . . . . . . . . . . . . . 15
295	22	oveq1i 6090	. . . . . . . . . . . . . . 15
296	291, 294, 295	3eqtri 2457	. . . . . . . . . . . . . 14
297	296	oveq1i 6090	. . . . . . . . . . . . 13
298	5, 89, 32	mulassi 9383	. . . . . . . . . . . . 13
299	193	oveq2i 6091	. . . . . . . . . . . . 13
300	297, 298, 299	3eqtri 2457	. . . . . . . . . . . 12
301		4p3e7 10445	. . . . . . . . . . . . . . . 16
302		5p2e7 10447	. . . . . . . . . . . . . . . 16
303	112, 89	addcomi 9548	. . . . . . . . . . . . . . . 16
304	301, 302, 303	3eqtr2i 2459	. . . . . . . . . . . . . . 15
305	304	oveq2i 6091	. . . . . . . . . . . . . 14
306		expadd 11890	. . . . . . . . . . . . . . 15 $/\$ $/\$
307	89, 206, 292, 306	mp3an 1307	. . . . . . . . . . . . . 14
308		2nn0 10584	. . . . . . . . . . . . . . 15
309		expadd 11890	. . . . . . . . . . . . . . 15 $/\$ $/\$
310	89, 308, 90, 309	mp3an 1307	. . . . . . . . . . . . . 14
311	305, 307, 310	3eqtr3i 2461	. . . . . . . . . . . . 13
312	22	oveq2i 6091	. . . . . . . . . . . . 13
313		sq2 11946	. . . . . . . . . . . . . 14
314	313	oveq1i 6090	. . . . . . . . . . . . 13
315	311, 312, 314	3eqtr3i 2461	. . . . . . . . . . . 12
316	300, 315	oveq12i 6092	. . . . . . . . . . 11
317	289, 316	eqtr3i 2455	. . . . . . . . . 10
318	281, 282, 317	3brtr4i 4308	. . . . . . . . 9
319	167, 11, 38	redivcli 10086	. . . . . . . . . 10
320		1re 9373	. . . . . . . . . 10
321		ltsub2 9824	. . . . . . . . . 10 $/\$ $/\$
322	176, 319, 320, 321	mp3an 1307	. . . . . . . . 9
323	318, 322	mpbi 208	. . . . . . . 8
324	257, 323	eqbrtrri 4301	. . . . . . 7
325	243, 11, 38	redivcli 10086	. . . . . . . 8
326	173, 11, 38	redivcli 10086	. . . . . . . 8
327	320, 176	resubcli 9659	. . . . . . . 8
328	325, 326, 327	lttri 9488	. . . . . . 7 $/\$
329	245, 324, 328	mp2an 665	. . . . . 6
330	325, 176, 320	ltaddsubi 9889	. . . . . 6
331	329, 330	mpbir 209	. . . . 5
332	205, 331	eqbrtri 4299	. . . 4
333		1lt2 10476	. . . . . . 7
334		rplogcl 21938	. . . . . . 7 $/\$
335	53, 333, 334	mp2an 665	. . . . . 6
336		rpgt0 10990	. . . . . 6
337	335, 336	ax-mp 5	. . . . 5
338	180, 320, 36, 337	ltmul1ii 10249	. . . 4
339	332, 338	mpbi 208	. . 3
340	37	mulid2i 9377	. . . 4
341	340	eqcomi 2437	. . 3
342	339, 166, 341	3brtr4i 4308	. 2 ;
343	182, 342	pm3.2i 452	1 ; $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wb 184 $/\$ wa 369

wceq 1362

wcel 1755

wne 2596 class class class wbr 4280

cmpt 4338

cfv 5406 (class class class)co 6080

cc 9268

cr 9269

cc0 9270

c1 9271

caddc 9273

cmul 9275

clt 9406

cle 9407

cmin 9583

cdiv 9981

cn 10310

c2 10359

c3 10360

c4 10361

c5 10362

c6 10363

c7 10364

c8 10365

c9 10366

c10 10367

cn0 10567

cz 10634 ;cdc 10743

crp 10979

cexp 11849

csqr 12706

clog 21891

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-map 7204 df-pm 7205 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-5 10371 df-6 10372 df-7 10373 df-8 10374 df-9 10375 df-10 10376 df-n0 10568 df-z 10635 df-dec 10744 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-ioc 11293 df-ico 11294 df-icc 11295 df-fz 11425 df-fzo 11533 df-fl 11626 df-mod 11693 df-seq 11791 df-exp 11850 df-fac 12036 df-bc 12063 df-hash 12088 df-shft 12540 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-limsup 12933 df-clim 12950 df-rlim 12951 df-sum 13148 df-ef 13336 df-sin 13338 df-cos 13339 df-pi 13341 df-struct 14159 df-ndx 14160 df-slot 14161 df-base 14162 df-sets 14163 df-ress 14164 df-plusg 14234 df-mulr 14235 df-starv 14236 df-sca 14237 df-vsca 14238 df-ip 14239 df-tset 14240 df-ple 14241 df-ds 14243 df-unif 14244 df-hom 14245 df-cco 14246 df-rest 14344 df-topn 14345 df-0g 14363 df-gsum 14364 df-topgen 14365 df-pt 14366 df-prds 14369 df-xrs 14423 df-qtop 14428 df-imas 14429 df-xps 14431 df-mre 14507 df-mrc 14508 df-acs 14510 df-mnd 15398 df-submnd 15448 df-mulg 15528 df-cntz 15815 df-cmn 16259 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-fbas 17658 df-fg 17659 df-cnfld 17663 df-top 18345 df-bases 18347 df-topon 18348 df-topsp 18349 df-cld 18465 df-ntr 18466 df-cls 18467 df-nei 18544 df-lp 18582 df-perf 18583 df-cn 18673 df-cnp 18674 df-haus 18761 df-tx 18977 df-hmeo 19170 df-fil 19261 df-fm 19353 df-flim 19354 df-flf 19355 df-xms 19737 df-ms 19738 df-tms 19739 df-cncf 20296 df-limc 21183 df-dv 21184 df-log 21893

This theorem is referenced by: bposlem9 22516

W3C validator