This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzpred

Description: Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

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

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
2 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
4 1 2 3 3syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
5 fzsplit2 ⊢ ( ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
6 4 5 mpancom ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
7 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
8 1 7 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
9 8 uneq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
10 6 9 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )