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

Metamath Proof Explorer

Theorem fzpreddisj

Description: A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019)

Ref Expression
Assertion fzpreddisj ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 incom ⊢ ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ { 𝑀 } )
2 0lt1 ⊢ 0 < 1
3 0re ⊢ 0 ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 3 4 ltnlei ⊢ ( 0 < 1 ↔ ¬ 1 ≤ 0 )
6 2 5 mpbi ⊢ ¬ 1 ≤ 0
7 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
8 7 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ )
9 leaddle0 ⊢ ( ( 𝑀 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑀 + 1 ) ≤ 𝑀 ↔ 1 ≤ 0 ) )
10 8 4 9 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + 1 ) ≤ 𝑀 ↔ 1 ≤ 0 ) )
11 6 10 mtbiri ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ ( 𝑀 + 1 ) ≤ 𝑀 )
12 11 intnanrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ ( ( 𝑀 + 1 ) ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) )
13 12 intnand ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
14 elfz2 ⊢ ( 𝑀 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
15 13 14 sylnibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
16 disjsn ⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
17 15 16 sylibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ { 𝑀 } ) = ∅ )
18 1 17 eqtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )