Description: The difference of two integers from a finite set of sequential nonnegative integers is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | difelfzle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfznn0 | |
|
2 | elfznn0 | |
|
3 | nn0z | |
|
4 | nn0z | |
|
5 | zsubcl | |
|
6 | 3 4 5 | syl2anr | |
7 | 6 | adantr | |
8 | nn0re | |
|
9 | nn0re | |
|
10 | subge0 | |
|
11 | 8 9 10 | syl2anr | |
12 | 11 | biimpar | |
13 | 7 12 | jca | |
14 | 13 | exp31 | |
15 | 1 2 14 | syl2im | |
16 | 15 | 3imp | |
17 | elnn0z | |
|
18 | 16 17 | sylibr | |
19 | elfz3nn0 | |
|
20 | 19 | 3ad2ant1 | |
21 | elfz2nn0 | |
|
22 | 8 | 3ad2ant1 | |
23 | resubcl | |
|
24 | 22 9 23 | syl2an | |
25 | 22 | adantr | |
26 | nn0re | |
|
27 | 26 | 3ad2ant2 | |
28 | 27 | adantr | |
29 | nn0ge0 | |
|
30 | 29 | adantl | |
31 | subge02 | |
|
32 | 22 9 31 | syl2an | |
33 | 30 32 | mpbid | |
34 | simpl3 | |
|
35 | 24 25 28 33 34 | letrd | |
36 | 35 | ex | |
37 | 21 36 | sylbi | |
38 | 1 37 | syl5com | |
39 | 38 | a1dd | |
40 | 39 | 3imp | |
41 | elfz2nn0 | |
|
42 | 18 20 40 41 | syl3anbrc | |