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 ) )