This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) = (/)