Theorem sqrlem7 12009

Description: Lemma for 01sqrex 12010. (Contributed by Mario Carneiro, 10-Jul-2013.)

Hypotheses

Ref	Expression
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

Ref	Expression
sqrlem7	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = A )

Distinct variable groups:   a, b, y, S   x, a, A, b, y   y, B

Allowed substitution hints:   B( x, a, b)   S( x)   T( x, y, a, b)

Proof of Theorem sqrlem7

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sqrlem1.1	. . 3 |- S = { x e. RR+ | ( x ^ 2 ) <_ A }
2		sqrlem1.2	. . 3 |- B = sup ( S , RR , < )
3		sqrlem5.3	. . 3 |- T = { y | E. a e. S E. b e. S y = ( a x. b ) }
4	1, 2, 3	sqrlem6 12008	. 2 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) <_ A )
5	1, 2	sqrlem3 12005	. . . . 5 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) )
6	5	adantr 452	. . . 4 |- ( ( ( 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 12006	. . . . . . . 8 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B e. RR+ /\ B <_ 1 ) )
8	7	adantr 452	. . . . . . 7 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B e. RR+ /\ B <_ 1 ) )
9	8	simpld 446	. . . . . 6 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> B e. RR+ )
10		rpre 10574	. . . . . . . . . . 11 |- ( A e. RR+ -> A e. RR )
11	10	adantr 452	. . . . . . . . . 10 |- ( ( A e. RR+ /\ A <_ 1 ) -> A e. RR )
12		rpre 10574	. . . . . . . . . . . . 13 |- ( B e. RR+ -> B e. RR )
13	12	adantr 452	. . . . . . . . . . . 12 |- ( ( B e. RR+ /\ B <_ 1 ) -> B e. RR )
14	7, 13	syl 16	. . . . . . . . . . 11 |- ( ( A e. RR+ /\ A <_ 1 ) -> B e. RR )
15	14	resqcld 11504	. . . . . . . . . 10 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) e. RR )
16	11, 15	resubcld 9421	. . . . . . . . 9 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( A - ( B ^ 2 ) ) e. RR )
17	16	adantr 452	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) e. RR )
18	15, 11	posdifd 9569	. . . . . . . . 9 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( B ^ 2 ) < A <-> 0 < ( A - ( B ^ 2 ) ) ) )
19	18	biimpa 471	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> 0 < ( A - ( B ^ 2 ) ) )
20	17, 19	elrpd 10602	. . . . . . 7 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) e. RR+ )
21		3re 10027	. . . . . . . 8 |- 3 e. RR
22		3pos 10040	. . . . . . . 8 |- 0 < 3
23	21, 22	elrpii 10571	. . . . . . 7 |- 3 e. RR+
24		rpdivcl 10590	. . . . . . 7 |- ( ( ( A - ( B ^ 2 ) ) e. RR+ /\ 3 e. RR+ ) -> ( ( A - ( B ^ 2 ) ) / 3 ) e. RR+ )
25	20, 23, 24	sylancl 644	. . . . . 6 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( A - ( B ^ 2 ) ) / 3 ) e. RR+ )
26	9, 25	rpaddcld 10619	. . . . 5 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) e. RR+ )
27	14	adantr 452	. . . . . . . . 9 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> B e. RR )
28	27	recnd 9070	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> B e. CC )
29		3nn 10090	. . . . . . . . . . 11 |- 3 e. NN
30		nndivre 9991	. . . . . . . . . . 11 |- ( ( ( A - ( B ^ 2 ) ) e. RR /\ 3 e. NN ) -> ( ( A - ( B ^ 2 ) ) / 3 ) e. RR )
31	16, 29, 30	sylancl 644	. . . . . . . . . 10 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( A - ( B ^ 2 ) ) / 3 ) e. RR )
32	31	adantr 452	. . . . . . . . 9 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( A - ( B ^ 2 ) ) / 3 ) e. RR )
33	32	recnd 9070	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( A - ( B ^ 2 ) ) / 3 ) e. CC )
34		binom2 11451	. . . . . . . 8 |- ( ( 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 ) ) )
35	28, 33, 34	syl2anc 643	. . . . . . 7 |- ( ( ( 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 ) ) )
36	15	adantr 452	. . . . . . . . 9 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B ^ 2 ) e. RR )
37	36	recnd 9070	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B ^ 2 ) e. CC )
38		2re 10025	. . . . . . . . . 10 |- 2 e. RR
39	27, 32	remulcld 9072	. . . . . . . . . 10 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) e. RR )
40		remulcl 9031	. . . . . . . . . 10 |- ( ( 2 e. RR /\ ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) e. RR ) -> ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) e. RR )
41	38, 39, 40	sylancr 645	. . . . . . . . 9 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) e. RR )
42	41	recnd 9070	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) e. CC )
43	32	resqcld 11504	. . . . . . . . 9 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( ( A - ( B ^ 2 ) ) / 3 ) ^ 2 ) e. RR )
44	43	recnd 9070	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( ( A - ( B ^ 2 ) ) / 3 ) ^ 2 ) e. CC )
45	37, 42, 44	addassd 9066	. . . . . . 7 |- ( ( ( 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 ) ) ) )
46	35, 45	eqtrd 2436	. . . . . 6 |- ( ( ( 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 ) ) ) )
47		2cn 10026	. . . . . . . . . . . . 13 |- 2 e. CC
48		mulass 9034	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
49	47, 48	mp3an1 1266	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
50	28, 33, 49	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( 2 x. B ) x. ( ( A - ( B ^ 2 ) ) / 3 ) ) = ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) )
51	50	eqcomd 2409	. . . . . . . . . 10 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) = ( ( 2 x. B ) x. ( ( A - ( B ^ 2 ) ) / 3 ) ) )
52	33	sqvald 11475	. . . . . . . . . 10 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( ( A - ( B ^ 2 ) ) / 3 ) ^ 2 ) = ( ( ( A - ( B ^ 2 ) ) / 3 ) x. ( ( A - ( B ^ 2 ) ) / 3 ) ) )
53	51, 52	oveq12d 6058	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
54		remulcl 9031	. . . . . . . . . . . 12 |- ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
55	38, 27, 54	sylancr 645	. . . . . . . . . . 11 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. B ) e. RR )
56	55	recnd 9070	. . . . . . . . . 10 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. B ) e. CC )
57	56, 33, 33	adddird 9069	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
58	53, 57	eqtr4d 2439	. . . . . . . 8 |- ( ( ( 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 ) ) )
59	7	simprd 450	. . . . . . . . . . . . . . 15 |- ( ( A e. RR+ /\ A <_ 1 ) -> B <_ 1 )
60		2pos 10038	. . . . . . . . . . . . . . . . 17 |- 0 < 2
61		1re 9046	. . . . . . . . . . . . . . . . . 18 |- 1 e. RR
62		lemul2 9819	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( B <_ 1 <-> ( 2 x. B ) <_ ( 2 x. 1 ) ) )
63	61, 62	mp3an2 1267	. . . . . . . . . . . . . . . . 17 |- ( ( B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( B <_ 1 <-> ( 2 x. B ) <_ ( 2 x. 1 ) ) )
64	38, 60, 63	mpanr12 667	. . . . . . . . . . . . . . . 16 |- ( B e. RR -> ( B <_ 1 <-> ( 2 x. B ) <_ ( 2 x. 1 ) ) )
65	14, 64	syl 16	. . . . . . . . . . . . . . 15 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B <_ 1 <-> ( 2 x. B ) <_ ( 2 x. 1 ) ) )
66	59, 65	mpbid 202	. . . . . . . . . . . . . 14 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( 2 x. B ) <_ ( 2 x. 1 ) )
67	66	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. B ) <_ ( 2 x. 1 ) )
68		ax-1rid 9016	. . . . . . . . . . . . . 14 |- ( 2 e. RR -> ( 2 x. 1 ) = 2 )
69	38, 68	ax-mp 8	. . . . . . . . . . . . 13 |- ( 2 x. 1 ) = 2
70	67, 69	syl6breq 4211	. . . . . . . . . . . 12 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 2 x. B ) <_ 2 )
71	11	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> A e. RR )
72	61	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> 1 e. RR )
73	27	sqge0d 11505	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> 0 <_ ( B ^ 2 ) )
74	71, 36	addge01d 9570	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 0 <_ ( B ^ 2 ) <-> A <_ ( A + ( B ^ 2 ) ) ) )
75	73, 74	mpbid 202	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> A <_ ( A + ( B ^ 2 ) ) )
76	71, 36, 71	lesubaddd 9579	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( A - ( B ^ 2 ) ) <_ A <-> A <_ ( A + ( B ^ 2 ) ) ) )
77	75, 76	mpbird 224	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) <_ A )
78		simplr 732	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> A <_ 1 )
79	17, 71, 72, 77, 78	letrd 9183	. . . . . . . . . . . . . . 15 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) <_ 1 )
80		nnge1 9982	. . . . . . . . . . . . . . . . 17 |- ( 3 e. NN -> 1 <_ 3 )
81	29, 80	ax-mp 8	. . . . . . . . . . . . . . . 16 |- 1 <_ 3
82		letr 9123	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A - ( B ^ 2 ) ) e. RR /\ 1 e. RR /\ 3 e. RR ) -> ( ( ( A - ( B ^ 2 ) ) <_ 1 /\ 1 <_ 3 ) -> ( A - ( B ^ 2 ) ) <_ 3 ) )
83	61, 21, 82	mp3an23 1271	. . . . . . . . . . . . . . . . 17 |- ( ( A - ( B ^ 2 ) ) e. RR -> ( ( ( A - ( B ^ 2 ) ) <_ 1 /\ 1 <_ 3 ) -> ( A - ( B ^ 2 ) ) <_ 3 ) )
84	17, 83	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( ( A - ( B ^ 2 ) ) <_ 1 /\ 1 <_ 3 ) -> ( A - ( B ^ 2 ) ) <_ 3 ) )
85	81, 84	mpan2i 659	. . . . . . . . . . . . . . 15 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( A - ( B ^ 2 ) ) <_ 1 -> ( A - ( B ^ 2 ) ) <_ 3 ) )
86	79, 85	mpd 15	. . . . . . . . . . . . . 14 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) <_ 3 )
87		ax-1rid 9016	. . . . . . . . . . . . . . 15 |- ( 3 e. RR -> ( 3 x. 1 ) = 3 )
88	21, 87	ax-mp 8	. . . . . . . . . . . . . 14 |- ( 3 x. 1 ) = 3
89	86, 88	syl6breqr 4212	. . . . . . . . . . . . 13 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) <_ ( 3 x. 1 ) )
90		ledivmul 9839	. . . . . . . . . . . . . . . 16 |- ( ( ( A - ( B ^ 2 ) ) e. RR /\ 1 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( ( A - ( B ^ 2 ) ) / 3 ) <_ 1 <-> ( A - ( B ^ 2 ) ) <_ ( 3 x. 1 ) ) )
91	61, 90	mp3an2 1267	. . . . . . . . . . . . . . 15 |- ( ( ( A - ( B ^ 2 ) ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( ( A - ( B ^ 2 ) ) / 3 ) <_ 1 <-> ( A - ( B ^ 2 ) ) <_ ( 3 x. 1 ) ) )
92	21, 22, 91	mpanr12 667	. . . . . . . . . . . . . 14 |- ( ( A - ( B ^ 2 ) ) e. RR -> ( ( ( A - ( B ^ 2 ) ) / 3 ) <_ 1 <-> ( A - ( B ^ 2 ) ) <_ ( 3 x. 1 ) ) )
93	17, 92	syl 16	. . . . . . . . . . . . 13 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( ( A - ( B ^ 2 ) ) / 3 ) <_ 1 <-> ( A - ( B ^ 2 ) ) <_ ( 3 x. 1 ) ) )
94	89, 93	mpbird 224	. . . . . . . . . . . 12 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( A - ( B ^ 2 ) ) / 3 ) <_ 1 )
95		le2add 9466	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
96	38, 61, 95	mpanr12 667	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
97	55, 32, 96	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
98	70, 94, 97	mp2and 661	. . . . . . . . . . 11 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( 2 x. B ) + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ ( 2 + 1 ) )
99		df-3 10015	. . . . . . . . . . 11 |- 3 = ( 2 + 1 )
100	98, 99	syl6breqr 4212	. . . . . . . . . 10 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( 2 x. B ) + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ 3 )
101	55, 32	readdcld 9071	. . . . . . . . . . 11 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( 2 x. B ) + ( ( A - ( B ^ 2 ) ) / 3 ) ) e. RR )
102	21	a1i 11	. . . . . . . . . . 11 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> 3 e. RR )
103	101, 102, 25	lemul1d 10643	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
104	100, 103	mpbid 202	. . . . . . . . 9 |- ( ( ( 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 ) ) )
105	17	recnd 9070	. . . . . . . . . 10 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( A - ( B ^ 2 ) ) e. CC )
106		3cn 10028	. . . . . . . . . . 11 |- 3 e. CC
107		3ne0 10041	. . . . . . . . . . 11 |- 3 =/= 0
108		divcan2 9642	. . . . . . . . . . 11 |- ( ( ( A - ( B ^ 2 ) ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 3 x. ( ( A - ( B ^ 2 ) ) / 3 ) ) = ( A - ( B ^ 2 ) ) )
109	106, 107, 108	mp3an23 1271	. . . . . . . . . 10 |- ( ( A - ( B ^ 2 ) ) e. CC -> ( 3 x. ( ( A - ( B ^ 2 ) ) / 3 ) ) = ( A - ( B ^ 2 ) ) )
110	105, 109	syl 16	. . . . . . . . 9 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( 3 x. ( ( A - ( B ^ 2 ) ) / 3 ) ) = ( A - ( B ^ 2 ) ) )
111	104, 110	breqtrd 4196	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( ( 2 x. B ) + ( ( A - ( B ^ 2 ) ) / 3 ) ) x. ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ ( A - ( B ^ 2 ) ) )
112	58, 111	eqbrtrd 4192	. . . . . . 7 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) + ( ( ( A - ( B ^ 2 ) ) / 3 ) ^ 2 ) ) <_ ( A - ( B ^ 2 ) ) )
113	41, 43	readdcld 9071	. . . . . . . 8 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) + ( ( ( A - ( B ^ 2 ) ) / 3 ) ^ 2 ) ) e. RR )
114	36, 113, 71	leaddsub2d 9584	. . . . . . 7 |- ( ( ( 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 ) ) ) )
115	112, 114	mpbird 224	. . . . . 6 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( B ^ 2 ) + ( ( 2 x. ( B x. ( ( A - ( B ^ 2 ) ) / 3 ) ) ) + ( ( ( A - ( B ^ 2 ) ) / 3 ) ^ 2 ) ) ) <_ A )
116	46, 115	eqbrtrd 4192	. . . . 5 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) ^ 2 ) <_ A )
117		oveq1 6047	. . . . . . 7 |- ( y = ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) -> ( y ^ 2 ) = ( ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) ^ 2 ) )
118	117	breq1d 4182	. . . . . 6 |- ( y = ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) -> ( ( y ^ 2 ) <_ A <-> ( ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) ^ 2 ) <_ A ) )
119		oveq1 6047	. . . . . . . . 9 |- ( x = y -> ( x ^ 2 ) = ( y ^ 2 ) )
120	119	breq1d 4182	. . . . . . . 8 |- ( x = y -> ( ( x ^ 2 ) <_ A <-> ( y ^ 2 ) <_ A ) )
121	120	cbvrabv 2915	. . . . . . 7 |- { x e. RR+ | ( x ^ 2 ) <_ A } = { y e. RR+ | ( y ^ 2 ) <_ A }
122	1, 121	eqtri 2424	. . . . . 6 |- S = { y e. RR+ | ( y ^ 2 ) <_ A }
123	118, 122	elrab2 3054	. . . . 5 |- ( ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) e. S <-> ( ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) e. RR+ /\ ( ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) ^ 2 ) <_ A ) )
124	26, 116, 123	sylanbrc 646	. . . 4 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) e. S )
125		suprub 9925	. . . . 5 |- ( ( ( 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 , < ) )
126	125, 2	syl6breqr 4212	. . . 4 |- ( ( ( 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 )
127	6, 124, 126	syl2anc 643	. . 3 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ B )
128	25	rpgt0d 10607	. . . 4 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> 0 < ( ( A - ( B ^ 2 ) ) / 3 ) )
129	31, 14	ltaddposd 9566	. . . . . 6 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( 0 < ( ( A - ( B ^ 2 ) ) / 3 ) <-> B < ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) ) )
130	14, 31	readdcld 9071	. . . . . . 7 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) e. RR )
131	14, 130	ltnled 9176	. . . . . 6 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B < ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) <-> -. ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ B ) )
132	129, 131	bitrd 245	. . . . 5 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( 0 < ( ( A - ( B ^ 2 ) ) / 3 ) <-> -. ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ B ) )
133	132	biimpa 471	. . . 4 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ 0 < ( ( A - ( B ^ 2 ) ) / 3 ) ) -> -. ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ B )
134	128, 133	syldan 457	. . 3 |- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( B ^ 2 ) < A ) -> -. ( B + ( ( A - ( B ^ 2 ) ) / 3 ) ) <_ B )
135	127, 134	pm2.65da 560	. 2 |- ( ( A e. RR+ /\ A <_ 1 ) -> -. ( B ^ 2 ) < A )
136	15, 11	eqleltd 9173	. 2 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( B ^ 2 ) = A <-> ( ( B ^ 2 ) <_ A /\ -. ( B ^ 2 ) < A ) ) )
137	4, 135, 136	mpbir2and 889	1 |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   {cab 2390   =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   C_ wss 3280   (/)c0 3588   class class class wbr 4172  (class class class)co 6040   supcsup 7403   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   NNcn 9956   2c2 10005   3c3 10006   RR+crp 10568   ^cexp 11337

This theorem is referenced by:  01sqrex  12010

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-seq 11279  df-exp 11338