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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpgecl | |
|
2 | rpcn | |
|
3 | rpne0 | |
|
4 | 2 3 | dividd | |
5 | 4 | eqcomd | |
6 | 1 5 | syl | |
7 | simp3 | |
|
8 | simp1 | |
|
9 | 8 1 1 | lediv2d | |
10 | 7 9 | mpbid | |
11 | 6 10 | eqbrtrd | |