Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem sqrlem11 4741

Description: Lemma for square root theorem.

**Hypotheses**
Ref	Expression
sqrlem1.1	⊢ A ∈ ℝ
sqrlem1.2	⊢ 0 < A
sqrlem9.3	⊢ B ∈ ℝ
sqrlem9.4	⊢ C ∈ ℝ
sqrlem9.5	⊢ 0 < B
sqrlem9.6	⊢ A < (B · B)
sqrlem9.7	⊢ C = ((B + (A / B)) / (1 + 1))

**Assertion**
Ref	Expression
sqrlem11	⊢ A < (C · C)

**Proof of Theorem sqrlem11**
Step	Hyp	Ref	Expression
1		sqrlem9.3	. . . . . . . . . . . 12 ⊢ B ∈ ℝ
2	1, 1	remulcl 4119	. . . . . . . . . . 11 ⊢ (B · B) ∈ ℝ
3	2	recn 4098	. . . . . . . . . 10 ⊢ (B · B) ∈ ℂ
4		1cn 4101	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
5	4, 4	addcl 4104	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℂ
6	5	negcl 4142	. . . . . . . . . 10 ⊢ -(1 + 1) ∈ ℂ
7		sqrlem1.1	. . . . . . . . . . . 12 ⊢ A ∈ ℝ
8	7	renegcl 4171	. . . . . . . . . . 11 ⊢ -A ∈ ℝ
9	8	recn 4098	. . . . . . . . . 10 ⊢ -A ∈ ℂ
10	3, 6, 9	mul12 4178	. . . . . . . . 9 ⊢ ((B · B) · (-(1 + 1) · -A)) = (-(1 + 1) · ((B · B) · -A))
11	2, 8	remulcl 4119	. . . . . . . . . . 11 ⊢ ((B · B) · -A) ∈ ℝ
12	11	recn 4098	. . . . . . . . . 10 ⊢ ((B · B) · -A) ∈ ℂ
13	5, 12	mulneg1 4190	. . . . . . . . 9 ⊢ (-(1 + 1) · ((B · B) · -A)) = -((1 + 1) · ((B · B) · -A))
14	12	1p1times 4187	. . . . . . . . . . 11 ⊢ ((1 + 1) · ((B · B) · -A)) = (((B · B) · -A) + ((B · B) · -A))
15	14	negeqi 4137	. . . . . . . . . 10 ⊢ -((1 + 1) · ((B · B) · -A)) = -(((B · B) · -A) + ((B · B) · -A))
16		df-neg 4135	. . . . . . . . . 10 ⊢ -(((B · B) · -A) + ((B · B) · -A)) = (0 − (((B · B) · -A) + ((B · B) · -A)))
17	15, 16	eqtr 1119	. . . . . . . . 9 ⊢ -((1 + 1) · ((B · B) · -A)) = (0 − (((B · B) · -A) + ((B · B) · -A)))
18	10, 13, 17	3eqtr 1123	. . . . . . . 8 ⊢ ((B · B) · (-(1 + 1) · -A)) = (0 − (((B · B) · -A) + ((B · B) · -A)))
19	2, 8	readdcl 4118	. . . . . . . . . . 11 ⊢ ((B · B) + -A) ∈ ℝ
20	7	recn 4098	. . . . . . . . . . . . 13 ⊢ A ∈ ℂ
21	20	negid 4147	. . . . . . . . . . . 12 ⊢ (A + -A) = 0
22		sqrlem9.6	. . . . . . . . . . . . 13 ⊢ A < (B · B)
23	7, 2, 8	ltadd1 4313	. . . . . . . . . . . . 13 ⊢ (A < (B · B) ↔ (A + -A) < ((B · B) + -A))
24	22, 23	mpbi 164	. . . . . . . . . . . 12 ⊢ (A + -A) < ((B · B) + -A)
25	21, 24	eqbrtrr 2078	. . . . . . . . . . 11 ⊢ 0 < ((B · B) + -A)
26	19, 19, 25, 25	mulgt0i 4336	. . . . . . . . . 10 ⊢ 0 < (((B · B) + -A) · ((B · B) + -A))
27	3, 9, 3, 9	muladd 4181	. . . . . . . . . 10 ⊢ (((B · B) + -A) · ((B · B) + -A)) = ((((B · B) · (B · B)) + (-A · -A)) + (((B · B) · -A) + ((B · B) · -A)))
28	26, 27	breqtr 2080	. . . . . . . . 9 ⊢ 0 < ((((B · B) · (B · B)) + (-A · -A)) + (((B · B) · -A) + ((B · B) · -A)))
29		ax0re 4063	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
30	11, 11	readdcl 4118	. . . . . . . . . 10 ⊢ (((B · B) · -A) + ((B · B) · -A)) ∈ ℝ
31	2, 2	remulcl 4119	. . . . . . . . . . 11 ⊢ ((B · B) · (B · B)) ∈ ℝ
32	8, 8	remulcl 4119	. . . . . . . . . . 11 ⊢ (-A · -A) ∈ ℝ
33	31, 32	readdcl 4118	. . . . . . . . . 10 ⊢ (((B · B) · (B · B)) + (-A · -A)) ∈ ℝ
34	29, 30, 33	ltsubadd 4316	. . . . . . . . 9 ⊢ ((0 − (((B · B) · -A) + ((B · B) · -A))) < (((B · B) · (B · B)) + (-A · -A)) ↔ 0 < ((((B · B) · (B · B)) + (-A · -A)) + (((B · B) · -A) + ((B · B) · -A))))
35	28, 34	mpbir 165	. . . . . . . 8 ⊢ (0 − (((B · B) · -A) + ((B · B) · -A))) < (((B · B) · (B · B)) + (-A · -A))
36	18, 35	eqbrtr 2076	. . . . . . 7 ⊢ ((B · B) · (-(1 + 1) · -A)) < (((B · B) · (B · B)) + (-A · -A))
37		ax1re 4064	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
38	37, 37	readdcl 4118	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℝ
39	38	renegcl 4171	. . . . . . . . . 10 ⊢ -(1 + 1) ∈ ℝ
40	39, 8	remulcl 4119	. . . . . . . . 9 ⊢ (-(1 + 1) · -A) ∈ ℝ
41	2, 40	remulcl 4119	. . . . . . . 8 ⊢ ((B · B) · (-(1 + 1) · -A)) ∈ ℝ
42		sqrlem9.5	. . . . . . . . 9 ⊢ 0 < B
43	1, 1, 42, 42	mulgt0i 4336	. . . . . . . 8 ⊢ 0 < (B · B)
44	41, 33, 2, 43	ltdivi 4398	. . . . . . 7 ⊢ (((B · B) · (-(1 + 1) · -A)) < (((B · B) · (B · B)) + (-A · -A)) ↔ (((B · B) · (-(1 + 1) · -A)) / (B · B)) < ((((B · B) · (B · B)) + (-A · -A)) / (B · B)))
45	36, 44	mpbi 164	. . . . . 6 ⊢ (((B · B) · (-(1 + 1) · -A)) / (B · B)) < ((((B · B) · (B · B)) + (-A · -A)) / (B · B))
46	6, 9	mulcl 4105	. . . . . . . 8 ⊢ (-(1 + 1) · -A) ∈ ℂ
47	1	recn 4098	. . . . . . . . 9 ⊢ B ∈ ℂ
48	1, 42	gt0ne0i 4345	. . . . . . . . 9 ⊢ B ≠ 0
49	47, 47, 48, 48	muln0 4214	. . . . . . . 8 ⊢ (B · B) ≠ 0
50	3, 46, 49	divcan3 4247	. . . . . . 7 ⊢ (((B · B) · (-(1 + 1) · -A)) / (B · B)) = (-(1 + 1) · -A)
51	5, 20	mul2neg 4192	. . . . . . 7 ⊢ (-(1 + 1) · -A) = ((1 + 1) · A)
52	50, 51	eqtr 1119	. . . . . 6 ⊢ (((B · B) · (-(1 + 1) · -A)) / (B · B)) = ((1 + 1) · A)
53	31	recn 4098	. . . . . . 7 ⊢ ((B · B) · (B · B)) ∈ ℂ
54	32	recn 4098	. . . . . . 7 ⊢ (-A · -A) ∈ ℂ
55	2, 43	gt0ne0i 4345	. . . . . . 7 ⊢ (B · B) ≠ 0
56	53, 54, 3, 55	divdistr 4243	. . . . . 6 ⊢ ((((B · B) · (B · B)) + (-A · -A)) / (B · B)) = ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B)))
57	45, 52, 56	3brtr3 2084	. . . . 5 ⊢ ((1 + 1) · A) < ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B)))
58	38, 7	remulcl 4119	. . . . . 6 ⊢ ((1 + 1) · A) ∈ ℝ
59	31, 2, 55	redivcl 4274	. . . . . . 7 ⊢ (((B · B) · (B · B)) / (B · B)) ∈ ℝ
60	32, 2, 55	redivcl 4274	. . . . . . 7 ⊢ ((-A · -A) / (B · B)) ∈ ℝ
61	59, 60	readdcl 4118	. . . . . 6 ⊢ ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) ∈ ℝ
62	58, 61, 58	ltadd1 4313	. . . . 5 ⊢ (((1 + 1) · A) < ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) ↔ (((1 + 1) · A) + ((1 + 1) · A)) < (((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) + ((1 + 1) · A)))
63	57, 62	mpbi 164	. . . 4 ⊢ (((1 + 1) · A) + ((1 + 1) · A)) < (((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) + ((1 + 1) · A))
64	5, 5	mulcl 4105	. . . . . 6 ⊢ ((1 + 1) · (1 + 1)) ∈ ℂ
65	20, 64	mulcom 4107	. . . . 5 ⊢ (A · ((1 + 1) · (1 + 1))) = (((1 + 1) · (1 + 1)) · A)
66	5, 5, 20	mulass 4109	. . . . 5 ⊢ (((1 + 1) · (1 + 1)) · A) = ((1 + 1) · ((1 + 1) · A))
67	5, 20	mulcl 4105	. . . . . 6 ⊢ ((1 + 1) · A) ∈ ℂ
68	67	1p1times 4187	. . . . 5 ⊢ ((1 + 1) · ((1 + 1) · A)) = (((1 + 1) · A) + ((1 + 1) · A))
69	65, 66, 68	3eqtr 1123	. . . 4 ⊢ (A · ((1 + 1) · (1 + 1))) = (((1 + 1) · A) + ((1 + 1) · A))
70	20, 47, 48	divcl 4221	. . . . . 6 ⊢ (A / B) ∈ ℂ
71	47, 70, 47, 70	muladd 4181	. . . . 5 ⊢ ((B + (A / B)) · (B + (A / B))) = (((B · B) + ((A / B) · (A / B))) + ((B · (A / B)) + (B · (A / B))))
72	3, 3, 55	divcan4 4248	. . . . . . . 8 ⊢ (((B · B) · (B · B)) / (B · B)) = (B · B)
73	72	cleqcomi 1105	. . . . . . 7 ⊢ (B · B) = (((B · B) · (B · B)) / (B · B))
74	20, 47, 20, 47, 48, 48	divmuldiv 4266	. . . . . . . 8 ⊢ ((A / B) · (A / B)) = ((A · A) / (B · B))
75	20, 20	mul2neg 4192	. . . . . . . . 9 ⊢ (-A · -A) = (A · A)
76	75	opreq1i 3009	. . . . . . . 8 ⊢ ((-A · -A) / (B · B)) = ((A · A) / (B · B))
77	74, 76	eqtr4 1122	. . . . . . 7 ⊢ ((A / B) · (A / B)) = ((-A · -A) / (B · B))
78	73, 77	opreq12i 3011	. . . . . 6 ⊢ ((B · B) + ((A / B) · (A / B))) = ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B)))
79	47, 70	mulcl 4105	. . . . . . . 8 ⊢ (B · (A / B)) ∈ ℂ
80	79	1p1times 4187	. . . . . . 7 ⊢ ((1 + 1) · (B · (A / B))) = ((B · (A / B)) + (B · (A / B)))
81	47, 20, 48	divcan2 4224	. . . . . . . 8 ⊢ (B · (A / B)) = A
82	81	opreq2i 3010	. . . . . . 7 ⊢ ((1 + 1) · (B · (A / B))) = ((1 + 1) · A)
83	80, 82	eqtr3 1121	. . . . . 6 ⊢ ((B · (A / B)) + (B · (A / B))) = ((1 + 1) · A)
84	78, 83	opreq12i 3011	. . . . 5 ⊢ (((B · B) + ((A / B) · (A / B))) + ((B · (A / B)) + (B · (A / B)))) = (((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) + ((1 + 1) · A))
85	71, 84	eqtr 1119	. . . 4 ⊢ ((B + (A / B)) · (B + (A / B))) = (((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) + ((1 + 1) · A))
86	63, 69, 85	3brtr4 2085	. . 3 ⊢ (A · ((1 + 1) · (1 + 1))) < ((B + (A / B)) · (B + (A / B)))
87	38, 38	remulcl 4119	. . . . 5 ⊢ ((1 + 1) · (1 + 1)) ∈ ℝ
88	7, 87	remulcl 4119	. . . 4 ⊢ (A · ((1 + 1) · (1 + 1))) ∈ ℝ
89	7, 1, 48	redivcl 4274	. . . . . 6 ⊢ (A / B) ∈ ℝ
90	1, 89	readdcl 4118	. . . . 5 ⊢ (B + (A / B)) ∈ ℝ
91	90, 90	remulcl 4119	. . . 4 ⊢ ((B + (A / B)) · (B + (A / B))) ∈ ℝ
92		lt01 4377	. . . . . 6 ⊢ 0 < 1
93	37, 37, 92, 92	addgt0i 4326	. . . . 5 ⊢ 0 < (1 + 1)
94	38, 38, 93, 93	mulgt0i 4336	. . . 4 ⊢ 0 < ((1 + 1) · (1 + 1))
95	88, 91, 87, 94	ltdivi 4398	. . 3 ⊢ ((A · ((1 + 1) · (1 + 1))) < ((B + (A / B)) · (B + (A / B))) ↔ ((A · ((1 + 1) · (1 + 1))) / ((1 + 1) · (1 + 1))) < (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1))))
96	86, 95	mpbi 164	. 2 ⊢ ((A · ((1 + 1) · (1 + 1))) / ((1 + 1) · (1 + 1))) < (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1)))
97	87	recn 4098	. . 3 ⊢ ((1 + 1) · (1 + 1)) ∈ ℂ
98	87, 94	gt0ne0i 4345	. . 3 ⊢ ((1 + 1) · (1 + 1)) ≠ 0
99	97, 20, 98	divcan4 4248	. 2 ⊢ ((A · ((1 + 1) · (1 + 1))) / ((1 + 1) · (1 + 1))) = A
100		sqrlem9.7	. . . 4 ⊢ C = ((B + (A / B)) / (1 + 1))
101	100, 100	opreq12i 3011	. . 3 ⊢ (C · C) = (((B + (A / B)) / (1 + 1)) · ((B + (A / B)) / (1 + 1)))
102	47, 70	addcl 4104	. . . 4 ⊢ (B + (A / B)) ∈ ℂ
103	38, 93	gt0ne0i 4345	. . . 4 ⊢ (1 + 1) ≠ 0
104	102, 5, 102, 5, 103, 103	divmuldiv 4266	. . 3 ⊢ (((B + (A / B)) / (1 + 1)) · ((B + (A / B)) / (1 + 1))) = (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1)))
105	101, 104	eqtr2 1120	. 2 ⊢ (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1))) = (C · C)
106	96, 99, 105	3brtr3 2084	1 ⊢ A < (C · C)

Colors of variables: wff set class

Syntax hints: = wceq 1091 ∈ wcel 1092 class class class wbr 2054 (class class class)co 3001 ℝcr 4027 0cc0 4028 1c1 4029 + caddc 4031 · cmulc 4032 < clt 4033 − cmin 4089 -cneg 4090 / cdiv 4091

This theorem is referenced by: sqrlem12 4742

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277

metamath.org