Theorem elfzoext

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

	Ref	Expression
Assertion	elfzoext	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) )

Proof

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