Metamath Proof Explorer


Theorem ltdivgt1

Description: Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ltdivgt1.1
|- ( ph -> A e. RR+ )
ltdivgt1.2
|- ( ph -> B e. RR+ )
Assertion ltdivgt1
|- ( ph -> ( 1 < B <-> ( A / B ) < A ) )

Proof

Step Hyp Ref Expression
1 ltdivgt1.1
 |-  ( ph -> A e. RR+ )
2 ltdivgt1.2
 |-  ( ph -> B e. RR+ )
3 1rp
 |-  1 e. RR+
4 3 a1i
 |-  ( ph -> 1 e. RR+ )
5 4 2 1 ltdiv2d
 |-  ( ph -> ( 1 < B <-> ( A / B ) < ( A / 1 ) ) )
6 1 rpcnd
 |-  ( ph -> A e. CC )
7 6 div1d
 |-  ( ph -> ( A / 1 ) = A )
8 7 breq2d
 |-  ( ph -> ( ( A / B ) < ( A / 1 ) <-> ( A / B ) < A ) )
9 5 8 bitrd
 |-  ( ph -> ( 1 < B <-> ( A / B ) < A ) )