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