This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divge1

Description: The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 rpgecl 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> B e. RR+ )
2 rpcn 
 |-  ( B e. RR+ -> B e. CC )
3 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
4 2 3 dividd 
 |-  ( B e. RR+ -> ( B / B ) = 1 )
5 4 eqcomd 
 |-  ( B e. RR+ -> 1 = ( B / B ) )
6 1 5 syl 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 1 = ( B / B ) )
7 simp3 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> A <_ B )
8 simp1 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> A e. RR+ )
9 8 1 1 lediv2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> ( A <_ B <-> ( B / B ) <_ ( B / A ) ) )
10 7 9 mpbid 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> ( B / B ) <_ ( B / A ) )
11 6 10 eqbrtrd 
 |-  ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 1 <_ ( B / A ) )