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 ) ) ) )