Theorem fzodisjsn

Description: A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021)

	Ref	Expression
Assertion	fzodisjsn	⊢ ( ( 𝐴 ..^ 𝐵 ) ∩ { 𝐵 } ) = ∅

Proof

Step	Hyp	Ref	Expression
1		disj1	⊢ ( ( ( 𝐴 ..^ 𝐵 ) ∩ { 𝐵 } ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝑥 ∈ { 𝐵 } ) )
2		elfzoelz	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ∈ ℤ )
3	2	zred	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ∈ ℝ )
4		elfzolt2	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 < 𝐵 )
5	3 4	ltned	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ≠ 𝐵 )
6	5	neneqd	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝑥 = 𝐵 )
7		elsni	⊢ ( 𝑥 ∈ { 𝐵 } → 𝑥 = 𝐵 )
8	6 7	nsyl	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝑥 ∈ { 𝐵 } )
9	1 8	mpgbir	⊢ ( ( 𝐴 ..^ 𝐵 ) ∩ { 𝐵 } ) = ∅