| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑛 = 1 → (𝑥↑𝑛) = (𝑥↑1)) |
| 2 | 1 | mpteq2dv 5244 |
. . . 4
⊢ (𝑛 = 1 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑1))) |
| 3 | 2 | oveq2d 7447 |
. . 3
⊢ (𝑛 = 1 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1)))) |
| 4 | | id 22 |
. . . . 5
⊢ (𝑛 = 1 → 𝑛 = 1) |
| 5 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1)) |
| 6 | 5 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = 1 → (𝑥↑(𝑛 − 1)) = (𝑥↑(1 − 1))) |
| 7 | 4, 6 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = 1 → (𝑛 · (𝑥↑(𝑛 − 1))) = (1 · (𝑥↑(1 −
1)))) |
| 8 | 7 | mpteq2dv 5244 |
. . 3
⊢ (𝑛 = 1 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 −
1))))) |
| 9 | 3, 8 | eqeq12d 2753 |
. 2
⊢ (𝑛 = 1 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 −
1)))))) |
| 10 | | oveq2 7439 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘)) |
| 11 | 10 | mpteq2dv 5244 |
. . . 4
⊢ (𝑛 = 𝑘 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
| 12 | 11 | oveq2d 7447 |
. . 3
⊢ (𝑛 = 𝑘 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) |
| 13 | | id 22 |
. . . . 5
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
| 14 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1)) |
| 15 | 14 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑥↑(𝑛 − 1)) = (𝑥↑(𝑘 − 1))) |
| 16 | 13, 15 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = 𝑘 → (𝑛 · (𝑥↑(𝑛 − 1))) = (𝑘 · (𝑥↑(𝑘 − 1)))) |
| 17 | 16 | mpteq2dv 5244 |
. . 3
⊢ (𝑛 = 𝑘 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
| 18 | 12, 17 | eqeq12d 2753 |
. 2
⊢ (𝑛 = 𝑘 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))))) |
| 19 | | oveq2 7439 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1))) |
| 20 | 19 | mpteq2dv 5244 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) |
| 21 | 20 | oveq2d 7447 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))) |
| 22 | | id 22 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) |
| 23 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1)) |
| 24 | 23 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (𝑥↑(𝑛 − 1)) = (𝑥↑((𝑘 + 1) − 1))) |
| 25 | 22, 24 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (𝑛 · (𝑥↑(𝑛 − 1))) = ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) |
| 26 | 25 | mpteq2dv 5244 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))))) |
| 27 | 21, 26 | eqeq12d 2753 |
. 2
⊢ (𝑛 = (𝑘 + 1) → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))))) |
| 28 | | oveq2 7439 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑥↑𝑛) = (𝑥↑𝑁)) |
| 29 | 28 | mpteq2dv 5244 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) |
| 30 | 29 | oveq2d 7447 |
. . 3
⊢ (𝑛 = 𝑁 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)))) |
| 31 | | id 22 |
. . . . 5
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) |
| 32 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1)) |
| 33 | 32 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑥↑(𝑛 − 1)) = (𝑥↑(𝑁 − 1))) |
| 34 | 31, 33 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝑛 · (𝑥↑(𝑛 − 1))) = (𝑁 · (𝑥↑(𝑁 − 1)))) |
| 35 | 34 | mpteq2dv 5244 |
. . 3
⊢ (𝑛 = 𝑁 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) |
| 36 | 30, 35 | eqeq12d 2753 |
. 2
⊢ (𝑛 = 𝑁 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))) |
| 37 | | exp1 14108 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) |
| 38 | 37 | mpteq2ia 5245 |
. . . . 5
⊢ (𝑥 ∈ ℂ ↦ (𝑥↑1)) = (𝑥 ∈ ℂ ↦ 𝑥) |
| 39 | | mptresid 6069 |
. . . . 5
⊢ ( I
↾ ℂ) = (𝑥
∈ ℂ ↦ 𝑥) |
| 40 | 38, 39 | eqtr4i 2768 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦ (𝑥↑1)) = ( I ↾
ℂ) |
| 41 | 40 | oveq2i 7442 |
. . 3
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑1))) = (ℂ D (
I ↾ ℂ)) |
| 42 | | 1m1e0 12338 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
| 43 | 42 | oveq2i 7442 |
. . . . . . . . 9
⊢ (𝑥↑(1 − 1)) = (𝑥↑0) |
| 44 | | exp0 14106 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥↑0) = 1) |
| 45 | 43, 44 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (𝑥↑(1 − 1)) =
1) |
| 46 | 45 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (1
· (𝑥↑(1 −
1))) = (1 · 1)) |
| 47 | | 1t1e1 12428 |
. . . . . . 7
⊢ (1
· 1) = 1 |
| 48 | 46, 47 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (1
· (𝑥↑(1 −
1))) = 1) |
| 49 | 48 | mpteq2ia 5245 |
. . . . 5
⊢ (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) = (𝑥 ∈ ℂ
↦ 1) |
| 50 | | fconstmpt 5747 |
. . . . 5
⊢ (ℂ
× {1}) = (𝑥 ∈
ℂ ↦ 1) |
| 51 | 49, 50 | eqtr4i 2768 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) = (ℂ × {1}) |
| 52 | | dvid 25953 |
. . . 4
⊢ (ℂ
D ( I ↾ ℂ)) = (ℂ × {1}) |
| 53 | 51, 52 | eqtr4i 2768 |
. . 3
⊢ (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) = (ℂ D ( I ↾ ℂ)) |
| 54 | 41, 53 | eqtr4i 2768 |
. 2
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑1))) = (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) |
| 55 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 𝑘 ∈
ℂ) |
| 57 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 58 | | pncan 11514 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
| 59 | 56, 57, 58 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘) |
| 60 | 59 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑((𝑘 + 1) − 1)) = (𝑥↑𝑘)) |
| 61 | 60 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑥↑𝑘))) |
| 62 | 57 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 1 ∈
ℂ) |
| 63 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
| 64 | | nnnn0 12533 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 65 | | expcl 14120 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑥↑𝑘) ∈
ℂ) |
| 66 | 63, 64, 65 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑘) ∈ ℂ) |
| 67 | 56, 62, 66 | adddird 11286 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑𝑘)) = ((𝑘 · (𝑥↑𝑘)) + (1 · (𝑥↑𝑘)))) |
| 68 | 66 | mullidd 11279 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (1
· (𝑥↑𝑘)) = (𝑥↑𝑘)) |
| 69 | 68 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑𝑘)) + (1 · (𝑥↑𝑘))) = ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘))) |
| 70 | 61, 67, 69 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))) = ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘))) |
| 71 | 70 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘)))) |
| 72 | | cnex 11236 |
. . . . . . . 8
⊢ ℂ
∈ V |
| 73 | 72 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ℂ
∈ V) |
| 74 | 56, 66 | mulcld 11281 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑𝑘)) ∈ ℂ) |
| 75 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
| 76 | | expcl 14120 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑘 − 1) ∈
ℕ0) → (𝑥↑(𝑘 − 1)) ∈ ℂ) |
| 77 | 63, 75, 76 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑘 − 1)) ∈ ℂ) |
| 78 | 56, 77 | mulcld 11281 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑(𝑘 − 1))) ∈
ℂ) |
| 79 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
| 80 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
| 81 | 39 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ( I
↾ ℂ) = (𝑥
∈ ℂ ↦ 𝑥)) |
| 82 | 73, 78, 79, 80, 81 | offval2 7717 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ)) = (𝑥
∈ ℂ ↦ ((𝑘
· (𝑥↑(𝑘 − 1))) · 𝑥))) |
| 83 | 56, 77, 79 | mulassd 11284 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥) = (𝑘 · ((𝑥↑(𝑘 − 1)) · 𝑥))) |
| 84 | | expm1t 14131 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝑥↑𝑘) = ((𝑥↑(𝑘 − 1)) · 𝑥)) |
| 85 | 84 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑘) = ((𝑥↑(𝑘 − 1)) · 𝑥)) |
| 86 | 85 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑𝑘)) = (𝑘 · ((𝑥↑(𝑘 − 1)) · 𝑥))) |
| 87 | 83, 86 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥) = (𝑘 · (𝑥↑𝑘))) |
| 88 | 87 | mpteq2dva 5242 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥)) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑𝑘)))) |
| 89 | 82, 88 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ)) = (𝑥
∈ ℂ ↦ (𝑘
· (𝑥↑𝑘)))) |
| 90 | 52, 50 | eqtri 2765 |
. . . . . . . . . 10
⊢ (ℂ
D ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ 1) |
| 91 | 90 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (ℂ
D ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ 1)) |
| 92 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
| 93 | 73, 62, 66, 91, 92 | offval2 7717 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((ℂ
D ( I ↾ ℂ)) ∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑𝑘)))) |
| 94 | 68 | mpteq2dva 5242 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (1
· (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
| 95 | 93, 94 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((ℂ
D ( I ↾ ℂ)) ∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
| 96 | 73, 74, 66, 89, 95 | offval2 7717 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘)))) |
| 97 | 71, 96 | eqtr4d 2780 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
| 98 | | oveq1 7438 |
. . . . . . 7
⊢ ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘f · ( I ↾
ℂ)) = ((𝑥 ∈
ℂ ↦ (𝑘 ·
(𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ))) |
| 99 | 98 | oveq1d 7446 |
. . . . . 6
⊢ ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘f · ( I ↾
ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
| 100 | 99 | eqcomd 2743 |
. . . . 5
⊢ ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘f · (
I ↾ ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘f · ( I ↾
ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
| 101 | 97, 100 | sylan9eq 2797 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘f · ( I ↾
ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
| 102 | | cnelprrecn 11248 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
| 103 | 102 | a1i 11 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → ℂ ∈
{ℝ, ℂ}) |
| 104 | 66 | fmpttd 7135 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)):ℂ⟶ℂ) |
| 105 | 104 | adantr 480 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)):ℂ⟶ℂ) |
| 106 | | f1oi 6886 |
. . . . . 6
⊢ ( I
↾ ℂ):ℂ–1-1-onto→ℂ |
| 107 | | f1of 6848 |
. . . . . 6
⊢ (( I
↾ ℂ):ℂ–1-1-onto→ℂ → ( I ↾
ℂ):ℂ⟶ℂ) |
| 108 | 106, 107 | mp1i 13 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → ( I ↾
ℂ):ℂ⟶ℂ) |
| 109 | | simpr 484 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
| 110 | 109 | dmeqd 5916 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = dom (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
| 111 | 78 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 −
1)))):ℂ⟶ℂ) |
| 112 | 111 | adantr 480 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 −
1)))):ℂ⟶ℂ) |
| 113 | 112 | fdmd 6746 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = ℂ) |
| 114 | 110, 113 | eqtrd 2777 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = ℂ) |
| 115 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 116 | 115 | fconst 6794 |
. . . . . . . 8
⊢ (ℂ
× {1}):ℂ⟶{1} |
| 117 | 52 | feq1i 6727 |
. . . . . . . 8
⊢ ((ℂ
D ( I ↾ ℂ)):ℂ⟶{1} ↔ (ℂ ×
{1}):ℂ⟶{1}) |
| 118 | 116, 117 | mpbir 231 |
. . . . . . 7
⊢ (ℂ
D ( I ↾ ℂ)):ℂ⟶{1} |
| 119 | 118 | fdmi 6747 |
. . . . . 6
⊢ dom
(ℂ D ( I ↾ ℂ)) = ℂ |
| 120 | 119 | a1i 11 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D ( I
↾ ℂ)) = ℂ) |
| 121 | 103, 105,
108, 114, 120 | dvmulf 25980 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘f · ( I ↾
ℂ))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘f · ( I ↾
ℂ)) ∘f + ((ℂ D ( I ↾ ℂ))
∘f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
| 122 | 73, 66, 79, 92, 81 | offval2 7717 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘f · ( I ↾
ℂ)) = (𝑥 ∈
ℂ ↦ ((𝑥↑𝑘) · 𝑥))) |
| 123 | | expp1 14109 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑥↑(𝑘 + 1)) = ((𝑥↑𝑘) · 𝑥)) |
| 124 | 63, 64, 123 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑘 + 1)) = ((𝑥↑𝑘) · 𝑥)) |
| 125 | 124 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))) = (𝑥 ∈ ℂ ↦ ((𝑥↑𝑘) · 𝑥))) |
| 126 | 122, 125 | eqtr4d 2780 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘f · ( I ↾
ℂ)) = (𝑥 ∈
ℂ ↦ (𝑥↑(𝑘 + 1)))) |
| 127 | 126 | oveq2d 7447 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (ℂ
D ((𝑥 ∈ ℂ
↦ (𝑥↑𝑘)) ∘f ·
( I ↾ ℂ))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))) |
| 128 | 127 | adantr 480 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘f · ( I ↾
ℂ))) = (ℂ D (𝑥
∈ ℂ ↦ (𝑥↑(𝑘 + 1))))) |
| 129 | 101, 121,
128 | 3eqtr2rd 2784 |
. . 3
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))))) |
| 130 | 129 | ex 412 |
. 2
⊢ (𝑘 ∈ ℕ → ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))))) |
| 131 | 9, 18, 27, 36, 54, 130 | nnind 12284 |
1
⊢ (𝑁 ∈ ℕ → (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) |