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

Metamath Proof Explorer

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 ) ) ) )