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 ) } ) )