Metamath Proof Explorer

Theorem nn0nndivcl

Description: Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion nn0nndivcl 
|- ( ( K e. NN0 /\ L e. NN ) -> ( K / L ) e. RR )

Proof

Step Hyp Ref Expression
1 elnnne0 
 |-  ( L e. NN <-> ( L e. NN0 /\ L =/= 0 ) )
2 nn0re 
 |-  ( K e. NN0 -> K e. RR )
3 2 adantr 
 |-  ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> K e. RR )
4 nn0re 
 |-  ( L e. NN0 -> L e. RR )
5 4 ad2antrl 
 |-  ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> L e. RR )
6 simprr 
 |-  ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> L =/= 0 )
7 3 5 6 3jca 
 |-  ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> ( K e. RR /\ L e. RR /\ L =/= 0 ) )
8 1 7 sylan2b 
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( K e. RR /\ L e. RR /\ L =/= 0 ) )
9 redivcl 
 |-  ( ( K e. RR /\ L e. RR /\ L =/= 0 ) -> ( K / L ) e. RR )
10 8 9 syl 
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( K / L ) e. RR )