| Step | Hyp | Ref
| Expression |
| 1 | | itcovalt2.f |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2
· 𝑛) + 𝐶)) |
| 2 | | nn0ex 12532 |
. . . . . 6
⊢
ℕ0 ∈ V |
| 3 | 2 | mptex 7243 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ ((2 · 𝑛) +
𝐶)) ∈
V |
| 4 | 1, 3 | eqeltri 2837 |
. . . 4
⊢ 𝐹 ∈ V |
| 5 | | simpl 482 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝑦 ∈ ℕ0) |
| 6 | | simpr 484 |
. . . 4
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) |
| 7 | | itcovalsucov 48589 |
. . . 4
⊢ ((𝐹 ∈ V ∧ 𝑦 ∈ ℕ0
∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)))) |
| 8 | 4, 5, 6, 7 | mp3an2ani 1470 |
. . 3
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)))) |
| 9 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 10 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ 2 ∈ ℕ) |
| 11 | | id 22 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℕ0) |
| 12 | 10, 11 | nnexpcld 14284 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℕ) |
| 13 | | itcovalt2lem2lem1 48594 |
. . . . . . 7
⊢
((((2↑𝑦) ∈
ℕ ∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶) ∈
ℕ0) |
| 14 | 12, 13 | sylanl1 680 |
. . . . . 6
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶) ∈
ℕ0) |
| 15 | | eqidd 2738 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) |
| 16 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚)) |
| 17 | 16 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → ((2 · 𝑛) + 𝐶) = ((2 · 𝑚) + 𝐶)) |
| 18 | 17 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((2 · 𝑛) +
𝐶)) = (𝑚 ∈ ℕ0 ↦ ((2
· 𝑚) + 𝐶)) |
| 19 | 1, 18 | eqtri 2765 |
. . . . . . 7
⊢ 𝐹 = (𝑚 ∈ ℕ0 ↦ ((2
· 𝑚) + 𝐶)) |
| 20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐹 = (𝑚 ∈ ℕ0 ↦ ((2
· 𝑚) + 𝐶))) |
| 21 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑚 = (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶) → (2 · 𝑚) = (2 · (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) |
| 22 | 21 | oveq1d 7446 |
. . . . . 6
⊢ (𝑚 = (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶) → ((2 · 𝑚) + 𝐶) = ((2 · (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) + 𝐶)) |
| 23 | 14, 15, 20, 22 | fmptco 7149 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) = (𝑛 ∈ ℕ0 ↦ ((2
· (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) + 𝐶))) |
| 24 | | itcovalt2lem2lem2 48595 |
. . . . . 6
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → ((2
· (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) + 𝐶) = (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)) |
| 25 | 24 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝑛 ∈ ℕ0 ↦ ((2
· (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) + 𝐶)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))) |
| 26 | 23, 25 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))) |
| 27 | 26 | adantr 480 |
. . 3
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))) |
| 28 | 8, 27 | eqtrd 2777 |
. 2
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))) |
| 29 | 28 | ex 412 |
1
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) |