Metamath Proof Explorer

Theorem rpgecl

Description: A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Assertion rpgecl 
|- ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> B e. RR+ )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> B e. RR )
2 0red 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 0 e. RR )
3 rpre 
 |-  ( A e. RR+ -> A e. RR )
4 3 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> A e. RR )
5 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
6 5 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 0 < A )
7 simp3 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> A <_ B )
8 2 4 1 6 7 ltletrd 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 0 < B )
9 elrp 
 |-  ( B e. RR+ <-> ( B e. RR /\ 0 < B ) )
10 1 8 9 sylanbrc 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> B e. RR+ )