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+ ) |