Theorem fzouzdisj

Description: A half-open integer range does not overlap the upper integer range starting at the endpoint of the first range. (Contributed by Mario Carneiro, 21-Sep-2016)

	Ref	Expression
Assertion	fzouzdisj	|- ( ( A ..^ B ) i^i ( ZZ>= ` B ) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	|- ( x e. ( A ..^ B ) -> x < B )
2	1	adantr	|- ( ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) -> x < B )
3		eluzel2	|- ( x e. ( ZZ>= ` B ) -> B e. ZZ )
4	3	adantl	|- ( ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) -> B e. ZZ )
5	4	zred	|- ( ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) -> B e. RR )
6		eluzelre	|- ( x e. ( ZZ>= ` B ) -> x e. RR )
7	6	adantl	|- ( ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) -> x e. RR )
8		eluzle	|- ( x e. ( ZZ>= ` B ) -> B <_ x )
9	8	adantl	|- ( ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) -> B <_ x )
10	5 7 9	lensymd	|- ( ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) -> -. x < B )
11	2 10	pm2.65i	|- -. ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) )
12		elin	|- ( x e. ( ( A ..^ B ) i^i ( ZZ>= ` B ) ) <-> ( x e. ( A ..^ B ) /\ x e. ( ZZ>= ` B ) ) )
13	11 12	mtbir	|- -. x e. ( ( A ..^ B ) i^i ( ZZ>= ` B ) )
14	13	nel0	|- ( ( A ..^ B ) i^i ( ZZ>= ` B ) ) = (/)