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

Metamath Proof Explorer

Theorem nelfzo

Description: An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020)

Ref Expression
Assertion nelfzo 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e/ ( M ..^ N ) <-> ( K < M \/ N <_ K ) ) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( K e/ ( M ..^ N ) <-> -. K e. ( M ..^ N ) )
2 ianor 
 |-  ( -. ( M <_ K /\ K < N ) <-> ( -. M <_ K \/ -. K < N ) )
3 2 a1i 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. ( M <_ K /\ K < N ) <-> ( -. M <_ K \/ -. K < N ) ) )
4 elfzo 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ..^ N ) <-> ( M <_ K /\ K < N ) ) )
5 4 notbid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. K e. ( M ..^ N ) <-> -. ( M <_ K /\ K < N ) ) )
6 zre 
 |-  ( K e. ZZ -> K e. RR )
7 zre 
 |-  ( M e. ZZ -> M e. RR )
8 6 7 anim12i 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K e. RR /\ M e. RR ) )
9 8 3adant3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. RR /\ M e. RR ) )
10 ltnle 
 |-  ( ( K e. RR /\ M e. RR ) -> ( K < M <-> -. M <_ K ) )
11 9 10 syl 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K < M <-> -. M <_ K ) )
12 zre 
 |-  ( N e. ZZ -> N e. RR )
13 6 12 anim12ci 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( N e. RR /\ K e. RR ) )
14 13 3adant2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( N e. RR /\ K e. RR ) )
15 lenlt 
 |-  ( ( N e. RR /\ K e. RR ) -> ( N <_ K <-> -. K < N ) )
16 14 15 syl 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( N <_ K <-> -. K < N ) )
17 11 16 orbi12d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K < M \/ N <_ K ) <-> ( -. M <_ K \/ -. K < N ) ) )
18 3 5 17 3bitr4d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. K e. ( M ..^ N ) <-> ( K < M \/ N <_ K ) ) )
19 1 18 bitrid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e/ ( M ..^ N ) <-> ( K < M \/ N <_ K ) ) )