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

Metamath Proof Explorer

Theorem zpnn0elfzo1

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 zpnn0elfzo1 ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( 𝑍 ..^ ( 𝑍 + ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 zpnn0elfzo ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) )
2 zcn ⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ℂ )
3 2 adantr ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑍 ∈ ℂ )
4 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
5 4 adantl ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
6 1cnd ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℂ )
7 3 5 6 addassd ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑍 + 𝑁 ) + 1 ) = ( 𝑍 + ( 𝑁 + 1 ) ) )
8 7 oveq2d ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 ..^ ( ( 𝑍 + 𝑁 ) + 1 ) ) = ( 𝑍 ..^ ( 𝑍 + ( 𝑁 + 1 ) ) ) )
9 1 8 eleqtrd ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑍 + 𝑁 ) ∈ ( 𝑍 ..^ ( 𝑍 + ( 𝑁 + 1 ) ) ) )