Theorem sqrlem11 6684

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 5347	. . . . . . . . . . 11 ⊢ (B · B) ∈ ℝ
3	2	recn 5326	. . . . . . . . . 10 ⊢ (B · B) ∈ ℂ
4		1re 5447	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
5	4, 4	readdcl 5346	. . . . . . . . . . . 12 ⊢ (1 + 1) ∈ ℝ
6	5	recn 5326	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℂ
7	6	negcl 5381	. . . . . . . . . 10 ⊢ -(1 + 1) ∈ ℂ
8		sqrlem1.1	. . . . . . . . . . . 12 ⊢ A ∈ ℝ
9	8	renegcl 5428	. . . . . . . . . . 11 ⊢ -A ∈ ℝ
10	9	recn 5326	. . . . . . . . . 10 ⊢ -A ∈ ℂ
11	3, 7, 10	mul12 5435	. . . . . . . . 9 ⊢ ((B · B) · (-(1 + 1) · -A)) = (-(1 + 1) · ((B · B) · -A))
12	2, 9	remulcl 5347	. . . . . . . . . . 11 ⊢ ((B · B) · -A) ∈ ℝ
13	12	recn 5326	. . . . . . . . . 10 ⊢ ((B · B) · -A) ∈ ℂ
14	6, 13	mulneg1 5457	. . . . . . . . 9 ⊢ (-(1 + 1) · ((B · B) · -A)) = -((1 + 1) · ((B · B) · -A))
15	13	1p1times 5445	. . . . . . . . . . 11 ⊢ ((1 + 1) · ((B · B) · -A)) = (((B · B) · -A) + ((B · B) · -A))
16	15	negeqi 5372	. . . . . . . . . 10 ⊢ -((1 + 1) · ((B · B) · -A)) = -(((B · B) · -A) + ((B · B) · -A))
17		df-neg 5370	. . . . . . . . . 10 ⊢ -(((B · B) · -A) + ((B · B) · -A)) = (0 − (((B · B) · -A) + ((B · B) · -A)))
18	16, 17	eqtr 1498	. . . . . . . . 9 ⊢ -((1 + 1) · ((B · B) · -A)) = (0 − (((B · B) · -A) + ((B · B) · -A)))
19	11, 14, 18	3eqtr 1502	. . . . . . . 8 ⊢ ((B · B) · (-(1 + 1) · -A)) = (0 − (((B · B) · -A) + ((B · B) · -A)))
20	2, 9	readdcl 5346	. . . . . . . . . . 11 ⊢ ((B · B) + -A) ∈ ℝ
21	8	recn 5326	. . . . . . . . . . . . 13 ⊢ A ∈ ℂ
22	21	negid 5392	. . . . . . . . . . . 12 ⊢ (A + -A) = 0
23		sqrlem9.6	. . . . . . . . . . . . 13 ⊢ A < (B · B)
24	8, 2, 9	ltadd1 5603	. . . . . . . . . . . . 13 ⊢ (A < (B · B) ↔ (A + -A) < ((B · B) + -A))
25	23, 24	mpbi 189	. . . . . . . . . . . 12 ⊢ (A + -A) < ((B · B) + -A)
26	22, 25	eqbrtrr 2641	. . . . . . . . . . 11 ⊢ 0 < ((B · B) + -A)
27	20, 20, 26, 26	mulgt0i 5620	. . . . . . . . . 10 ⊢ 0 < (((B · B) + -A) · ((B · B) + -A))
28	3, 10, 3, 10	muladd 5438	. . . . . . . . . 10 ⊢ (((B · B) + -A) · ((B · B) + -A)) = ((((B · B) · (B · B)) + (-A · -A)) + (((B · B) · -A) + ((B · B) · -A)))
29	27, 28	breqtr 2643	. . . . . . . . 9 ⊢ 0 < ((((B · B) · (B · B)) + (-A · -A)) + (((B · B) · -A) + ((B · B) · -A)))
30		0re 5452	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
31	12, 12	readdcl 5346	. . . . . . . . . 10 ⊢ (((B · B) · -A) + ((B · B) · -A)) ∈ ℝ
32	2, 2	remulcl 5347	. . . . . . . . . . 11 ⊢ ((B · B) · (B · B)) ∈ ℝ
33	9, 9	remulcl 5347	. . . . . . . . . . 11 ⊢ (-A · -A) ∈ ℝ
34	32, 33	readdcl 5346	. . . . . . . . . 10 ⊢ (((B · B) · (B · B)) + (-A · -A)) ∈ ℝ
35	30, 31, 34	ltsubadd 5606	. . . . . . . . 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))))
36	29, 35	mpbir 190	. . . . . . . 8 ⊢ (0 − (((B · B) · -A) + ((B · B) · -A))) < (((B · B) · (B · B)) + (-A · -A))
37	19, 36	eqbrtr 2639	. . . . . . 7 ⊢ ((B · B) · (-(1 + 1) · -A)) < (((B · B) · (B · B)) + (-A · -A))
38	5	renegcl 5428	. . . . . . . . . 10 ⊢ -(1 + 1) ∈ ℝ
39	38, 9	remulcl 5347	. . . . . . . . 9 ⊢ (-(1 + 1) · -A) ∈ ℝ
40	2, 39	remulcl 5347	. . . . . . . 8 ⊢ ((B · B) · (-(1 + 1) · -A)) ∈ ℝ
41		sqrlem9.5	. . . . . . . . 9 ⊢ 0 < B
42	1, 1, 41, 41	mulgt0i 5620	. . . . . . . 8 ⊢ 0 < (B · B)
43	40, 34, 2, 42	ltdiv1i 5825	. . . . . . 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)))
44	37, 43	mpbi 189	. . . . . 6 ⊢ (((B · B) · (-(1 + 1) · -A)) / (B · B)) < ((((B · B) · (B · B)) + (-A · -A)) / (B · B))
45	39	recn 5326	. . . . . . . 8 ⊢ (-(1 + 1) · -A) ∈ ℂ
46	1	recn 5326	. . . . . . . . 9 ⊢ B ∈ ℂ
47	1, 41	gt0ne0i 5629	. . . . . . . . 9 ⊢ B ≠ 0
48	46, 46, 47, 47	muln0 5711	. . . . . . . 8 ⊢ (B · B) ≠ 0
49	45, 3, 48	divcan3 5759	. . . . . . 7 ⊢ (((B · B) · (-(1 + 1) · -A)) / (B · B)) = (-(1 + 1) · -A)
50	6, 21	mul2neg 5459	. . . . . . 7 ⊢ (-(1 + 1) · -A) = ((1 + 1) · A)
51	49, 50	eqtr 1498	. . . . . 6 ⊢ (((B · B) · (-(1 + 1) · -A)) / (B · B)) = ((1 + 1) · A)
52	32	recn 5326	. . . . . . 7 ⊢ ((B · B) · (B · B)) ∈ ℂ
53	33	recn 5326	. . . . . . 7 ⊢ (-A · -A) ∈ ℂ
54	2, 42	gt0ne0i 5629	. . . . . . 7 ⊢ (B · B) ≠ 0
55	52, 53, 3, 54	divdir 5754	. . . . . 6 ⊢ ((((B · B) · (B · B)) + (-A · -A)) / (B · B)) = ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B)))
56	44, 51, 55	3brtr3 2647	. . . . 5 ⊢ ((1 + 1) · A) < ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B)))
57	5, 8	remulcl 5347	. . . . . 6 ⊢ ((1 + 1) · A) ∈ ℝ
58	32, 2, 54	redivcl 5800	. . . . . . 7 ⊢ (((B · B) · (B · B)) / (B · B)) ∈ ℝ
59	33, 2, 54	redivcl 5800	. . . . . . 7 ⊢ ((-A · -A) / (B · B)) ∈ ℝ
60	58, 59	readdcl 5346	. . . . . 6 ⊢ ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) ∈ ℝ
61	57, 60, 57	ltadd1 5603	. . . . 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)))
62	56, 61	mpbi 189	. . . 4 ⊢ (((1 + 1) · A) + ((1 + 1) · A)) < (((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) + ((1 + 1) · A))
63	5, 5	remulcl 5347	. . . . . . 7 ⊢ ((1 + 1) · (1 + 1)) ∈ ℝ
64	63	recn 5326	. . . . . 6 ⊢ ((1 + 1) · (1 + 1)) ∈ ℂ
65	21, 64	mulcom 5335	. . . . 5 ⊢ (A · ((1 + 1) · (1 + 1))) = (((1 + 1) · (1 + 1)) · A)
66	6, 6, 21	mulass 5337	. . . . 5 ⊢ (((1 + 1) · (1 + 1)) · A) = ((1 + 1) · ((1 + 1) · A))
67	57	recn 5326	. . . . . 6 ⊢ ((1 + 1) · A) ∈ ℂ
68	67	1p1times 5445	. . . . 5 ⊢ ((1 + 1) · ((1 + 1) · A)) = (((1 + 1) · A) + ((1 + 1) · A))
69	65, 66, 68	3eqtr 1502	. . . 4 ⊢ (A · ((1 + 1) · (1 + 1))) = (((1 + 1) · A) + ((1 + 1) · A))
70	8, 1, 47	redivcl 5800	. . . . . . 7 ⊢ (A / B) ∈ ℝ
71	70	recn 5326	. . . . . 6 ⊢ (A / B) ∈ ℂ
72	46, 71, 46, 71	muladd 5438	. . . . 5 ⊢ ((B + (A / B)) · (B + (A / B))) = (((B · B) + ((A / B) · (A / B))) + ((B · (A / B)) + (B · (A / B))))
73	3, 3, 54	divcan4 5760	. . . . . . . 8 ⊢ (((B · B) · (B · B)) / (B · B)) = (B · B)
74	73	eqcomi 1482	. . . . . . 7 ⊢ (B · B) = (((B · B) · (B · B)) / (B · B))
75	21, 46, 21, 46, 47, 47	divmuldiv 5788	. . . . . . . 8 ⊢ ((A / B) · (A / B)) = ((A · A) / (B · B))
76	21, 21	mul2neg 5459	. . . . . . . . 9 ⊢ (-A · -A) = (A · A)
77	76	opreq1i 3977	. . . . . . . 8 ⊢ ((-A · -A) / (B · B)) = ((A · A) / (B · B))
78	75, 77	eqtr4 1501	. . . . . . 7 ⊢ ((A / B) · (A / B)) = ((-A · -A) / (B · B))
79	74, 78	opreq12i 3979	. . . . . 6 ⊢ ((B · B) + ((A / B) · (A / B))) = ((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B)))
80	46, 71	mulcl 5333	. . . . . . . 8 ⊢ (B · (A / B)) ∈ ℂ
81	80	1p1times 5445	. . . . . . 7 ⊢ ((1 + 1) · (B · (A / B))) = ((B · (A / B)) + (B · (A / B)))
82	21, 46, 47	divcan2 5728	. . . . . . . 8 ⊢ (B · (A / B)) = A
83	82	opreq2i 3978	. . . . . . 7 ⊢ ((1 + 1) · (B · (A / B))) = ((1 + 1) · A)
84	81, 83	eqtr3 1500	. . . . . 6 ⊢ ((B · (A / B)) + (B · (A / B))) = ((1 + 1) · A)
85	79, 84	opreq12i 3979	. . . . 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))
86	72, 85	eqtr 1498	. . . 4 ⊢ ((B + (A / B)) · (B + (A / B))) = (((((B · B) · (B · B)) / (B · B)) + ((-A · -A) / (B · B))) + ((1 + 1) · A))
87	62, 69, 86	3brtr4 2648	. . 3 ⊢ (A · ((1 + 1) · (1 + 1))) < ((B + (A / B)) · (B + (A / B)))
88	8, 63	remulcl 5347	. . . 4 ⊢ (A · ((1 + 1) · (1 + 1))) ∈ ℝ
89	1, 70	readdcl 5346	. . . . 5 ⊢ (B + (A / B)) ∈ ℝ
90	89, 89	remulcl 5347	. . . 4 ⊢ ((B + (A / B)) · (B + (A / B))) ∈ ℝ
91		lt01 5692	. . . . . 6 ⊢ 0 < 1
92	4, 4, 91, 91	addgt0i 5613	. . . . 5 ⊢ 0 < (1 + 1)
93	5, 5, 92, 92	mulgt0i 5620	. . . 4 ⊢ 0 < ((1 + 1) · (1 + 1))
94	88, 90, 63, 93	ltdiv1i 5825	. . 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))))
95	87, 94	mpbi 189	. 2 ⊢ ((A · ((1 + 1) · (1 + 1))) / ((1 + 1) · (1 + 1))) < (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1)))
96	63, 93	gt0ne0i 5629	. . 3 ⊢ ((1 + 1) · (1 + 1)) ≠ 0
97	21, 64, 96	divcan4 5760	. 2 ⊢ ((A · ((1 + 1) · (1 + 1))) / ((1 + 1) · (1 + 1))) = A
98		sqrlem9.7	. . . 4 ⊢ C = ((B + (A / B)) / (1 + 1))
99	98, 98	opreq12i 3979	. . 3 ⊢ (C · C) = (((B + (A / B)) / (1 + 1)) · ((B + (A / B)) / (1 + 1)))
100	89	recn 5326	. . . 4 ⊢ (B + (A / B)) ∈ ℂ
101	5, 92	gt0ne0i 5629	. . . 4 ⊢ (1 + 1) ≠ 0
102	100, 6, 100, 6, 101, 101	divmuldiv 5788	. . 3 ⊢ (((B + (A / B)) / (1 + 1)) · ((B + (A / B)) / (1 + 1))) = (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1)))
103	99, 102	eqtr2 1499	. 2 ⊢ (((B + (A / B)) · (B + (A / B))) / ((1 + 1) · (1 + 1))) = (C · C)
104	95, 97, 103	3brtr3 2647	1 ⊢ A < (C · C)

Syntax hints:   = wceq 958   ∈ wcel 960   class class class wbr 2624  (class class class)co 3969  ℝcr 5245  0cc0 5246  1c1 5247   + caddc 5249   · cmul 5251   − cmin 5304  -cneg 5305   / cdiv 5306   < clt 5498

This theorem is referenced by:  sqrlem12 6685

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-nel 1591  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-rdg 3938  df-opr 3971  df-oprab 3972  df-1st 4085  df-2nd 4086  df-1o 4139  df-oadd 4141  df-omul 4142  df-er 4267  df-ec 4269  df-qs 4272  df-en 4374  df-dom 4375  df-sdom 4376  df-ni 5012  df-pli 5013  df-mi 5014  df-lti 5015  df-plpq 5047  df-mpq 5048  df-enq 5049  df-nq 5050  df-plq 5051  df-mq 5052  df-rq 5053  df-ltq 5054  df-1q 5055  df-np 5098  df-1p 5099  df-plp 5100  df-mp 5101  df-ltp 5102  df-plpr 5176  df-mpr 5177  df-enr 5178  df-nr 5179  df-plr 5180  df-mr 5181  df-ltr 5182  df-0r 5183  df-1r 5184  df-m1r 5185  df-c 5252  df-0 5253  df-1 5254  df-i 5255  df-r 5256  df-plus 5257  df-mul 5258  df-lt 5259  df-sub 5368  df-neg 5370  df-pnf 5499  df-mnf 5500  df-xr 5501  df-ltxr 5502  df-le 5503  df-div 5715

Copyright terms: Public domain