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