Metamath Proof Explorer


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+BAB1BA

Proof

Step Hyp Ref Expression
1 rpgecl A+BABB+
2 rpcn B+B
3 rpne0 B+B0
4 2 3 dividd B+BB=1
5 4 eqcomd B+1=BB
6 1 5 syl A+BAB1=BB
7 simp3 A+BABAB
8 simp1 A+BABA+
9 8 1 1 lediv2d A+BABABBBBA
10 7 9 mpbid A+BABBBBA
11 6 10 eqbrtrd A+BAB1BA