Metamath Proof Explorer


Theorem ge0divd

Description: Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpgecld.1 φA
rpgecld.2 φB+
Assertion ge0divd φ0A0AB

Proof

Step Hyp Ref Expression
1 rpgecld.1 φA
2 rpgecld.2 φB+
3 2 rpred φB
4 2 rpgt0d φ0<B
5 ge0div AB0<B0A0AB
6 1 3 4 5 syl3anc φ0A0AB