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 
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
sqrlem1.2 
|- B = sup ( S , RR , < )
sqrlem5.3 
|- T = { y | E. a e. S E. b e. S y = ( a x. b ) }
Assertion sqrlem7 
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = A )

Proof

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