Step | Hyp | Ref
| Expression |
1 | | itcovalpc.f |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) |
2 | | nn0ex 11925 |
. . . . . 6
⊢
ℕ0 ∈ V |
3 | 2 | mptex 6970 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ (𝑛 + 𝐶)) ∈ V |
4 | 1, 3 | eqeltri 2847 |
. . . 4
⊢ 𝐹 ∈ V |
5 | | simpl 487 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝑦 ∈ ℕ0) |
6 | | simpr 489 |
. . . 4
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) → ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) |
7 | | itcovalsucov 45432 |
. . . 4
⊢ ((𝐹 ∈ V ∧ 𝑦 ∈ ℕ0
∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))))) |
8 | 4, 5, 6, 7 | mp3an2ani 1466 |
. . 3
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))))) |
9 | | simpr 489 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
10 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → 𝐶 ∈
ℕ0) |
11 | 5 | adantr 485 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → 𝑦 ∈
ℕ0) |
12 | 10, 11 | nn0mulcld 11984 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → (𝐶 · 𝑦) ∈
ℕ0) |
13 | 9, 12 | nn0addcld 11983 |
. . . . . 6
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → (𝑛 + (𝐶 · 𝑦)) ∈
ℕ0) |
14 | | eqidd 2760 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) |
15 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑛 + 𝐶) = (𝑚 + 𝐶)) |
16 | 15 | cbvmptv 5128 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (𝑛 + 𝐶)) = (𝑚 ∈ ℕ0 ↦ (𝑚 + 𝐶)) |
17 | 1, 16 | eqtri 2782 |
. . . . . . 7
⊢ 𝐹 = (𝑚 ∈ ℕ0 ↦ (𝑚 + 𝐶)) |
18 | 17 | a1i 11 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐹 = (𝑚 ∈ ℕ0 ↦ (𝑚 + 𝐶))) |
19 | | oveq1 7150 |
. . . . . 6
⊢ (𝑚 = (𝑛 + (𝐶 · 𝑦)) → (𝑚 + 𝐶) = ((𝑛 + (𝐶 · 𝑦)) + 𝐶)) |
20 | 13, 14, 18, 19 | fmptco 6875 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) = (𝑛 ∈ ℕ0 ↦ ((𝑛 + (𝐶 · 𝑦)) + 𝐶))) |
21 | 9 | nn0cnd 11981 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℂ) |
22 | 12 | nn0cnd 11981 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → (𝐶 · 𝑦) ∈ ℂ) |
23 | 10 | nn0cnd 11981 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → 𝐶 ∈
ℂ) |
24 | 21, 22, 23 | addassd 10686 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → ((𝑛 + (𝐶 · 𝑦)) + 𝐶) = (𝑛 + ((𝐶 · 𝑦) + 𝐶))) |
25 | | nn0cn 11929 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ ℕ0
→ 𝐶 ∈
ℂ) |
26 | 25 | mulid1d 10681 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℕ0
→ (𝐶 · 1) =
𝐶) |
27 | 26 | adantl 486 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐶 · 1) = 𝐶) |
28 | 27 | eqcomd 2765 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐶 = (𝐶 · 1)) |
29 | 28 | oveq2d 7159 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → ((𝐶 · 𝑦) + 𝐶) = ((𝐶 · 𝑦) + (𝐶 · 1))) |
30 | | simpr 489 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐶 ∈
ℕ0) |
31 | 30 | nn0cnd 11981 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐶 ∈ ℂ) |
32 | 5 | nn0cnd 11981 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝑦 ∈ ℂ) |
33 | | 1cnd 10659 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 1 ∈ ℂ) |
34 | 31, 32, 33 | adddid 10688 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐶 · (𝑦 + 1)) = ((𝐶 · 𝑦) + (𝐶 · 1))) |
35 | 29, 34 | eqtr4d 2797 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → ((𝐶 · 𝑦) + 𝐶) = (𝐶 · (𝑦 + 1))) |
36 | 35 | oveq2d 7159 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝑛 + ((𝐶 · 𝑦) + 𝐶)) = (𝑛 + (𝐶 · (𝑦 + 1)))) |
37 | 36 | adantr 485 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → (𝑛 + ((𝐶 · 𝑦) + 𝐶)) = (𝑛 + (𝐶 · (𝑦 + 1)))) |
38 | 24, 37 | eqtrd 2794 |
. . . . . 6
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑛 ∈ ℕ0) → ((𝑛 + (𝐶 · 𝑦)) + 𝐶) = (𝑛 + (𝐶 · (𝑦 + 1)))) |
39 | 38 | mpteq2dva 5120 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝑛 ∈ ℕ0 ↦ ((𝑛 + (𝐶 · 𝑦)) + 𝐶)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))) |
40 | 20, 39 | eqtrd 2794 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))) |
41 | 40 | adantr 485 |
. . 3
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) → (𝐹 ∘ (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))) |
42 | 8, 41 | eqtrd 2794 |
. 2
⊢ (((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦)))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))) |
43 | 42 | ex 417 |
1
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1)))))) |