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