Theorem fzp1disj

Description: ( M ... ( N + 1 ) ) is the disjoint union of ( M ... N ) with { ( N + 1 ) } . (Contributed by Mario Carneiro, 7-Mar-2014)

	Ref	Expression
Assertion	fzp1disj	⊢ ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅

Proof

Step	Hyp	Ref	Expression
1		elfzle2	⊢ ( ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑁 + 1 ) ≤ 𝑁 )
2		elfzel2	⊢ ( ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
3	2	zred	⊢ ( ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℝ )
4		ltp1	⊢ ( 𝑁 ∈ ℝ → 𝑁 < ( 𝑁 + 1 ) )
5		peano2re	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
6		ltnle	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ) → ( 𝑁 < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ 𝑁 ) )
7	5 6	mpdan	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ 𝑁 ) )
8	4 7	mpbid	⊢ ( 𝑁 ∈ ℝ → ¬ ( 𝑁 + 1 ) ≤ 𝑁 )
9	3 8	syl	⊢ ( ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ¬ ( 𝑁 + 1 ) ≤ 𝑁 )
10	1 9	pm2.65i	⊢ ¬ ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 )
11		disjsn	⊢ ( ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ ↔ ¬ ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
12	10 11	mpbir	⊢ ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅