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 ∈ ℤ ∧ M < N ∧ I ∈ 0 ..^ N → ¬ I ∈ N − M ..^ N → I ∈ 0 ..^ N − M

Proof

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