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 ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 + 1 ) ) ∖ { ( 𝑁 + 1 ) } ) )

Proof

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