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

Metamath Proof Explorer

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