| 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 ) ) ) ) |