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