Theorem 01sqrexlem4

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

	Ref	Expression
Hypotheses	01sqrexlem1.1	|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
	01sqrexlem1.2	|- B = sup ( S , RR , < )
Assertion	01sqrexlem4	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B e. RR+ /\ B <_ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
2		01sqrexlem1.2	|- B = sup ( S , RR , < )
3	1 2	01sqrexlem3	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) )
4		suprcl	|- ( ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) -> sup ( S , RR , < ) e. RR )
5	3 4	syl	|- ( ( A e. RR+ /\ A <_ 1 ) -> sup ( S , RR , < ) e. RR )
6	2 5	eqeltrid	|- ( ( A e. RR+ /\ A <_ 1 ) -> B e. RR )
7		rpgt0	|- ( A e. RR+ -> 0 < A )
8	7	adantr	|- ( ( A e. RR+ /\ A <_ 1 ) -> 0 < A )
9	1 2	01sqrexlem2	|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. S )
10		suprub	|- ( ( ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) /\ A e. S ) -> A <_ sup ( S , RR , < ) )
11	3 9 10	syl2anc	|- ( ( A e. RR+ /\ A <_ 1 ) -> A <_ sup ( S , RR , < ) )
12	11 2	breqtrrdi	|- ( ( A e. RR+ /\ A <_ 1 ) -> A <_ B )
13		0re	|- 0 e. RR
14		rpre	|- ( A e. RR+ -> A e. RR )
15		ltletr	|- ( ( 0 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) )
16	13 14 6 15	mp3an2ani	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) )
17	8 12 16	mp2and	|- ( ( A e. RR+ /\ A <_ 1 ) -> 0 < B )
18	6 17	elrpd	|- ( ( A e. RR+ /\ A <_ 1 ) -> B e. RR+ )
19	1 2	01sqrexlem1	|- ( ( A e. RR+ /\ A <_ 1 ) -> A. z e. S z <_ 1 )
20		1re	|- 1 e. RR
21		suprleub	|- ( ( ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) /\ 1 e. RR ) -> ( sup ( S , RR , < ) <_ 1 <-> A. z e. S z <_ 1 ) )
22	3 20 21	sylancl	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( sup ( S , RR , < ) <_ 1 <-> A. z e. S z <_ 1 ) )
23	19 22	mpbird	|- ( ( A e. RR+ /\ A <_ 1 ) -> sup ( S , RR , < ) <_ 1 )
24	2 23	eqbrtrid	|- ( ( A e. RR+ /\ A <_ 1 ) -> B <_ 1 )
25	18 24	jca	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B e. RR+ /\ B <_ 1 ) )