Metamath Proof Explorer


Theorem divge0

Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999)

Ref Expression
Assertion divge0 A 0 A B 0 < B 0 A B

Proof

Step Hyp Ref Expression
1 ge0div A B 0 < B 0 A 0 A B
2 1 biimpd A B 0 < B 0 A 0 A B
3 2 3exp A B 0 < B 0 A 0 A B
4 3 com34 A B 0 A 0 < B 0 A B
5 4 com23 A 0 A B 0 < B 0 A B
6 5 imp43 A 0 A B 0 < B 0 A B