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	|- ( ( A ..^ B ) i^i { B } ) = (/)

Proof

Step	Hyp	Ref	Expression
1		disj1	|- ( ( ( A ..^ B ) i^i { B } ) = (/) <-> A. x ( x e. ( A ..^ B ) -> -. x e. { B } ) )
2		elfzoelz	|- ( x e. ( A ..^ B ) -> x e. ZZ )
3	2	zred	|- ( x e. ( A ..^ B ) -> x e. RR )
4		elfzolt2	|- ( x e. ( A ..^ B ) -> x < B )
5	3 4	ltned	|- ( x e. ( A ..^ B ) -> x =/= B )
6	5	neneqd	|- ( x e. ( A ..^ B ) -> -. x = B )
7		elsni	|- ( x e. { B } -> x = B )
8	6 7	nsyl	|- ( x e. ( A ..^ B ) -> -. x e. { B } )
9	1 8	mpgbir	|- ( ( A ..^ B ) i^i { B } ) = (/)