sqrlem11 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sqrlem11 6621

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 5315	. . . . . . . . . . 11
3	2	recn 5294	. . . . . . . . . 10
4		1re 5415	. . . . . . . . . . . . 13
5	4, 4	readdcl 5314	. . . . . . . . . . . 12
6	5	recn 5294	. . . . . . . . . . 11
7	6	negcl 5349	. . . . . . . . . 10
8		sqrlem1.1	. . . . . . . . . . . 12
9	8	renegcl 5396	. . . . . . . . . . 11
10	9	recn 5294	. . . . . . . . . 10
11	3, 7, 10	mul12 5403	. . . . . . . . 9
12	2, 9	remulcl 5315	. . . . . . . . . . 11
13	12	recn 5294	. . . . . . . . . 10
14	6, 13	mulneg1 5425	. . . . . . . . 9
15	13	1p1times 5413	. . . . . . . . . . 11
16	15	negeqi 5340	. . . . . . . . . 10
17		df-neg 5338	. . . . . . . . . 10
18	16, 17	eqtr 1492	. . . . . . . . 9
19	11, 14, 18	3eqtr 1496	. . . . . . . 8
20	2, 9	readdcl 5314	. . . . . . . . . . 11
21	8	recn 5294	. . . . . . . . . . . . 13
22	21	negid 5360	. . . . . . . . . . . 12
23		sqrlem9.6	. . . . . . . . . . . . 13
24	8, 2, 9	ltadd1 5573	. . . . . . . . . . . . 13
25	23, 24	mpbi 189	. . . . . . . . . . . 12
26	22, 25	eqbrtrr 2631	. . . . . . . . . . 11
27	20, 20, 26, 26	mulgt0i 5590	. . . . . . . . . 10
28	3, 10, 3, 10	muladd 5406	. . . . . . . . . 10
29	27, 28	breqtr 2633	. . . . . . . . 9
30		0re 5420	. . . . . . . . . 10
31	12, 12	readdcl 5314	. . . . . . . . . 10
32	2, 2	remulcl 5315	. . . . . . . . . . 11
33	9, 9	remulcl 5315	. . . . . . . . . . 11
34	32, 33	readdcl 5314	. . . . . . . . . 10
35	30, 31, 34	ltsubadd 5576	. . . . . . . . 9
36	29, 35	mpbir 190	. . . . . . . 8
37	19, 36	eqbrtr 2629	. . . . . . 7
38	5	renegcl 5396	. . . . . . . . . 10
39	38, 9	remulcl 5315	. . . . . . . . 9
40	2, 39	remulcl 5315	. . . . . . . 8
41		sqrlem9.5	. . . . . . . . 9
42	1, 1, 41, 41	mulgt0i 5590	. . . . . . . 8
43	40, 34, 2, 42	ltdiv1i 5787	. . . . . . 7
44	37, 43	mpbi 189	. . . . . 6
45	39	recn 5294	. . . . . . . 8
46	1	recn 5294	. . . . . . . . 9
47	1, 41	gt0ne0i 5599	. . . . . . . . 9
48	46, 46, 47, 47	muln0 5676	. . . . . . . 8
49	3, 45, 48	divcan3 5722	. . . . . . 7
50	6, 21	mul2neg 5427	. . . . . . 7
51	49, 50	eqtr 1492	. . . . . 6
52	32	recn 5294	. . . . . . 7
53	33	recn 5294	. . . . . . 7
54	2, 42	gt0ne0i 5599	. . . . . . 7
55	52, 53, 3, 54	divdir 5718	. . . . . 6
56	44, 51, 55	3brtr3 2637	. . . . 5
57	5, 8	remulcl 5315	. . . . . 6
58	32, 2, 54	redivcl 5762	. . . . . . 7
59	33, 2, 54	redivcl 5762	. . . . . . 7
60	58, 59	readdcl 5314	. . . . . 6
61	57, 60, 57	ltadd1 5573	. . . . 5
62	56, 61	mpbi 189	. . . 4
63	5, 5	remulcl 5315	. . . . . . 7
64	63	recn 5294	. . . . . 6
65	21, 64	mulcom 5303	. . . . 5
66	6, 6, 21	mulass 5305	. . . . 5
67	57	recn 5294	. . . . . 6
68	67	1p1times 5413	. . . . 5
69	65, 66, 68	3eqtr 1496	. . . 4