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 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ 𝑆 )