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