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 ) ... 𝑁 ) ) = ∅ )