Metamath Proof Explorer


Theorem difelfzle

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 K0NM0NKMMK0N

Proof

Step Hyp Ref Expression
1 elfznn0 K0NK0
2 elfznn0 M0NM0
3 nn0z M0M
4 nn0z K0K
5 zsubcl MKMK
6 3 4 5 syl2anr K0M0MK
7 6 adantr K0M0KMMK
8 nn0re M0M
9 nn0re K0K
10 subge0 MK0MKKM
11 8 9 10 syl2anr K0M00MKKM
12 11 biimpar K0M0KM0MK
13 7 12 jca K0M0KMMK0MK
14 13 exp31 K0M0KMMK0MK
15 1 2 14 syl2im K0NM0NKMMK0MK
16 15 3imp K0NM0NKMMK0MK
17 elnn0z MK0MK0MK
18 16 17 sylibr K0NM0NKMMK0
19 elfz3nn0 K0NN0
20 19 3ad2ant1 K0NM0NKMN0
21 elfz2nn0 M0NM0N0MN
22 8 3ad2ant1 M0N0MNM
23 resubcl MKMK
24 22 9 23 syl2an M0N0MNK0MK
25 22 adantr M0N0MNK0M
26 nn0re N0N
27 26 3ad2ant2 M0N0MNN
28 27 adantr M0N0MNK0N
29 nn0ge0 K00K
30 29 adantl M0N0MNK00K
31 subge02 MK0KMKM
32 22 9 31 syl2an M0N0MNK00KMKM
33 30 32 mpbid M0N0MNK0MKM
34 simpl3 M0N0MNK0MN
35 24 25 28 33 34 letrd M0N0MNK0MKN
36 35 ex M0N0MNK0MKN
37 21 36 sylbi M0NK0MKN
38 1 37 syl5com K0NM0NMKN
39 38 a1dd K0NM0NKMMKN
40 39 3imp K0NM0NKMMKN
41 elfz2nn0 MK0NMK0N0MKN
42 18 20 40 41 syl3anbrc K0NM0NKMMK0N