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