Metamath Proof Explorer

Theorem preduz

Description: The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Assertion preduz 
|- ( N e. ( ZZ>= ` M ) -> Pred ( < , ( ZZ>= ` M ) , N ) = ( M ... ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 elpred 
 |-  ( N e. ( ZZ>= ` M ) -> ( x e. Pred ( < , ( ZZ>= ` M ) , N ) <-> ( x e. ( ZZ>= ` M ) /\ x < N ) ) )
3 eluzelz 
 |-  ( x e. ( ZZ>= ` M ) -> x e. ZZ )
4 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
5 zltlem1 
 |-  ( ( x e. ZZ /\ N e. ZZ ) -> ( x < N <-> x <_ ( N - 1 ) ) )
6 3 4 5 syl2anr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( ZZ>= ` M ) ) -> ( x < N <-> x <_ ( N - 1 ) ) )
7 6 pm5.32da 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( x e. ( ZZ>= ` M ) /\ x < N ) <-> ( x e. ( ZZ>= ` M ) /\ x <_ ( N - 1 ) ) ) )
8 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
9 eluz1 
 |-  ( M e. ZZ -> ( x e. ( ZZ>= ` M ) <-> ( x e. ZZ /\ M <_ x ) ) )
10 8 9 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( x e. ( ZZ>= ` M ) <-> ( x e. ZZ /\ M <_ x ) ) )
11 10 anbi1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( x e. ( ZZ>= ` M ) /\ x <_ ( N - 1 ) ) <-> ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) )
12 7 11 bitrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( x e. ( ZZ>= ` M ) /\ x < N ) <-> ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) )
13 2 12 bitrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( x e. Pred ( < , ( ZZ>= ` M ) , N ) <-> ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) )
14 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
15 4 14 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - 1 ) e. ZZ )
16 8 15 jca 
 |-  ( N e. ( ZZ>= ` M ) -> ( M e. ZZ /\ ( N - 1 ) e. ZZ ) )
17 16 biantrurd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) ) )
18 13 17 bitrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( x e. Pred ( < , ( ZZ>= ` M ) , N ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) ) )
19 elfz2 
 |-  ( x e. ( M ... ( N - 1 ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ x e. ZZ ) /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) )
20 df-3an 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ x e. ZZ ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ x e. ZZ ) )
21 20 anbi1i 
 |-  ( ( ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ x e. ZZ ) /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) <-> ( ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ x e. ZZ ) /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) )
22 anass 
 |-  ( ( ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ x e. ZZ ) /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( x e. ZZ /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) ) )
23 anass 
 |-  ( ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) <-> ( x e. ZZ /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) )
24 23 anbi2i 
 |-  ( ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( x e. ZZ /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) ) )
25 22 24 bitr4i 
 |-  ( ( ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ x e. ZZ ) /\ ( M <_ x /\ x <_ ( N - 1 ) ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) )
26 19 21 25 3bitri 
 |-  ( x e. ( M ... ( N - 1 ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( ( x e. ZZ /\ M <_ x ) /\ x <_ ( N - 1 ) ) ) )
27 18 26 bitr4di 
 |-  ( N e. ( ZZ>= ` M ) -> ( x e. Pred ( < , ( ZZ>= ` M ) , N ) <-> x e. ( M ... ( N - 1 ) ) ) )
28 27 eqrdv 
 |-  ( N e. ( ZZ>= ` M ) -> Pred ( < , ( ZZ>= ` M ) , N ) = ( M ... ( N - 1 ) ) )