Metamath Proof Explorer

Theorem fzdif1

Description: Split the first element of a finite set of sequential integers. More generic than fzpred . Analogous to fzdif2 . (Contributed by AV, 12-Sep-2025)

Ref Expression
Assertion fzdif1 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝑥 ∈ ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) )
2 elsng ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ { 𝑀 } ↔ 𝑥 = 𝑀 ) )
3 2 necon3bbid ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ¬ 𝑥 ∈ { 𝑀 } ↔ 𝑥 ≠ 𝑀 ) )
4 fzne1 ⊢ ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ≠ 𝑀 ) → 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
5 3 4 sylbida ⊢ ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) → 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
6 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
7 6 uzidd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 fzss1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
10 7 8 9 3syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
11 10 sselda ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
12 elfz2 ⊢ ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) )
13 6 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ )
14 13 adantl ⊢ ( ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ )
15 simp3 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
16 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑀 < 𝑥 ↔ ( 𝑀 + 1 ) ≤ 𝑥 ) )
17 6 15 16 syl2anr ⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 < 𝑥 ↔ ( 𝑀 + 1 ) ≤ 𝑥 ) )
18 17 biimprd ⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 + 1 ) ≤ 𝑥 → 𝑀 < 𝑥 ) )
19 18 a1d ⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ≤ 𝑁 → ( ( 𝑀 + 1 ) ≤ 𝑥 → 𝑀 < 𝑥 ) ) )
20 19 ex ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ≤ 𝑁 → ( ( 𝑀 + 1 ) ≤ 𝑥 → 𝑀 < 𝑥 ) ) ) )
21 20 com24 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑥 → ( 𝑥 ≤ 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 < 𝑥 ) ) ) )
22 21 imp42 ⊢ ( ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 < 𝑥 )
23 14 22 gtned ⊢ ( ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑥 ≠ 𝑀 )
24 23 ex ⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑥 ≠ 𝑀 ) )
25 12 24 sylbi ⊢ ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑥 ≠ 𝑀 ) )
26 25 impcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑥 ≠ 𝑀 )
27 nelsn ⊢ ( 𝑥 ≠ 𝑀 → ¬ 𝑥 ∈ { 𝑀 } )
28 26 27 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ¬ 𝑥 ∈ { 𝑀 } )
29 11 28 jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) )
30 29 ex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) ) )
31 5 30 impbid2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) ↔ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
32 1 31 bitrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) ↔ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
33 32 eqrdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )