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

Metamath Proof Explorer

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