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 e. ( M ... N ) -> Pred ( < , ( M ... N ) , K ) = ( M ... ( K - 1 ) ) )

Proof

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