Metamath Proof Explorer


Theorem sqrlem7

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Hypotheses sqrlem1.1 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
sqrlem1.2 𝐵 = sup ( 𝑆 , ℝ , < )
sqrlem5.3 𝑇 = { 𝑦 ∣ ∃ 𝑎𝑆𝑏𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
Assertion sqrlem7 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 sqrlem1.1 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 sqrlem1.2 𝐵 = sup ( 𝑆 , ℝ , < )
3 sqrlem5.3 𝑇 = { 𝑦 ∣ ∃ 𝑎𝑆𝑏𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
4 1 2 3 sqrlem6 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ≤ 𝐴 )
5 1 2 sqrlem3 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) )
6 5 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) )
7 1 2 sqrlem4 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ∈ ℝ+𝐵 ≤ 1 ) )
8 7 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 ∈ ℝ+𝐵 ≤ 1 ) )
9 8 simpld ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐵 ∈ ℝ+ )
10 rpre ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ )
11 10 adantr ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐴 ∈ ℝ )
12 rpre ( 𝐵 ∈ ℝ+𝐵 ∈ ℝ )
13 12 adantr ( ( 𝐵 ∈ ℝ+𝐵 ≤ 1 ) → 𝐵 ∈ ℝ )
14 7 13 syl ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐵 ∈ ℝ )
15 14 resqcld ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
16 11 15 resubcld ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
17 16 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
18 15 11 posdifd ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( ( 𝐵 ↑ 2 ) < 𝐴 ↔ 0 < ( 𝐴 − ( 𝐵 ↑ 2 ) ) ) )
19 18 biimpa ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 0 < ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
20 17 19 elrpd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ+ )
21 3rp 3 ∈ ℝ+
22 rpdivcl ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ+ )
23 20 21 22 sylancl ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ+ )
24 9 23 rpaddcld ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ+ )
25 14 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐵 ∈ ℝ )
26 25 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐵 ∈ ℂ )
27 3nn 3 ∈ ℕ
28 nndivre ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ )
29 16 27 28 sylancl ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ )
30 29 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ )
31 30 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℂ )
32 binom2 ( ( 𝐵 ∈ ℂ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℂ ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) )
33 26 31 32 syl2anc ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) )
34 15 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
35 34 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
36 2re 2 ∈ ℝ
37 25 30 remulcld ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ )
38 remulcl ( ( 2 ∈ ℝ ∧ ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ∈ ℝ )
39 36 37 38 sylancr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ∈ ℝ )
40 39 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ∈ ℂ )
41 30 resqcld ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ∈ ℝ )
42 41 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ∈ ℂ )
43 35 40 42 addassd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) )
44 33 43 eqtrd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) )
45 2cn 2 ∈ ℂ
46 mulass ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℂ ) → ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
47 45 26 31 46 mp3an2i ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
48 47 eqcomd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) = ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
49 31 sqvald ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) = ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
50 48 49 oveq12d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) = ( ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
51 remulcl ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐵 ) ∈ ℝ )
52 36 25 51 sylancr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ∈ ℝ )
53 52 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ∈ ℂ )
54 53 31 31 adddird ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
55 50 54 eqtr4d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) = ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
56 7 simprd ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐵 ≤ 1 )
57 1red ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 1 ∈ ℝ )
58 2rp 2 ∈ ℝ+
59 58 a1i ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 2 ∈ ℝ+ )
60 14 57 59 lemul2d ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ≤ 1 ↔ ( 2 · 𝐵 ) ≤ ( 2 · 1 ) ) )
61 56 60 mpbid ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 2 · 𝐵 ) ≤ ( 2 · 1 ) )
62 61 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ≤ ( 2 · 1 ) )
63 2t1e2 ( 2 · 1 ) = 2
64 62 63 breqtrdi ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ≤ 2 )
65 11 adantr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐴 ∈ ℝ )
66 1red ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 1 ∈ ℝ )
67 25 sqge0d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 0 ≤ ( 𝐵 ↑ 2 ) )
68 65 34 addge01d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 0 ≤ ( 𝐵 ↑ 2 ) ↔ 𝐴 ≤ ( 𝐴 + ( 𝐵 ↑ 2 ) ) ) )
69 67 68 mpbid ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐴 ≤ ( 𝐴 + ( 𝐵 ↑ 2 ) ) )
70 65 34 65 lesubaddd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 𝐴𝐴 ≤ ( 𝐴 + ( 𝐵 ↑ 2 ) ) ) )
71 69 70 mpbird ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 𝐴 )
72 simplr ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐴 ≤ 1 )
73 17 65 66 71 72 letrd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 )
74 1le3 1 ≤ 3
75 1re 1 ∈ ℝ
76 3re 3 ∈ ℝ
77 letr ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 3 ∈ ℝ ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 ∧ 1 ≤ 3 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
78 75 76 77 mp3an23 ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 ∧ 1 ≤ 3 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
79 17 78 syl ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 ∧ 1 ≤ 3 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
80 74 79 mpan2i ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
81 73 80 mpd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 )
82 3t1e3 ( 3 · 1 ) = 3
83 81 82 breqtrrdi ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) )
84 3pos 0 < 3
85 ledivmul ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
86 75 85 mp3an2 ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
87 76 84 86 mpanr12 ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
88 17 87 syl ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
89 83 88 mpbird ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 )
90 le2add ( ( ( ( 2 · 𝐵 ) ∈ ℝ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ ) ∧ ( 2 ∈ ℝ ∧ 1 ∈ ℝ ) ) → ( ( ( 2 · 𝐵 ) ≤ 2 ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) ) )
91 36 75 90 mpanr12 ( ( ( 2 · 𝐵 ) ∈ ℝ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ ) → ( ( ( 2 · 𝐵 ) ≤ 2 ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) ) )
92 52 30 91 syl2anc ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) ≤ 2 ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) ) )
93 64 89 92 mp2and ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) )
94 df-3 3 = ( 2 + 1 )
95 93 94 breqtrrdi ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 3 )
96 52 30 readdcld ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ )
97 76 a1i ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 3 ∈ ℝ )
98 96 97 23 lemul1d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 3 ↔ ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
99 95 98 mpbid ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
100 17 recnd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℂ )
101 3cn 3 ∈ ℂ
102 3ne0 3 ≠ 0
103 divcan2 ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
104 101 102 103 mp3an23 ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℂ → ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
105 100 104 syl ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
106 99 105 breqtrd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
107 55 106 eqbrtrd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ≤ ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
108 39 41 readdcld ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ∈ ℝ )
109 34 108 65 leaddsub2d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) ≤ 𝐴 ↔ ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ≤ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ) )
110 107 109 mpbird ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) ≤ 𝐴 )
111 44 110 eqbrtrd ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) ≤ 𝐴 )
112 oveq1 ( 𝑦 = ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) → ( 𝑦 ↑ 2 ) = ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) )
113 112 breq1d ( 𝑦 = ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) → ( ( 𝑦 ↑ 2 ) ≤ 𝐴 ↔ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) ≤ 𝐴 ) )
114 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
115 114 breq1d ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) ≤ 𝐴 ↔ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) )
116 115 cbvrabv { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 } = { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 }
117 1 116 eqtri 𝑆 = { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 }
118 113 117 elrab2 ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 ↔ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ+ ∧ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) ≤ 𝐴 ) )
119 24 111 118 sylanbrc ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 )
120 suprub ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) ∧ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ sup ( 𝑆 , ℝ , < ) )
121 120 2 breqtrrdi ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) ∧ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
122 6 119 121 syl2anc ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
123 23 rpgt0d ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) )
124 29 14 ltaddposd ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↔ 𝐵 < ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
125 14 29 readdcld ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ )
126 14 125 ltnled ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 < ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↔ ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 ) )
127 124 126 bitrd ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↔ ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 ) )
128 127 biimpa ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) → ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
129 123 128 syldan ( ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
130 122 129 pm2.65da ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ¬ ( 𝐵 ↑ 2 ) < 𝐴 )
131 15 11 eqleltd ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( ( 𝐵 ↑ 2 ) = 𝐴 ↔ ( ( 𝐵 ↑ 2 ) ≤ 𝐴 ∧ ¬ ( 𝐵 ↑ 2 ) < 𝐴 ) ) )
132 4 130 131 mpbir2and ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = 𝐴 )