Metamath Proof Explorer

Theorem elfzoext

Description: Membership of an integer in an extended open range of integers. (Contributed by AV, 30-Apr-2020)

Ref Expression
Assertion elfzoext ⊢ Z ∈ M ..^ N ∧ I ∈ ℕ 0 → Z ∈ M ..^ N + I

Proof

Step Hyp Ref Expression
1 elfzoel2 ⊢ Z ∈ M ..^ N → N ∈ ℤ
2 zcn ⊢ N ∈ ℤ → N ∈ ℂ
3 nn0cn ⊢ I ∈ ℕ 0 → I ∈ ℂ
4 addcom ⊢ N ∈ ℂ ∧ I ∈ ℂ → N + I = I + N
5 2 3 4 syl2an ⊢ N ∈ ℤ ∧ I ∈ ℕ 0 → N + I = I + N
6 nn0pzuz ⊢ I ∈ ℕ 0 ∧ N ∈ ℤ → I + N ∈ ℤ ≥ N
7 6 ancoms ⊢ N ∈ ℤ ∧ I ∈ ℕ 0 → I + N ∈ ℤ ≥ N
8 5 7 eqeltrd ⊢ N ∈ ℤ ∧ I ∈ ℕ 0 → N + I ∈ ℤ ≥ N
9 fzoss2 ⊢ N + I ∈ ℤ ≥ N → M ..^ N ⊆ M ..^ N + I
10 8 9 syl ⊢ N ∈ ℤ ∧ I ∈ ℕ 0 → M ..^ N ⊆ M ..^ N + I
11 10 sselda ⊢ N ∈ ℤ ∧ I ∈ ℕ 0 ∧ Z ∈ M ..^ N → Z ∈ M ..^ N + I
12 11 expcom ⊢ Z ∈ M ..^ N → N ∈ ℤ ∧ I ∈ ℕ 0 → Z ∈ M ..^ N + I
13 1 12 mpand ⊢ Z ∈ M ..^ N → I ∈ ℕ 0 → Z ∈ M ..^ N + I
14 13 imp ⊢ Z ∈ M ..^ N ∧ I ∈ ℕ 0 → Z ∈ M ..^ N + I