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 K M N Pred < M N K = M K 1

Proof

Step Hyp Ref Expression
1 elfzelz x M N x
2 elfzelz K M N K
3 zltlem1 x K x < K x K 1
4 1 2 3 syl2anr K M N x M N x < K x K 1
5 elfzuz x M N x M
6 peano2zm K K 1
7 2 6 syl K M N K 1
8 elfz5 x M K 1 x M K 1 x K 1
9 5 7 8 syl2anr K M N x M N x M K 1 x K 1
10 4 9 bitr4d K M N x M N x < K x M K 1
11 10 pm5.32da K M N x M N x < K x M N x M K 1
12 vex x V
13 12 elpred K M N x Pred < M N K x M N x < K
14 elfzuz3 K M N N K
15 2 zcnd K M N K
16 ax-1cn 1
17 npcan K 1 K - 1 + 1 = K
18 15 16 17 sylancl K M N K - 1 + 1 = K
19 18 fveq2d K M N K - 1 + 1 = K
20 14 19 eleqtrrd K M N N K - 1 + 1
21 peano2uzr K 1 N K - 1 + 1 N K 1
22 7 20 21 syl2anc K M N N K 1
23 fzss2 N K 1 M K 1 M N
24 22 23 syl K M N M K 1 M N
25 24 sseld K M N x M K 1 x M N
26 25 pm4.71rd K M N x M K 1 x M N x M K 1
27 11 13 26 3bitr4d K M N x Pred < M N K x M K 1
28 27 eqrdv K M N Pred < M N K = M K 1