Step | Hyp | Ref
| Expression |
1 | | fveq2 6651 |
. . . . 5
⊢ (𝑥 = 0 →
((IterComp‘𝐹)‘𝑥) = ((IterComp‘𝐹)‘0)) |
2 | | oveq2 7151 |
. . . . . . . 8
⊢ (𝑥 = 0 → (2↑𝑥) = (2↑0)) |
3 | 2 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑛 + 𝐶) · (2↑𝑥)) = ((𝑛 + 𝐶) · (2↑0))) |
4 | 3 | oveq1d 7158 |
. . . . . 6
⊢ (𝑥 = 0 → (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶) = (((𝑛 + 𝐶) · (2↑0)) − 𝐶)) |
5 | 4 | mpteq2dv 5121 |
. . . . 5
⊢ (𝑥 = 0 → (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))) |
6 | 1, 5 | eqeq12d 2775 |
. . . 4
⊢ (𝑥 = 0 →
(((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) ↔ ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶)))) |
7 | 6 | imbi2d 345 |
. . 3
⊢ (𝑥 = 0 → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶))) ↔ (𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))))) |
8 | | fveq2 6651 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((IterComp‘𝐹)‘𝑥) = ((IterComp‘𝐹)‘𝑦)) |
9 | | oveq2 7151 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (2↑𝑥) = (2↑𝑦)) |
10 | 9 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑛 + 𝐶) · (2↑𝑥)) = ((𝑛 + 𝐶) · (2↑𝑦))) |
11 | 10 | oveq1d 7158 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶) = (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) |
12 | 11 | mpteq2dv 5121 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) |
13 | 8, 12 | eqeq12d 2775 |
. . . 4
⊢ (𝑥 = 𝑦 → (((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) ↔ ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)))) |
14 | 13 | imbi2d 345 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶))) ↔ (𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))))) |
15 | | fveq2 6651 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((IterComp‘𝐹)‘𝑥) = ((IterComp‘𝐹)‘(𝑦 + 1))) |
16 | | oveq2 7151 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (2↑𝑥) = (2↑(𝑦 + 1))) |
17 | 16 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑛 + 𝐶) · (2↑𝑥)) = ((𝑛 + 𝐶) · (2↑(𝑦 + 1)))) |
18 | 17 | oveq1d 7158 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶) = (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)) |
19 | 18 | mpteq2dv 5121 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))) |
20 | 15, 19 | eqeq12d 2775 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) ↔ ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) |
21 | 20 | imbi2d 345 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶))) ↔ (𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))) |
22 | | fveq2 6651 |
. . . . 5
⊢ (𝑥 = 𝐼 → ((IterComp‘𝐹)‘𝑥) = ((IterComp‘𝐹)‘𝐼)) |
23 | | oveq2 7151 |
. . . . . . . 8
⊢ (𝑥 = 𝐼 → (2↑𝑥) = (2↑𝐼)) |
24 | 23 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑥 = 𝐼 → ((𝑛 + 𝐶) · (2↑𝑥)) = ((𝑛 + 𝐶) · (2↑𝐼))) |
25 | 24 | oveq1d 7158 |
. . . . . 6
⊢ (𝑥 = 𝐼 → (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶) = (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶)) |
26 | 25 | mpteq2dv 5121 |
. . . . 5
⊢ (𝑥 = 𝐼 → (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶))) |
27 | 22, 26 | eqeq12d 2775 |
. . . 4
⊢ (𝑥 = 𝐼 → (((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶)) ↔ ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶)))) |
28 | 27 | imbi2d 345 |
. . 3
⊢ (𝑥 = 𝐼 → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑥) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑥)) − 𝐶))) ↔ (𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶))))) |
29 | | itcovalt2.f |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2
· 𝑛) + 𝐶)) |
30 | 29 | itcovalt2lem1 45439 |
. . 3
⊢ (𝐶 ∈ ℕ0
→ ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))) |
31 | | pm2.27 42 |
. . . . . . 7
⊢ (𝐶 ∈ ℕ0
→ ((𝐶 ∈
ℕ0 → ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)))) |
32 | 31 | adantl 486 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)))) |
33 | 29 | itcovalt2lem2 45440 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) |
34 | 32, 33 | syld 47 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) |
35 | 34 | ex 417 |
. . . 4
⊢ (𝑦 ∈ ℕ0
→ (𝐶 ∈
ℕ0 → ((𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))) |
36 | 35 | com23 86 |
. . 3
⊢ (𝑦 ∈ ℕ0
→ ((𝐶 ∈
ℕ0 → ((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶))) → (𝐶 ∈ ℕ0 →
((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))) |
37 | 7, 14, 21, 28, 30, 36 | nn0ind 12101 |
. 2
⊢ (𝐼 ∈ ℕ0
→ (𝐶 ∈
ℕ0 → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶)))) |
38 | 37 | imp 411 |
1
⊢ ((𝐼 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶))) |