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

Metamath Proof Explorer

Theorem seqcl

Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqcl.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqcl.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
seqcl.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
Assertion seqcl ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 seqcl.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 seqcl.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
3 seqcl.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑀 ) )
5 4 eleq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( 𝐹 ‘ 𝑀 ) ∈ 𝑆 ) )
6 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
7 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
8 1 7 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
9 5 6 8 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝑆 )
10 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
11 1 10 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
12 fzp1ss ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
13 11 12 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
14 13 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
15 14 2 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
16 9 3 1 15 seqcl2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝑆 )