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