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

Metamath Proof Explorer

Theorem seqf

Description: Range of the recursive sequence builder (special case of seqf2 ). (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypotheses seqf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
seqf.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
seqf.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
seqf.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
Assertion seqf ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 seqf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 seqf.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 seqf.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
4 seqf.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
5 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑀 ) )
6 5 eleq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( 𝐹 ‘ 𝑀 ) ∈ 𝑆 ) )
7 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
8 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 2 8 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 9 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
11 6 7 10 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝑆 )
12 peano2uzr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 2 12 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
14 13 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ 𝑍 )
15 14 3 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
16 11 4 1 2 15 seqf2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ 𝑆 )