Metamath Proof Explorer


Theorem predfz

Description: Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013) (Proof shortened by Mario Carneiro, 3-May-2015)

Ref Expression
Assertion predfz KMNPred<MNK=MK1

Proof

Step Hyp Ref Expression
1 elfzelz xMNx
2 elfzelz KMNK
3 zltlem1 xKx<KxK1
4 1 2 3 syl2anr KMNxMNx<KxK1
5 elfzuz xMNxM
6 peano2zm KK1
7 2 6 syl KMNK1
8 elfz5 xMK1xMK1xK1
9 5 7 8 syl2anr KMNxMNxMK1xK1
10 4 9 bitr4d KMNxMNx<KxMK1
11 10 pm5.32da KMNxMNx<KxMNxMK1
12 vex xV
13 12 elpred KMNxPred<MNKxMNx<K
14 elfzuz3 KMNNK
15 2 zcnd KMNK
16 ax-1cn 1
17 npcan K1K-1+1=K
18 15 16 17 sylancl KMNK-1+1=K
19 18 fveq2d KMNK-1+1=K
20 14 19 eleqtrrd KMNNK-1+1
21 peano2uzr K1NK-1+1NK1
22 7 20 21 syl2anc KMNNK1
23 fzss2 NK1MK1MN
24 22 23 syl KMNMK1MN
25 24 sseld KMNxMK1xMN
26 25 pm4.71rd KMNxMK1xMNxMK1
27 11 13 26 3bitr4d KMNxPred<MNKxMK1
28 27 eqrdv KMNPred<MNK=MK1