Metamath Proof Explorer


Theorem fzdifsuc2

Description: Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc , but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion fzdifsuc2
|- ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> N = ( M - 1 ) )
2 zre
 |-  ( M e. ZZ -> M e. RR )
3 2 ad2antlr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M e. RR )
4 3 ltm1d
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M - 1 ) < M )
5 1 4 eqbrtrd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> N < M )
6 simplr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M e. ZZ )
7 eluzelz
 |-  ( N e. ( ZZ>= ` ( M - 1 ) ) -> N e. ZZ )
8 7 ad2antrr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> N e. ZZ )
9 fzn
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) )
10 6 8 9 syl2anc
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( N < M <-> ( M ... N ) = (/) ) )
11 5 10 mpbid
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... N ) = (/) )
12 difid
 |-  ( { M } \ { M } ) = (/)
13 12 a1i
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( { M } \ { M } ) = (/) )
14 13 eqcomd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> (/) = ( { M } \ { M } ) )
15 oveq1
 |-  ( N = ( M - 1 ) -> ( N + 1 ) = ( ( M - 1 ) + 1 ) )
16 15 adantl
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( N + 1 ) = ( ( M - 1 ) + 1 ) )
17 2 recnd
 |-  ( M e. ZZ -> M e. CC )
18 17 ad2antlr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M e. CC )
19 1cnd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> 1 e. CC )
20 18 19 npcand
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( ( M - 1 ) + 1 ) = M )
21 16 20 eqtrd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( N + 1 ) = M )
22 21 oveq2d
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... ( N + 1 ) ) = ( M ... M ) )
23 fzsn
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
24 23 ad2antlr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... M ) = { M } )
25 22 24 eqtr2d
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> { M } = ( M ... ( N + 1 ) ) )
26 21 eqcomd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M = ( N + 1 ) )
27 26 sneqd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> { M } = { ( N + 1 ) } )
28 25 27 difeq12d
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( { M } \ { M } ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
29 11 14 28 3eqtrd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
30 simplr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> M e. ZZ )
31 7 ad2antrr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N e. ZZ )
32 2 ad2antlr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> M e. RR )
33 1red
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> 1 e. RR )
34 32 33 resubcld
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M - 1 ) e. RR )
35 31 zred
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N e. RR )
36 eluzle
 |-  ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( M - 1 ) <_ N )
37 36 ad2antrr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M - 1 ) <_ N )
38 neqne
 |-  ( -. N = ( M - 1 ) -> N =/= ( M - 1 ) )
39 38 adantl
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N =/= ( M - 1 ) )
40 34 35 37 39 leneltd
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M - 1 ) < N )
41 zlem1lt
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M - 1 ) < N ) )
42 30 31 41 syl2anc
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M <_ N <-> ( M - 1 ) < N ) )
43 40 42 mpbird
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> M <_ N )
44 30 31 43 3jca
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
45 eluz2
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
46 44 45 sylibr
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N e. ( ZZ>= ` M ) )
47 fzdifsuc
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
48 46 47 syl
 |-  ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
49 29 48 pm2.61dan
 |-  ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
50 eluzel2
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
51 50 con3i
 |-  ( -. M e. ZZ -> -. N e. ( ZZ>= ` M ) )
52 fzn0
 |-  ( ( M ... N ) =/= (/) <-> N e. ( ZZ>= ` M ) )
53 51 52 sylnibr
 |-  ( -. M e. ZZ -> -. ( M ... N ) =/= (/) )
54 nne
 |-  ( -. ( M ... N ) =/= (/) <-> ( M ... N ) = (/) )
55 53 54 sylib
 |-  ( -. M e. ZZ -> ( M ... N ) = (/) )
56 eluzel2
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
57 56 con3i
 |-  ( -. M e. ZZ -> -. ( N + 1 ) e. ( ZZ>= ` M ) )
58 fzn0
 |-  ( ( M ... ( N + 1 ) ) =/= (/) <-> ( N + 1 ) e. ( ZZ>= ` M ) )
59 57 58 sylnibr
 |-  ( -. M e. ZZ -> -. ( M ... ( N + 1 ) ) =/= (/) )
60 nne
 |-  ( -. ( M ... ( N + 1 ) ) =/= (/) <-> ( M ... ( N + 1 ) ) = (/) )
61 59 60 sylib
 |-  ( -. M e. ZZ -> ( M ... ( N + 1 ) ) = (/) )
62 61 difeq1d
 |-  ( -. M e. ZZ -> ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) = ( (/) \ { ( N + 1 ) } ) )
63 0dif
 |-  ( (/) \ { ( N + 1 ) } ) = (/)
64 63 a1i
 |-  ( -. M e. ZZ -> ( (/) \ { ( N + 1 ) } ) = (/) )
65 62 64 eqtr2d
 |-  ( -. M e. ZZ -> (/) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
66 55 65 eqtrd
 |-  ( -. M e. ZZ -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
67 66 adantl
 |-  ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ -. M e. ZZ ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
68 49 67 pm2.61dan
 |-  ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )