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 )