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 K0LKL

Proof

Step Hyp Ref Expression
1 elnnne0 LL0L0
2 nn0re K0K
3 2 adantr K0L0L0K
4 nn0re L0L
5 4 ad2antrl K0L0L0L
6 simprr K0L0L0L0
7 3 5 6 3jca K0L0L0KLL0
8 1 7 sylan2b K0LKLL0
9 redivcl KLL0KL
10 8 9 syl K0LKL