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

Metamath Proof Explorer

Theorem seqp1

Description: Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion seqp1 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
2 fveq2 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
3 2 eleq2d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) )
4 seqeq1 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → seq 𝑀 ( + , 𝐹 ) = seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) )
5 4 fveq1d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
6 4 fveq1d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ 𝑁 ) )
7 6 oveq2d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )
8 5 7 eqeq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ↔ ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
9 3 8 imbi12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
10 0z ⊢ 0 ∈ ℤ
11 10 elimel ⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
12 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω )
13 fvex ⊢ ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ∈ V
14 eqid ⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) , ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟩ ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) , ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟩ ) ↾ ω )
15 14 seqval ⊢ seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) , ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟩ ) ↾ ω )
16 11 12 13 14 15 uzrdgsuci ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )
17 9 16 dedth ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
18 1 17 mpcom ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
19 elex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ V )
20 fvex ⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V
21 fvoveq1 ⊢ ( 𝑧 = 𝑁 → ( 𝐹 ‘ ( 𝑧 + 1 ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
22 21 oveq2d ⊢ ( 𝑧 = 𝑁 → ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = ( 𝑤 + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
23 oveq1 ⊢ ( 𝑤 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) → ( 𝑤 + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
24 eqid ⊢ ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
25 ovex ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) ∈ V
26 22 23 24 25 ovmpo ⊢ ( ( 𝑁 ∈ V ∧ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V ) → ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
27 19 20 26 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
28 18 27 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )