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

Metamath Proof Explorer

Theorem elfzoextl

Description: Membership of an integer in an extended open range of integers, extension added to the left. (Contributed by AV, 31-Aug-2025) Generalized by replacing the left border of the ranges. (Revised by SN, 18-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 elfzoel2 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
2 nn0pzuz ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝐼 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
3 1 2 sylan2 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐼 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
4 fzoss2 ⊢ ( ( 𝐼 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) )
5 3 4 syl ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) )
6 5 sseld ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 ∈ ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) ) )
7 6 syldbl2 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑍 ∈ ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) )
8 7 ancoms ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) )