sqrlem11 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sqrlem11 6683

Description: Lemma for square root theorem.

**Hypotheses**
Ref	Expression
sqrlem1.1
sqrlem1.2
sqrlem9.3
sqrlem9.4
sqrlem9.5
sqrlem9.6
sqrlem9.7

**Assertion**
Ref	Expression
sqrlem11

**Proof of Theorem sqrlem11**
Step	Hyp	Ref	Expression
1		sqrlem9.3	. . . . . . . . . . . 12
2	1, 1	remulcl 5335	. . . . . . . . . . 11
3	2	recn 5314	. . . . . . . . . 10
4		1re 5435	. . . . . . . . . . . . 13
5	4, 4	readdcl 5334	. . . . . . . . . . . 12
6	5	recn 5314	. . . . . . . . . . 11
7	6	negcl 5369	. . . . . . . . . 10
8		sqrlem1.1	. . . . . . . . . . . 12
9	8	renegcl 5416	. . . . . . . . . . 11
10	9	recn 5314	. . . . . . . . . 10
11	3, 7, 10	mul12 5423	. . . . . . . . 9
12	2, 9	remulcl 5335	. . . . . . . . . . 11
13	12	recn 5314	. . . . . . . . . 10
14	6, 13	mulneg1 5445	. . . . . . . . 9
15	13	1p1times 5433	. . . . . . . . . . 11
16	15	negeqi 5360	. . . . . . . . . 10
17		df-neg 5358	. . . . . . . . . 10
18	16, 17	eqtr 1495	. . . . . . . . 9
19	11, 14, 18	3eqtr 1499	. . . . . . . 8
20	2, 9	readdcl 5334	. . . . . . . . . . 11
21	8	recn 5314	. . . . . . . . . . . . 13
22	21	negid 5380	. . . . . . . . . . . 12
23		sqrlem9.6	. . . . . . . . . . . . 13
24	8, 2, 9	ltadd1 5591	. . . . . . . . . . . . 13
25	23, 24	mpbi 189	. . . . . . . . . . . 12
26	22, 25	eqbrtrr 2636	. . . . . . . . . . 11
27	20, 20, 26, 26	mulgt0i 5608	. . . . . . . . . 10
28	3, 10, 3, 10	muladd 5426	. . . . . . . . . 10
29	27, 28	breqtr 2638	. . . . . . . . 9
30		0re 5440	. . . . . . . . . 10
31	12, 12	readdcl 5334	. . . . . . . . . 10
32	2, 2	remulcl 5335	. . . . . . . . . . 11
33	9, 9	remulcl 5335	. . . . . . . . . . 11
34	32, 33	readdcl 5334	. . . . . . . . . 10
35	30, 31, 34	ltsubadd 5594	. . . . . . . . 9
36	29, 35	mpbir 190	. . . . . . . 8
37	19, 36	eqbrtr 2634	. . . . . . 7
38	5	renegcl 5416	. . . . . . . . . 10
39	38, 9	remulcl 5335	. . . . . . . . 9
40	2, 39	remulcl 5335	. . . . . . . 8
41		sqrlem9.5	. . . . . . . . 9
42	1, 1, 41, 41	mulgt0i 5608	. . . . . . . 8
43	40, 34, 2, 42	ltdiv1i 5823	. . . . . . 7
44	37, 43	mpbi 189	. . . . . 6
45	39	recn 5314	. . . . . . . 8
46	1	recn 5314	. . . . . . . . 9
47	1, 41	gt0ne0i 5617	. . . . . . . . 9
48	46, 46, 47, 47	muln0 5699	. . . . . . . 8
49	45, 3, 48	divcan3 5752	. . . . . . 7
50	6, 21	mul2neg 5447	. . . . . . 7
51	49, 50	eqtr 1495	. . . . . 6
52	32	recn 5314	. . . . . . 7
53	33	recn 5314	. . . . . . 7
54	2, 42	gt0ne0i 5617	. . . . . . 7
55	52, 53, 3, 54	divdir 5747	. . . . . 6
56	44, 51, 55	3brtr3 2642	. . . . 5
57	5, 8	remulcl 5335	. . . . . 6
58	32, 2, 54	redivcl 5798	. . . . . . 7
59	33, 2, 54	redivcl 5798	. . . . . . 7
60	58, 59	readdcl 5334	. . . . . 6
61	57, 60, 57	ltadd1 5591	. . . . 5
62	56, 61	mpbi 189	. . . 4
63	5, 5	remulcl 5335	. . . . . . 7
64	63	recn 5314	. . . . . 6
65	21, 64	mulcom 5323	. . . . 5
66	6, 6, 21	mulass 5325	. . . . 5
67	57	recn 5314	. . . . . 6
68	67	1p1times 5433	. . . . 5
69	65, 66, 68	3eqtr 1499	. . . 4