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

Metamath Proof Explorer

Theorem fzdifsuc

Description: Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 fzsuc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
2 1 difeq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... ( 𝑁 + 1 ) ) ∖ { ( 𝑁 + 1 ) } ) = ( ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ∖ { ( 𝑁 + 1 ) } ) )
3 uncom ⊢ ( { ( 𝑁 + 1 ) } ∪ ( 𝑀 ... 𝑁 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } )
4 ssun2 ⊢ { ( 𝑁 + 1 ) } ⊆ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } )
5 incom ⊢ ( { ( 𝑁 + 1 ) } ∩ ( 𝑀 ... 𝑁 ) ) = ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } )
6 fzp1disj ⊢ ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
7 5 6 eqtri ⊢ ( { ( 𝑁 + 1 ) } ∩ ( 𝑀 ... 𝑁 ) ) = ∅
8 7 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( { ( 𝑁 + 1 ) } ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )
9 uneqdifeq ⊢ ( ( { ( 𝑁 + 1 ) } ⊆ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ∧ ( { ( 𝑁 + 1 ) } ∩ ( 𝑀 ... 𝑁 ) ) = ∅ ) → ( ( { ( 𝑁 + 1 ) } ∪ ( 𝑀 ... 𝑁 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ↔ ( ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ∖ { ( 𝑁 + 1 ) } ) = ( 𝑀 ... 𝑁 ) ) )
10 4 8 9 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( { ( 𝑁 + 1 ) } ∪ ( 𝑀 ... 𝑁 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ↔ ( ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ∖ { ( 𝑁 + 1 ) } ) = ( 𝑀 ... 𝑁 ) ) )
11 3 10 mpbii ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ∖ { ( 𝑁 + 1 ) } ) = ( 𝑀 ... 𝑁 ) )
12 2 11 eqtr2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 + 1 ) ) ∖ { ( 𝑁 + 1 ) } ) )