This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 01sqrexlem7

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

Ref Expression
Hypotheses 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
01sqrexlem5.3 ⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
Assertion 01sqrexlem7 ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3 01sqrexlem5.3 ⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
4 1 2 3 01sqrexlem6 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ≤ 𝐴 )
5 1 2 01sqrexlem3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
6 5 adantr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
7 1 2 01sqrexlem4 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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 ) = 𝐴 )