Theorem fzonfzoufzol

Description: If an element of a half-open integer range is not in the upper part of the range, it is in the lower part of the range. (Contributed by Alexander van der Vekens, 29-Oct-2018)

	Ref	Expression
Assertion	fzonfzoufzol	|- ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) -> ( -. I e. ( ( N - M ) ..^ N ) -> I e. ( 0 ..^ ( N - M ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoel2	|- ( I e. ( 0 ..^ N ) -> N e. ZZ )
2		zsubcl	|- ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
3	2	ex	|- ( N e. ZZ -> ( M e. ZZ -> ( N - M ) e. ZZ ) )
4	1 3	syl	|- ( I e. ( 0 ..^ N ) -> ( M e. ZZ -> ( N - M ) e. ZZ ) )
5	4	impcom	|- ( ( M e. ZZ /\ I e. ( 0 ..^ N ) ) -> ( N - M ) e. ZZ )
6	5	3adant2	|- ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) -> ( N - M ) e. ZZ )
7	6	adantr	|- ( ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) /\ -. I e. ( 0 ..^ ( N - M ) ) ) -> ( N - M ) e. ZZ )
8		simp3	|- ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) -> I e. ( 0 ..^ N ) )
9	8	anim1i	|- ( ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) /\ -. I e. ( 0 ..^ ( N - M ) ) ) -> ( I e. ( 0 ..^ N ) /\ -. I e. ( 0 ..^ ( N - M ) ) ) )
10		elfzonelfzo	|- ( ( N - M ) e. ZZ -> ( ( I e. ( 0 ..^ N ) /\ -. I e. ( 0 ..^ ( N - M ) ) ) -> I e. ( ( N - M ) ..^ N ) ) )
11	7 9 10	sylc	|- ( ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) /\ -. I e. ( 0 ..^ ( N - M ) ) ) -> I e. ( ( N - M ) ..^ N ) )
12	11	ex	|- ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) -> ( -. I e. ( 0 ..^ ( N - M ) ) -> I e. ( ( N - M ) ..^ N ) ) )
13	12	con1d	|- ( ( M e. ZZ /\ M < N /\ I e. ( 0 ..^ N ) ) -> ( -. I e. ( ( N - M ) ..^ N ) -> I e. ( 0 ..^ ( N - M ) ) ) )