bposlem9 - Metamath Proof Explorer

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

Theorem bposlem9 25017

Description: Lemma for bpos 25018. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)

**Hypotheses**
Ref	Expression
bposlem7.1
bposlem7.2
bposlem9.3
bposlem9.4	;
bposlem9.5	$/\$

**Assertion**
Ref	Expression
bposlem9

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

Proof of Theorem bposlem9 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bposlem9.4	. . 3 ;
2		bposlem7.1	. . . 4
3		bposlem7.2	. . . 4
4		6nn0 11313	. . . . . 6
5		4nn 11187	. . . . . 6
6	4, 5	decnncl 11518	. . . . 5 ;
7	6	a1i 11	. . . 4 ;
8		bposlem9.3	. . . 4
9		ere 14819	. . . . . . . 8
10		8re 11105	. . . . . . . 8
11		egt2lt3 14934	. . . . . . . . . 10 $/\$
12	11	simpri 478	. . . . . . . . 9
13		3lt8 11219	. . . . . . . . 9
14		3re 11094	. . . . . . . . . 10
15	9, 14, 10	lttri 10163	. . . . . . . . 9 $/\$
16	12, 13, 15	mp2an 708	. . . . . . . 8
17	9, 10, 16	ltleii 10160	. . . . . . 7
18		0re 10040	. . . . . . . . 9
19		epos 14935	. . . . . . . . 9
20	18, 9, 19	ltleii 10160	. . . . . . . 8
21		8pos 11121	. . . . . . . . 9
22	18, 10, 21	ltleii 10160	. . . . . . . 8
23		le2sq 12938	. . . . . . . 8 $/\$ $/\$ $/\$
24	9, 20, 10, 22, 23	mp4an 709	. . . . . . 7
25	17, 24	mpbi 220	. . . . . 6
26	10	recni 10052	. . . . . . . 8
27	26	sqvali 12943	. . . . . . 7
28		8t8e64 11662	. . . . . . 7 ;
29	27, 28	eqtri 2644	. . . . . 6 ;
30	25, 29	breqtri 4678	. . . . 5 ;
31	30	a1i 11	. . . 4 ;
32	9	resqcli 12949	. . . . . 6
33	32	a1i 11	. . . . 5
34	6	nnrei 11029	. . . . . 6 ;
35	34	a1i 11	. . . . 5 ;
36	8	nnred 11035	. . . . 5
37		ltle 10126	. . . . . . 7 ; $/\$ ; ;
38	34, 36, 37	sylancr 695	. . . . . 6 ; ;
39	1, 38	mpd 15	. . . . 5 ;
40	33, 35, 36, 31, 39	letrd 10194	. . . 4
41	2, 3, 7, 8, 31, 40	bposlem7 25015	. . 3 ; ;
42	1, 41	mpd 15	. 2 ;
43	2, 3	bposlem8 25016	. . . . 5 ; $/\$ ;
44	43	a1i 11	. . . 4 ; $/\$ ;
45	44	simpld 475	. . 3 ;
46		fveq2 6191	. . . . . . . . . 10
47	46	fveq2d 6195	. . . . . . . . 9
48	47	oveq2d 6666	. . . . . . . 8
49		oveq1 6657	. . . . . . . . . 10
50	49	fveq2d 6195	. . . . . . . . 9
51	50	oveq2d 6666	. . . . . . . 8
52	48, 51	oveq12d 6668	. . . . . . 7
53		oveq2 6658	. . . . . . . . 9
54	53	fveq2d 6195	. . . . . . . 8
55	54	oveq2d 6666	. . . . . . 7
56	52, 55	oveq12d 6668	. . . . . 6
57		ovex 6678	. . . . . 6
58	56, 2, 57	fvmpt 6282	. . . . 5
59	8, 58	syl 17	. . . 4
60		sqrt2re 14980	. . . . . . 7
61	8	nnrpd 11870	. . . . . . . . . 10
62	61	rpsqrtcld 14150	. . . . . . . . 9
63		fveq2 6191	. . . . . . . . . . 11
64		id 22	. . . . . . . . . . 11
65	63, 64	oveq12d 6668	. . . . . . . . . 10
66		ovex 6678	. . . . . . . . . 10
67	65, 3, 66	fvmpt 6282	. . . . . . . . 9
68	62, 67	syl 17	. . . . . . . 8
69	62	relogcld 24369	. . . . . . . . 9
70	69, 62	rerpdivcld 11903	. . . . . . . 8
71	68, 70	eqeltrd 2701	. . . . . . 7
72		remulcl 10021	. . . . . . 7 $/\$
73	60, 71, 72	sylancr 695	. . . . . 6
74		9re 11107	. . . . . . . 8
75		4re 11097	. . . . . . . 8
76		4ne0 11117	. . . . . . . 8
77	74, 75, 76	redivcli 10792	. . . . . . 7
78	61	rphalfcld 11884	. . . . . . . . 9
79		fveq2 6191	. . . . . . . . . . 11
80		id 22	. . . . . . . . . . 11
81	79, 80	oveq12d 6668	. . . . . . . . . 10
82		ovex 6678	. . . . . . . . . 10
83	81, 3, 82	fvmpt 6282	. . . . . . . . 9
84	78, 83	syl 17	. . . . . . . 8
85	78	relogcld 24369	. . . . . . . . 9
86	85, 78	rerpdivcld 11903	. . . . . . . 8
87	84, 86	eqeltrd 2701	. . . . . . 7
88		remulcl 10021	. . . . . . 7 $/\$
89	77, 87, 88	sylancr 695	. . . . . 6
90	73, 89	readdcld 10069	. . . . 5
91		2rp 11837	. . . . . . 7
92		relogcl 24322	. . . . . . 7
93	91, 92	ax-mp 5	. . . . . 6
94		rpmulcl 11855	. . . . . . . 8 $/\$
95	91, 61, 94	sylancr 695	. . . . . . 7
96	95	rpsqrtcld 14150	. . . . . 6
97		rerpdivcl 11861	. . . . . 6 $/\$
98	93, 96, 97	sylancr 695	. . . . 5
99	90, 98	readdcld 10069	. . . 4
100	59, 99	eqeltrd 2701	. . 3
101	93	a1i 11	. . . 4
102	44	simprd 479	. . . 4 ;
103		nnrp 11842	. . . . . . . . . . 11
104	5, 103	ax-mp 5	. . . . . . . . . 10
105		relogcl 24322	. . . . . . . . . 10
106	104, 105	ax-mp 5	. . . . . . . . 9
107		remulcl 10021	. . . . . . . . 9 $/\$
108	36, 106, 107	sylancl 694	. . . . . . . 8
109	61	relogcld 24369	. . . . . . . 8
110	108, 109	resubcld 10458	. . . . . . 7
111		rpre 11839	. . . . . . . . . . . . 13
112		rpge0 11845	. . . . . . . . . . . . 13
113	111, 112	resqrtcld 14156	. . . . . . . . . . . 12
114	95, 113	syl 17	. . . . . . . . . . 11
115		3nn 11186	. . . . . . . . . . 11
116		nndivre 11056	. . . . . . . . . . 11 $/\$
117	114, 115, 116	sylancl 694	. . . . . . . . . 10
118		2re 11090	. . . . . . . . . 10
119		readdcl 10019	. . . . . . . . . 10 $/\$
120	117, 118, 119	sylancl 694	. . . . . . . . 9
121	95	relogcld 24369	. . . . . . . . 9
122	120, 121	remulcld 10070	. . . . . . . 8
123		remulcl 10021	. . . . . . . . . . . 12 $/\$
124	75, 36, 123	sylancr 695	. . . . . . . . . . 11
125		nndivre 11056	. . . . . . . . . . 11 $/\$
126	124, 115, 125	sylancl 694	. . . . . . . . . 10
127		5re 11099	. . . . . . . . . 10
128		resubcl 10345	. . . . . . . . . 10 $/\$
129	126, 127, 128	sylancl 694	. . . . . . . . 9
130		remulcl 10021	. . . . . . . . 9 $/\$
131	129, 93, 130	sylancl 694	. . . . . . . 8
132	122, 131	readdcld 10069	. . . . . . 7
133		remulcl 10021	. . . . . . . . 9 $/\$
134	126, 93, 133	sylancl 694	. . . . . . . 8
135	134, 109	resubcld 10458	. . . . . . 7
136	8	nnzd 11481	. . . . . . . . . . 11
137		df-5 11082	. . . . . . . . . . . 12
138	75	a1i 11	. . . . . . . . . . . . . 14
139		6nn 11189	. . . . . . . . . . . . . . . 16
140		4nn0 11311	. . . . . . . . . . . . . . . 16
141		4lt10 11678	. . . . . . . . . . . . . . . 16 ;
142	139, 140, 140, 141	declti 11546	. . . . . . . . . . . . . . 15 ;
143	142	a1i 11	. . . . . . . . . . . . . 14 ;
144	138, 35, 36, 143, 1	lttrd 10198	. . . . . . . . . . . . 13
145		4z 11411	. . . . . . . . . . . . . 14
146		zltp1le 11427	. . . . . . . . . . . . . 14 $/\$
147	145, 136, 146	sylancr 695	. . . . . . . . . . . . 13
148	144, 147	mpbid 222	. . . . . . . . . . . 12
149	137, 148	syl5eqbr 4688	. . . . . . . . . . 11
150		5nn 11188	. . . . . . . . . . . . 13
151	150	nnzi 11401	. . . . . . . . . . . 12
152	151	eluz1i 11695	. . . . . . . . . . 11 $/\$
153	136, 149, 152	sylanbrc 698	. . . . . . . . . 10
154		bposlem9.5	. . . . . . . . . . 11 $/\$
155		breq2 4657	. . . . . . . . . . . . 13
156		breq1 4656	. . . . . . . . . . . . 13
157	155, 156	anbi12d 747	. . . . . . . . . . . 12 $/\$ $/\$
158	157	cbvrexv 3172	. . . . . . . . . . 11 $/\$ $/\$
159	154, 158	sylnib 318	. . . . . . . . . 10 $/\$
160		eqid 2622	. . . . . . . . . 10
161		eqid 2622	. . . . . . . . . 10
162		eqid 2622	. . . . . . . . . 10
163	153, 159, 160, 161, 162	bposlem6 25014	. . . . . . . . 9
164		reexplog 24341	. . . . . . . . . . . 12 $/\$
165	104, 136, 164	sylancr 695	. . . . . . . . . . 11
166	61	reeflogd 24370	. . . . . . . . . . . 12
167	166	eqcomd 2628	. . . . . . . . . . 11
168	165, 167	oveq12d 6668	. . . . . . . . . 10
169	108	recnd 10068	. . . . . . . . . . 11
170	109	recnd 10068	. . . . . . . . . . 11
171		efsub 14830	. . . . . . . . . . 11 $/\$
172	169, 170, 171	syl2anc 693	. . . . . . . . . 10
173	168, 172	eqtr4d 2659	. . . . . . . . 9
174	95	rpcnd 11874	. . . . . . . . . . . 12
175	95	rpne0d 11877	. . . . . . . . . . . 12
176	120	recnd 10068	. . . . . . . . . . . 12
177	174, 175, 176	cxpefd 24458	. . . . . . . . . . 11
178		2cn 11091	. . . . . . . . . . . 12
179		2ne0 11113	. . . . . . . . . . . 12
180	129	recnd 10068	. . . . . . . . . . . 12
181		cxpef 24411	. . . . . . . . . . . 12 $/\$ $/\$
182	178, 179, 180, 181	mp3an12i 1428	. . . . . . . . . . 11
183	177, 182	oveq12d 6668	. . . . . . . . . 10
184	122	recnd 10068	. . . . . . . . . . 11
185	131	recnd 10068	. . . . . . . . . . 11
186		efadd 14824	. . . . . . . . . . 11 $/\$
187	184, 185, 186	syl2anc 693	. . . . . . . . . 10
188	183, 187	eqtr4d 2659	. . . . . . . . 9
189	163, 173, 188	3brtr3d 4684	. . . . . . . 8
190		eflt 14847	. . . . . . . . 9 $/\$
191	110, 132, 190	syl2anc 693	. . . . . . . 8
192	189, 191	mpbird 247	. . . . . . 7
193	110, 132, 135, 192	ltsub1dd 10639	. . . . . 6
194	36	recnd 10068	. . . . . . . . . . 11
195		mulcom 10022	. . . . . . . . . . 11 $/\$
196	178, 194, 195	sylancr 695	. . . . . . . . . 10
197	196	oveq1d 6665	. . . . . . . . 9
198	93	recni 10052	. . . . . . . . . . . 12
199		mulass 10024	. . . . . . . . . . . 12 $/\$ $/\$
200	178, 198, 199	mp3an23 1416	. . . . . . . . . . 11
201	194, 200	syl 17	. . . . . . . . . 10
202	198	2timesi 11147	. . . . . . . . . . . 12
203		relogmul 24338	. . . . . . . . . . . . 13 $/\$
204	91, 91, 203	mp2an 708	. . . . . . . . . . . 12
205		2t2e4 11177	. . . . . . . . . . . . 13
206	205	fveq2i 6194	. . . . . . . . . . . 12
207	202, 204, 206	3eqtr2i 2650	. . . . . . . . . . 11
208	207	oveq2i 6661	. . . . . . . . . 10
209	201, 208	syl6eq 2672	. . . . . . . . 9
210	197, 209	eqtrd 2656	. . . . . . . 8
211	210	oveq1d 6665	. . . . . . 7
212		4p2e6 11162	. . . . . . . . . . . . . . 15
213	212	oveq1i 6660	. . . . . . . . . . . . . 14
214		4cn 11098	. . . . . . . . . . . . . . 15
215		adddir 10031	. . . . . . . . . . . . . . 15 $/\$ $/\$
216	214, 178, 194, 215	mp3an12i 1428	. . . . . . . . . . . . . 14
217	213, 216	syl5eqr 2670	. . . . . . . . . . . . 13
218	217	oveq1d 6665	. . . . . . . . . . . 12
219		6cn 11102	. . . . . . . . . . . . . . 15
220		3cn 11095	. . . . . . . . . . . . . . . 16
221		3ne0 11115	. . . . . . . . . . . . . . . 16
222	220, 221	pm3.2i 471	. . . . . . . . . . . . . . 15 $/\$
223		div23 10704	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
224	219, 222, 223	mp3an13 1415	. . . . . . . . . . . . . 14
225	194, 224	syl 17	. . . . . . . . . . . . 13
226		3t2e6 11179	. . . . . . . . . . . . . . . 16
227	226	oveq1i 6660	. . . . . . . . . . . . . . 15
228	178, 220, 221	divcan3i 10771	. . . . . . . . . . . . . . 15
229	227, 228	eqtr3i 2646	. . . . . . . . . . . . . 14
230	229	oveq1i 6660	. . . . . . . . . . . . 13
231	225, 230	syl6eq 2672	. . . . . . . . . . . 12
232	124	recnd 10068	. . . . . . . . . . . . 13
233		remulcl 10021	. . . . . . . . . . . . . . 15 $/\$
234	118, 36, 233	sylancr 695	. . . . . . . . . . . . . 14
235	234	recnd 10068	. . . . . . . . . . . . 13
236		divdir 10710	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
237	222, 236	mp3an3 1413	. . . . . . . . . . . . 13 $/\$
238	232, 235, 237	syl2anc 693	. . . . . . . . . . . 12
239	218, 231, 238	3eqtr3d 2664	. . . . . . . . . . 11
240	239	oveq1d 6665	. . . . . . . . . 10
241	126	recnd 10068	. . . . . . . . . . 11
242		3rp 11838	. . . . . . . . . . . . 13
243		rpdivcl 11856	. . . . . . . . . . . . 13 $/\$
244	95, 242, 243	sylancl 694	. . . . . . . . . . . 12
245	244	rpcnd 11874	. . . . . . . . . . 11
246	241, 245	pncan2d 10394	. . . . . . . . . 10
247	240, 246	eqtrd 2656	. . . . . . . . 9
248	247	oveq1d 6665	. . . . . . . 8
249	101	recnd 10068	. . . . . . . . 9
250	235, 241, 249	subdird 10487	. . . . . . . 8
251	248, 250	eqtr3d 2658	. . . . . . 7
252	134	recnd 10068	. . . . . . . 8
253	169, 252, 170	nnncan2d 10427	. . . . . . 7
254	211, 251, 253	3eqtr4d 2666	. . . . . 6
255	117	recnd 10068	. . . . . . . . . 10
256	178	a1i 11	. . . . . . . . . 10
257	121	recnd 10068	. . . . . . . . . 10
258	255, 256, 257	adddird 10065	. . . . . . . . 9
259		relogmul 24338	. . . . . . . . . . . . 13 $/\$
260	91, 61, 259	sylancr 695	. . . . . . . . . . . 12
261	260	oveq2d 6666	. . . . . . . . . . 11
262	256, 249, 170	adddid 10064	. . . . . . . . . . 11
263	261, 262	eqtrd 2656	. . . . . . . . . 10
264	263	oveq2d 6666	. . . . . . . . 9
265	258, 264	eqtrd 2656	. . . . . . . 8
266		5cn 11100	. . . . . . . . . . . 12
267	266	a1i 11	. . . . . . . . . . 11
268	241, 267, 249	subdird 10487	. . . . . . . . . 10
269	268	oveq1d 6665	. . . . . . . . 9
270	266, 198	mulcli 10045	. . . . . . . . . . 11
271	270	a1i 11	. . . . . . . . . 10
272	252, 271, 170	nnncan1d 10426	. . . . . . . . 9
273	269, 272	eqtrd 2656	. . . . . . . 8
274	265, 273	oveq12d 6668	. . . . . . 7
275	135	recnd 10068	. . . . . . . 8
276	184, 185, 275	addsubassd 10412	. . . . . . 7
277	266, 220, 198	subdiri 10480	. . . . . . . . . . . . 13
278		3p2e5 11160	. . . . . . . . . . . . . . . 16
279	278	oveq1i 6660	. . . . . . . . . . . . . . 15
280		pncan2 10288	. . . . . . . . . . . . . . . 16 $/\$
281	220, 178, 280	mp2an 708	. . . . . . . . . . . . . . 15
282	279, 281	eqtr3i 2646	. . . . . . . . . . . . . 14
283	282	oveq1i 6660	. . . . . . . . . . . . 13
284	277, 283	eqtr3i 2646	. . . . . . . . . . . 12
285	284	a1i 11	. . . . . . . . . . 11
286		df-3 11080	. . . . . . . . . . . . . . . 16
287	286	oveq1i 6660	. . . . . . . . . . . . . . 15
288		1cnd 10056	. . . . . . . . . . . . . . . 16
289	256, 288, 170	adddird 10065	. . . . . . . . . . . . . . 15
290	287, 289	syl5eq 2668	. . . . . . . . . . . . . 14
291	170	mulid2d 10058	. . . . . . . . . . . . . . 15
292	291	oveq2d 6666	. . . . . . . . . . . . . 14
293	290, 292	eqtrd 2656	. . . . . . . . . . . . 13
294	293	oveq1d 6665	. . . . . . . . . . . 12
295		mulcl 10020	. . . . . . . . . . . . . 14 $/\$
296	178, 170, 295	sylancr 695	. . . . . . . . . . . . 13
297	296, 170, 271	addsubassd 10412	. . . . . . . . . . . 12
298	294, 297	eqtrd 2656	. . . . . . . . . . 11
299	285, 298	oveq12d 6668	. . . . . . . . . 10
300		relogdiv 24339	. . . . . . . . . . . . . 14 $/\$
301	61, 91, 300	sylancl 694	. . . . . . . . . . . . 13
302	301	oveq2d 6666	. . . . . . . . . . . 12
303		subdi 10463	. . . . . . . . . . . . . 14 $/\$ $/\$
304	220, 198, 303	mp3an13 1415	. . . . . . . . . . . . 13
305	170, 304	syl 17	. . . . . . . . . . . 12
306	302, 305	eqtrd 2656	. . . . . . . . . . 11
307		div23 10704	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
308	178, 222, 307	mp3an13 1415	. . . . . . . . . . . . . . . 16
309	194, 308	syl 17	. . . . . . . . . . . . . . 15
310	220, 178, 220, 178, 179, 179	divmuldivi 10785	. . . . . . . . . . . . . . . . 17
311		3t3e9 11180	. . . . . . . . . . . . . . . . . 18
312	311, 205	oveq12i 6662	. . . . . . . . . . . . . . . . 17
313	310, 312	eqtr2i 2645	. . . . . . . . . . . . . . . 16
314	313	a1i 11	. . . . . . . . . . . . . . 15
315	309, 314	oveq12d 6668	. . . . . . . . . . . . . 14
316	178, 220, 221	divcli 10767	. . . . . . . . . . . . . . 15
317	220, 178, 179	divcli 10767	. . . . . . . . . . . . . . . 16
318		mul4 10205	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
319	317, 317, 318	mpanr12 721	. . . . . . . . . . . . . . 15 $/\$
320	316, 194, 319	sylancr 695	. . . . . . . . . . . . . 14
321		divcan6 10732	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
322	178, 179, 220, 221, 321	mp4an 709	. . . . . . . . . . . . . . . . 17
323	322	oveq1i 6660	. . . . . . . . . . . . . . . 16
324		mulcl 10020	. . . . . . . . . . . . . . . . . 18 $/\$
325	194, 317, 324	sylancl 694	. . . . . . . . . . . . . . . . 17
326	325	mulid2d 10058	. . . . . . . . . . . . . . . 16
327	323, 326	syl5eq 2668	. . . . . . . . . . . . . . 15
328		2cnne0 11242	. . . . . . . . . . . . . . . . 17 $/\$
329		div12 10707	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
330	220, 328, 329	mp3an23 1416	. . . . . . . . . . . . . . . 16
331	194, 330	syl 17	. . . . . . . . . . . . . . 15
332	327, 331	eqtrd 2656	. . . . . . . . . . . . . 14
333	315, 320, 332	3eqtrd 2660	. . . . . . . . . . . . 13
334	333, 84	oveq12d 6668	. . . . . . . . . . . 12
335	77	recni 10052	. . . . . . . . . . . . . 14
336	335	a1i 11	. . . . . . . . . . . . 13
337	87	recnd 10068	. . . . . . . . . . . . 13
338	245, 336, 337	mulassd 10063	. . . . . . . . . . . 12
339	220	a1i 11	. . . . . . . . . . . . . 14
340	78	rpcnd 11874	. . . . . . . . . . . . . 14
341	85	recnd 10068	. . . . . . . . . . . . . . 15
342	78	rpne0d 11877	. . . . . . . . . . . . . . 15
343	341, 340, 342	divcld 10801	. . . . . . . . . . . . . 14
344	339, 340, 343	mulassd 10063	. . . . . . . . . . . . 13
345	341, 340, 342	divcan2d 10803	. . . . . . . . . . . . . 14
346	345	oveq2d 6666	. . . . . . . . . . . . 13
347	344, 346	eqtrd 2656	. . . . . . . . . . . 12
348	334, 338, 347	3eqtr3d 2664	. . . . . . . . . . 11
349	220, 198	mulcli 10045	. . . . . . . . . . . . 13
350	349	a1i 11	. . . . . . . . . . . 12
351		mulcl 10020	. . . . . . . . . . . . 13 $/\$
352	220, 170, 351	sylancr 695	. . . . . . . . . . . 12
353	271, 350, 352	npncan3d 10428	. . . . . . . . . . 11
354	306, 348, 353	3eqtr4d 2666	. . . . . . . . . 10
355	118, 93	remulcli 10054	. . . . . . . . . . . . 13
356	355	recni 10052	. . . . . . . . . . . 12
357	356	a1i 11	. . . . . . . . . . 11
358		subcl 10280	. . . . . . . . . . . 12 $/\$
359	170, 270, 358	sylancl 694	. . . . . . . . . . 11
360	357, 296, 359	addassd 10062	. . . . . . . . . 10
361	299, 354, 360	3eqtr4d 2666	. . . . . . . . 9
362	361	oveq2d 6666	. . . . . . . 8
363		mulcl 10020	. . . . . . . . . . 11 $/\$
364	255, 198, 363	sylancl 694	. . . . . . . . . 10
365	255, 170	mulcld 10060	. . . . . . . . . 10
366	89	recnd 10068	. . . . . . . . . . 11
367	245, 366	mulcld 10060	. . . . . . . . . 10
368	364, 365, 367	addassd 10062	. . . . . . . . 9
369	260	oveq2d 6666	. . . . . . . . . . 11
370	255, 249, 170	adddid 10064	. . . . . . . . . . 11
371	369, 370	eqtrd 2656	. . . . . . . . . 10
372	371	oveq1d 6665	. . . . . . . . 9
373	59	oveq2d 6666	. . . . . . . . . . 11
374	90	recnd 10068	. . . . . . . . . . . 12
375	98	recnd 10068	. . . . . . . . . . . 12
376	245, 374, 375	adddid 10064	. . . . . . . . . . 11
377	373, 376	eqtrd 2656	. . . . . . . . . 10
378	73	recnd 10068	. . . . . . . . . . . . 13
379	245, 378, 366	adddid 10064	. . . . . . . . . . . 12
380	95	rpge0d 11876	. . . . . . . . . . . . . . . . . 18
381		remsqsqrt 13997	. . . . . . . . . . . . . . . . . 18 $/\$
382	234, 380, 381	syl2anc 693	. . . . . . . . . . . . . . . . 17
383	382	oveq1d 6665	. . . . . . . . . . . . . . . 16
384	114	recnd 10068	. . . . . . . . . . . . . . . . 17
385	221	a1i 11	. . . . . . . . . . . . . . . . 17
386	384, 384, 339, 385	div23d 10838	. . . . . . . . . . . . . . . 16
387	383, 386	eqtr3d 2658	. . . . . . . . . . . . . . 15
388	387	oveq1d 6665	. . . . . . . . . . . . . 14
389	255, 384, 378	mulassd 10063	. . . . . . . . . . . . . 14
390		0le2 11111	. . . . . . . . . . . . . . . . . . 19
391	118, 390	pm3.2i 471	. . . . . . . . . . . . . . . . . 18 $/\$
392	61	rprege0d 11879	. . . . . . . . . . . . . . . . . 18 $/\$
393		sqrtmul 14000	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
394	391, 392, 393	sylancr 695	. . . . . . . . . . . . . . . . 17
395	394	oveq1d 6665	. . . . . . . . . . . . . . . 16
396	60	recni 10052	. . . . . . . . . . . . . . . . . 18
397	396	a1i 11	. . . . . . . . . . . . . . . . 17
398	62	rpcnd 11874	. . . . . . . . . . . . . . . . 17
399	71	recnd 10068	. . . . . . . . . . . . . . . . 17
400	397, 398, 397, 399	mul4d 10248	. . . . . . . . . . . . . . . 16
401		remsqsqrt 13997	. . . . . . . . . . . . . . . . . . . 20 $/\$
402	118, 390, 401	mp2an 708	. . . . . . . . . . . . . . . . . . 19
403	402	a1i 11	. . . . . . . . . . . . . . . . . 18
404	68	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
405	69	recnd 10068	. . . . . . . . . . . . . . . . . . . 20
406	62	rpne0d 11877	. . . . . . . . . . . . . . . . . . . 20
407	405, 398, 406	divcan2d 10803	. . . . . . . . . . . . . . . . . . 19
408	404, 407	eqtrd 2656	. . . . . . . . . . . . . . . . . 18
409	403, 408	oveq12d 6668	. . . . . . . . . . . . . . . . 17
410	405	2timesd 11275	. . . . . . . . . . . . . . . . 17
411	62, 62	relogmuld 24371	. . . . . . . . . . . . . . . . . 18
412		remsqsqrt 13997	. . . . . . . . . . . . . . . . . . . 20 $/\$
413	392, 412	syl 17	. . . . . . . . . . . . . . . . . . 19
414	413	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
415	411, 414	eqtr3d 2658	. . . . . . . . . . . . . . . . 17
416	409, 410, 415	3eqtrd 2660	. . . . . . . . . . . . . . . 16
417	395, 400, 416	3eqtrd 2660	. . . . . . . . . . . . . . 15
418	417	oveq2d 6666	. . . . . . . . . . . . . 14
419	388, 389, 418	3eqtrd 2660	. . . . . . . . . . . . 13
420	419	oveq1d 6665	. . . . . . . . . . . 12
421	379, 420	eqtrd 2656	. . . . . . . . . . 11
422	387	oveq1d 6665	. . . . . . . . . . . 12
423	255, 384, 375	mulassd 10063	. . . . . . . . . . . 12
424	96	rpne0d 11877	. . . . . . . . . . . . . 14
425	249, 384, 424	divcan2d 10803	. . . . . . . . . . . . 13
426	425	oveq2d 6666	. . . . . . . . . . . 12
427	422, 423, 426	3eqtrd 2660	. . . . . . . . . . 11
428	421, 427	oveq12d 6668	. . . . . . . . . 10
429	365, 367	addcld 10059	. . . . . . . . . . 11
430	429, 364	addcomd 10238	. . . . . . . . . 10
431	377, 428, 430	3eqtrd 2660	. . . . . . . . 9
432	368, 372, 431	3eqtr4rd 2667	. . . . . . . 8
433	255, 257	mulcld 10060	. . . . . . . . 9
434		addcl 10018	. . . . . . . . . 10 $/\$
435	356, 296, 434	sylancr 695	. . . . . . . . 9
436	433, 435, 359	addassd 10062	. . . . . . . 8
437	362, 432, 436	3eqtr4d 2666	. . . . . . 7
438	274, 276, 437	3eqtr4rd 2667	. . . . . 6
439	193, 254, 438	3brtr4d 4685	. . . . 5
440	101, 100, 244	ltmul2d 11914	. . . . 5
441	439, 440	mpbird 247	. . . 4
442	45, 101, 100, 102, 441	lttrd 10198	. . 3 ;
443	45, 100, 442	ltnsymd 10186	. 2 ;
444	42, 443	pm2.21dd 186	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wrex 2913

cif 4086 class class class wbr 4653

cmpt 4729

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

c2 11070

c3 11071

c4 11072

c5 11073

c6 11074

c8 11076

c9 11077

cz 11377 ;cdc 11493

cuz 11687

crp 11832

cfl 12591

cexp 12860

cbc 13089

csqrt 13973

ce 14792

ceu 14793

cprime 15385

cpc 15541

clog 24301

ccxp 24302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-xnn0 11364 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-e 14799 df-sin 14800 df-cos 14801 df-pi 14803 df-dvds 14984 df-gcd 15217 df-prm 15386 df-pc 15542 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-cxp 24304 df-cht 24823 df-ppi 24826

This theorem is referenced by: bpos 25018

W3C validator