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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( ¬ 𝐼 ∈ ( ( 𝑁 − 𝑀 ) ..^ 𝑁 ) → 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoel2	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
2		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
3	2	ex	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℤ → ( 𝑁 − 𝑀 ) ∈ ℤ ) )
4	1 3	syl	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝑀 ∈ ℤ → ( 𝑁 − 𝑀 ) ∈ ℤ ) )
5	4	impcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
6	5	3adant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
7	6	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
8		simp3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → 𝐼 ∈ ( 0 ..^ 𝑁 ) )
9	8	anim1i	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ ¬ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )
10		elfzonelfzo	⊢ ( ( 𝑁 − 𝑀 ) ∈ ℤ → ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ ¬ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝐼 ∈ ( ( 𝑁 − 𝑀 ) ..^ 𝑁 ) ) )
11	7 9 10	sylc	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝐼 ∈ ( ( 𝑁 − 𝑀 ) ..^ 𝑁 ) )
12	11	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( ¬ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → 𝐼 ∈ ( ( 𝑁 − 𝑀 ) ..^ 𝑁 ) ) )
13	12	con1d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 < 𝑁 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( ¬ 𝐼 ∈ ( ( 𝑁 − 𝑀 ) ..^ 𝑁 ) → 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )