Theorem seqf2

Description: Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		seqcl2.1	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝐶 )
2		seqcl2.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐶 )
3		seqf2.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		seqf2.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		seqf2.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
6		seqfn	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) )
7	4 6	syl	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ 𝐶 )
9	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐶 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
11		elfzuz	⊢ ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑘 ) → 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
12	11 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑘 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
13	12	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑘 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
14	8 9 10 13	seqcl2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ∈ 𝐶 )
15	14	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ∈ 𝐶 )
16		ffnfv	⊢ ( seq 𝑀 ( + , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ 𝐶 ↔ ( seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ∈ 𝐶 ) )
17	7 15 16	sylanbrc	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ 𝐶 )
18	3	feq2i	⊢ ( seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ 𝐶 ↔ seq 𝑀 ( + , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ 𝐶 )
19	17 18	sylibr	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ 𝐶 )