Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = 1 → (𝑥↑𝑛) = (𝑥↑1)) |
2 | 1 | mpteq2dv 4745 |
. . . 4
⊢ (𝑛 = 1 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑1))) |
3 | 2 | oveq2d 6666 |
. . 3
⊢ (𝑛 = 1 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1)))) |
4 | | id 22 |
. . . . 5
⊢ (𝑛 = 1 → 𝑛 = 1) |
5 | | oveq1 6657 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1)) |
6 | 5 | oveq2d 6666 |
. . . . 5
⊢ (𝑛 = 1 → (𝑥↑(𝑛 − 1)) = (𝑥↑(1 − 1))) |
7 | 4, 6 | oveq12d 6668 |
. . . 4
⊢ (𝑛 = 1 → (𝑛 · (𝑥↑(𝑛 − 1))) = (1 · (𝑥↑(1 −
1)))) |
8 | 7 | mpteq2dv 4745 |
. . 3
⊢ (𝑛 = 1 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 −
1))))) |
9 | 3, 8 | eqeq12d 2637 |
. 2
⊢ (𝑛 = 1 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 −
1)))))) |
10 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘)) |
11 | 10 | mpteq2dv 4745 |
. . . 4
⊢ (𝑛 = 𝑘 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
12 | 11 | oveq2d 6666 |
. . 3
⊢ (𝑛 = 𝑘 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) |
13 | | id 22 |
. . . . 5
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
14 | | oveq1 6657 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1)) |
15 | 14 | oveq2d 6666 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑥↑(𝑛 − 1)) = (𝑥↑(𝑘 − 1))) |
16 | 13, 15 | oveq12d 6668 |
. . . 4
⊢ (𝑛 = 𝑘 → (𝑛 · (𝑥↑(𝑛 − 1))) = (𝑘 · (𝑥↑(𝑘 − 1)))) |
17 | 16 | mpteq2dv 4745 |
. . 3
⊢ (𝑛 = 𝑘 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
18 | 12, 17 | eqeq12d 2637 |
. 2
⊢ (𝑛 = 𝑘 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))))) |
19 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1))) |
20 | 19 | mpteq2dv 4745 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) |
21 | 20 | oveq2d 6666 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))) |
22 | | id 22 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) |
23 | | oveq1 6657 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1)) |
24 | 23 | oveq2d 6666 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (𝑥↑(𝑛 − 1)) = (𝑥↑((𝑘 + 1) − 1))) |
25 | 22, 24 | oveq12d 6668 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (𝑛 · (𝑥↑(𝑛 − 1))) = ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) |
26 | 25 | mpteq2dv 4745 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))))) |
27 | 21, 26 | eqeq12d 2637 |
. 2
⊢ (𝑛 = (𝑘 + 1) → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))))) |
28 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑥↑𝑛) = (𝑥↑𝑁)) |
29 | 28 | mpteq2dv 4745 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) |
30 | 29 | oveq2d 6666 |
. . 3
⊢ (𝑛 = 𝑁 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)))) |
31 | | id 22 |
. . . . 5
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) |
32 | | oveq1 6657 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1)) |
33 | 32 | oveq2d 6666 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑥↑(𝑛 − 1)) = (𝑥↑(𝑁 − 1))) |
34 | 31, 33 | oveq12d 6668 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝑛 · (𝑥↑(𝑛 − 1))) = (𝑁 · (𝑥↑(𝑁 − 1)))) |
35 | 34 | mpteq2dv 4745 |
. . 3
⊢ (𝑛 = 𝑁 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) |
36 | 30, 35 | eqeq12d 2637 |
. 2
⊢ (𝑛 = 𝑁 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))) |
37 | | exp1 12866 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) |
38 | 37 | mpteq2ia 4740 |
. . . . 5
⊢ (𝑥 ∈ ℂ ↦ (𝑥↑1)) = (𝑥 ∈ ℂ ↦ 𝑥) |
39 | | mptresid 5456 |
. . . . 5
⊢ (𝑥 ∈ ℂ ↦ 𝑥) = ( I ↾
ℂ) |
40 | 38, 39 | eqtri 2644 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦ (𝑥↑1)) = ( I ↾
ℂ) |
41 | 40 | oveq2i 6661 |
. . 3
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑1))) = (ℂ D (
I ↾ ℂ)) |
42 | | 1m1e0 11089 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
43 | 42 | oveq2i 6661 |
. . . . . . . . 9
⊢ (𝑥↑(1 − 1)) = (𝑥↑0) |
44 | | exp0 12864 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥↑0) = 1) |
45 | 43, 44 | syl5eq 2668 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (𝑥↑(1 − 1)) =
1) |
46 | 45 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (1
· (𝑥↑(1 −
1))) = (1 · 1)) |
47 | | 1t1e1 11175 |
. . . . . . 7
⊢ (1
· 1) = 1 |
48 | 46, 47 | syl6eq 2672 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (1
· (𝑥↑(1 −
1))) = 1) |
49 | 48 | mpteq2ia 4740 |
. . . . 5
⊢ (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) = (𝑥 ∈ ℂ
↦ 1) |
50 | | fconstmpt 5163 |
. . . . 5
⊢ (ℂ
× {1}) = (𝑥 ∈
ℂ ↦ 1) |
51 | 49, 50 | eqtr4i 2647 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) = (ℂ × {1}) |
52 | | dvid 23681 |
. . . 4
⊢ (ℂ
D ( I ↾ ℂ)) = (ℂ × {1}) |
53 | 51, 52 | eqtr4i 2647 |
. . 3
⊢ (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) = (ℂ D ( I ↾ ℂ)) |
54 | 41, 53 | eqtr4i 2647 |
. 2
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑1))) = (𝑥 ∈ ℂ ↦ (1
· (𝑥↑(1 −
1)))) |
55 | | nncn 11028 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
56 | 55 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 𝑘 ∈
ℂ) |
57 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
58 | | pncan 10287 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
59 | 56, 57, 58 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘) |
60 | 59 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑((𝑘 + 1) − 1)) = (𝑥↑𝑘)) |
61 | 60 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑥↑𝑘))) |
62 | 57 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 1 ∈
ℂ) |
63 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
64 | | nnnn0 11299 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
65 | | expcl 12878 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑥↑𝑘) ∈
ℂ) |
66 | 63, 64, 65 | syl2anr 495 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑘) ∈ ℂ) |
67 | 56, 62, 66 | adddird 10065 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑𝑘)) = ((𝑘 · (𝑥↑𝑘)) + (1 · (𝑥↑𝑘)))) |
68 | 66 | mulid2d 10058 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (1
· (𝑥↑𝑘)) = (𝑥↑𝑘)) |
69 | 68 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑𝑘)) + (1 · (𝑥↑𝑘))) = ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘))) |
70 | 61, 67, 69 | 3eqtrd 2660 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))) = ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘))) |
71 | 70 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘)))) |
72 | | cnex 10017 |
. . . . . . . 8
⊢ ℂ
∈ V |
73 | 72 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ℂ
∈ V) |
74 | 56, 66 | mulcld 10060 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑𝑘)) ∈ ℂ) |
75 | | nnm1nn0 11334 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
76 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑘 − 1) ∈
ℕ0) → (𝑥↑(𝑘 − 1)) ∈ ℂ) |
77 | 63, 75, 76 | syl2anr 495 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑘 − 1)) ∈ ℂ) |
78 | 56, 77 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑(𝑘 − 1))) ∈
ℂ) |
79 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
80 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
81 | 39 | eqcomi 2631 |
. . . . . . . . . 10
⊢ ( I
↾ ℂ) = (𝑥
∈ ℂ ↦ 𝑥) |
82 | 81 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ( I
↾ ℂ) = (𝑥
∈ ℂ ↦ 𝑥)) |
83 | 73, 78, 79, 80, 82 | offval2 6914 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘𝑓
· ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥))) |
84 | 56, 77, 79 | mulassd 10063 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥) = (𝑘 · ((𝑥↑(𝑘 − 1)) · 𝑥))) |
85 | | expm1t 12888 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝑥↑𝑘) = ((𝑥↑(𝑘 − 1)) · 𝑥)) |
86 | 85 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑘) = ((𝑥↑(𝑘 − 1)) · 𝑥)) |
87 | 86 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑𝑘)) = (𝑘 · ((𝑥↑(𝑘 − 1)) · 𝑥))) |
88 | 84, 87 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥) = (𝑘 · (𝑥↑𝑘))) |
89 | 88 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥)) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑𝑘)))) |
90 | 83, 89 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘𝑓
· ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑𝑘)))) |
91 | 52, 50 | eqtri 2644 |
. . . . . . . . . 10
⊢ (ℂ
D ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ 1) |
92 | 91 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (ℂ
D ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ 1)) |
93 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
94 | 73, 62, 66, 92, 93 | offval2 6914 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((ℂ
D ( I ↾ ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑𝑘)))) |
95 | 68 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (1
· (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
96 | 94, 95 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((ℂ
D ( I ↾ ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) |
97 | 73, 74, 66, 90, 96 | offval2 6914 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘𝑓
· ( I ↾ ℂ)) ∘𝑓 + ((ℂ D ( I
↾ ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘)))) |
98 | 71, 97 | eqtr4d 2659 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘𝑓
· ( I ↾ ℂ)) ∘𝑓 + ((ℂ D ( I
↾ ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
99 | | oveq1 6657 |
. . . . . . 7
⊢ ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘𝑓 · ( I
↾ ℂ)) = ((𝑥
∈ ℂ ↦ (𝑘
· (𝑥↑(𝑘 − 1))))
∘𝑓 · ( I ↾ ℂ))) |
100 | 99 | oveq1d 6665 |
. . . . . 6
⊢ ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘𝑓 · ( I
↾ ℂ)) ∘𝑓 + ((ℂ D ( I ↾
ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘𝑓
· ( I ↾ ℂ)) ∘𝑓 + ((ℂ D ( I
↾ ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
101 | 100 | eqcomd 2628 |
. . . . 5
⊢ ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘𝑓
· ( I ↾ ℂ)) ∘𝑓 + ((ℂ D ( I
↾ ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘𝑓 · ( I
↾ ℂ)) ∘𝑓 + ((ℂ D ( I ↾
ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
102 | 98, 101 | sylan9eq 2676 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘𝑓 · ( I
↾ ℂ)) ∘𝑓 + ((ℂ D ( I ↾
ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
103 | | cnelprrecn 10029 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
104 | 103 | a1i 11 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → ℂ ∈
{ℝ, ℂ}) |
105 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) |
106 | 66, 105 | fmptd 6385 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)):ℂ⟶ℂ) |
107 | 106 | adantr 481 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)):ℂ⟶ℂ) |
108 | | f1oi 6174 |
. . . . . 6
⊢ ( I
↾ ℂ):ℂ–1-1-onto→ℂ |
109 | | f1of 6137 |
. . . . . 6
⊢ (( I
↾ ℂ):ℂ–1-1-onto→ℂ → ( I ↾
ℂ):ℂ⟶ℂ) |
110 | 108, 109 | mp1i 13 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → ( I ↾
ℂ):ℂ⟶ℂ) |
111 | | simpr 477 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
112 | 111 | dmeqd 5326 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = dom (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) |
113 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) |
114 | 78, 113 | fmptd 6385 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 −
1)))):ℂ⟶ℂ) |
115 | 114 | adantr 481 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 −
1)))):ℂ⟶ℂ) |
116 | | fdm 6051 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))):ℂ⟶ℂ →
dom (𝑥 ∈ ℂ
↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = ℂ) |
117 | 115, 116 | syl 17 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = ℂ) |
118 | 112, 117 | eqtrd 2656 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = ℂ) |
119 | | 1ex 10035 |
. . . . . . . . 9
⊢ 1 ∈
V |
120 | 119 | fconst 6091 |
. . . . . . . 8
⊢ (ℂ
× {1}):ℂ⟶{1} |
121 | 52 | feq1i 6036 |
. . . . . . . 8
⊢ ((ℂ
D ( I ↾ ℂ)):ℂ⟶{1} ↔ (ℂ ×
{1}):ℂ⟶{1}) |
122 | 120, 121 | mpbir 221 |
. . . . . . 7
⊢ (ℂ
D ( I ↾ ℂ)):ℂ⟶{1} |
123 | 122 | fdmi 6052 |
. . . . . 6
⊢ dom
(ℂ D ( I ↾ ℂ)) = ℂ |
124 | 123 | a1i 11 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D ( I
↾ ℂ)) = ℂ) |
125 | 104, 107,
110, 118, 124 | dvmulf 23706 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘𝑓 · ( I
↾ ℂ))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘𝑓 · ( I
↾ ℂ)) ∘𝑓 + ((ℂ D ( I ↾
ℂ)) ∘𝑓 · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))) |
126 | 73, 66, 79, 93, 82 | offval2 6914 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘𝑓 · ( I
↾ ℂ)) = (𝑥
∈ ℂ ↦ ((𝑥↑𝑘) · 𝑥))) |
127 | | expp1 12867 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑥↑(𝑘 + 1)) = ((𝑥↑𝑘) · 𝑥)) |
128 | 63, 64, 127 | syl2anr 495 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑘 + 1)) = ((𝑥↑𝑘) · 𝑥)) |
129 | 128 | mpteq2dva 4744 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))) = (𝑥 ∈ ℂ ↦ ((𝑥↑𝑘) · 𝑥))) |
130 | 126, 129 | eqtr4d 2659 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘𝑓 · ( I
↾ ℂ)) = (𝑥
∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) |
131 | 130 | oveq2d 6666 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (ℂ
D ((𝑥 ∈ ℂ
↦ (𝑥↑𝑘)) ∘𝑓
· ( I ↾ ℂ))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))) |
132 | 131 | adantr 481 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘𝑓 · ( I
↾ ℂ))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))) |
133 | 102, 125,
132 | 3eqtr2rd 2663 |
. . 3
⊢ ((𝑘 ∈ ℕ ∧ (ℂ D
(𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))))) |
134 | 133 | ex 450 |
. 2
⊢ (𝑘 ∈ ℕ → ((ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))))) |
135 | 9, 18, 27, 36, 54, 134 | nnind 11038 |
1
⊢ (𝑁 ∈ ℕ → (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) |