Metamath Proof Explorer


Theorem fzodisj

Description: Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fzodisj A..^BB..^C=

Proof

Step Hyp Ref Expression
1 disj1 A..^BB..^C=xxA..^B¬xB..^C
2 elfzolt2 xA..^Bx<B
3 elfzoelz xA..^Bx
4 3 zred xA..^Bx
5 elfzoel2 xA..^BB
6 5 zred xA..^BB
7 4 6 ltnled xA..^Bx<B¬Bx
8 2 7 mpbid xA..^B¬Bx
9 elfzole1 xB..^CBx
10 8 9 nsyl xA..^B¬xB..^C
11 1 10 mpgbir A..^BB..^C=