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 ) ... 𝑁 ) )