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