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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnnne0 | |
|
2 | nn0re | |
|
3 | 2 | adantr | |
4 | nn0re | |
|
5 | 4 | ad2antrl | |
6 | simprr | |
|
7 | 3 5 6 | 3jca | |
8 | 1 7 | sylan2b | |
9 | redivcl | |
|
10 | 8 9 | syl | |