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	syl5bb	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e/ ( M ..^ N ) <-> ( K < M \/ N <_ K ) ) )