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 ) ) )