Metamath Proof Explorer


Theorem nn0ge0div

Description: Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion nn0ge0div
|- ( ( K e. NN0 /\ L e. NN ) -> 0 <_ ( K / L ) )

Proof

Step Hyp Ref Expression
1 nn0ge0
 |-  ( K e. NN0 -> 0 <_ K )
2 1 adantr
 |-  ( ( K e. NN0 /\ L e. NN ) -> 0 <_ K )
3 elnnz
 |-  ( L e. NN <-> ( L e. ZZ /\ 0 < L ) )
4 nn0re
 |-  ( K e. NN0 -> K e. RR )
5 4 adantr
 |-  ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> K e. RR )
6 zre
 |-  ( L e. ZZ -> L e. RR )
7 6 ad2antrl
 |-  ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> L e. RR )
8 simprr
 |-  ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> 0 < L )
9 5 7 8 3jca
 |-  ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> ( K e. RR /\ L e. RR /\ 0 < L ) )
10 3 9 sylan2b
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( K e. RR /\ L e. RR /\ 0 < L ) )
11 ge0div
 |-  ( ( K e. RR /\ L e. RR /\ 0 < L ) -> ( 0 <_ K <-> 0 <_ ( K / L ) ) )
12 10 11 syl
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( 0 <_ K <-> 0 <_ ( K / L ) ) )
13 2 12 mpbid
 |-  ( ( K e. NN0 /\ L e. NN ) -> 0 <_ ( K / L ) )