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

Metamath Proof Explorer

Theorem zpnn0elfzo

Description: Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion zpnn0elfzo ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 uzid ⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ( ℤ≥ ‘ 𝑍 ) )
2 1 anim1i ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 ∈ ( ℤ≥ ‘ 𝑍 ) ∧ 𝑁 ∈ ℕ0 ) )
3 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
4 zaddcl ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑍 + 𝑁 ) ∈ ℤ )
5 3 4 sylan2 ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ℤ )
6 elfzomin ⊢ ( ( 𝑍 + 𝑁 ) ∈ ℤ → ( 𝑍 + 𝑁 ) ∈ ( ( 𝑍 + 𝑁 ) ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )
7 5 6 syl ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( ( 𝑍 + 𝑁 ) ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )
8 uzaddcl ⊢ ( ( 𝑍 ∈ ( ℤ≥ ‘ 𝑍 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑍 ) )
9 fzoss1 ⊢ ( ( 𝑍 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑍 ) → ( ( 𝑍 + 𝑁 ) ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) ⊆ ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )
10 8 9 syl ⊢ ( ( 𝑍 ∈ ( ℤ≥ ‘ 𝑍 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑍 + 𝑁 ) ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) ⊆ ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )
11 10 sselda ⊢ ( ( ( 𝑍 ∈ ( ℤ≥ ‘ 𝑍 ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑍 + 𝑁 ) ∈ ( ( 𝑍 + 𝑁 ) ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) ) → ( 𝑍 + 𝑁 ) ∈ ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )
12 2 7 11 syl2anc ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )