dvexp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvexp		Structured version Visualization version GIF version

Theorem dvexp 25909

Description: Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)

**Assertion**
Ref	Expression
dvexp	⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))

Distinct variable group: 𝑥,𝑁

Proof of Theorem dvexp Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7413	. . . . 5 ⊢ (𝑛 = 1 → (𝑥↑𝑛) = (𝑥↑1))
2	1	mpteq2dv 5215	. . . 4 ⊢ (𝑛 = 1 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑1)))
3	2	oveq2d 7421	. . 3 ⊢ (𝑛 = 1 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1))))
4		id 22	. . . . 5 ⊢ (𝑛 = 1 → 𝑛 = 1)
5		oveq1 7412	. . . . . 6 ⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
6	5	oveq2d 7421	. . . . 5 ⊢ (𝑛 = 1 → (𝑥↑(𝑛 − 1)) = (𝑥↑(1 − 1)))
7	4, 6	oveq12d 7423	. . . 4 ⊢ (𝑛 = 1 → (𝑛 · (𝑥↑(𝑛 − 1))) = (1 · (𝑥↑(1 − 1))))
8	7	mpteq2dv 5215	. . 3 ⊢ (𝑛 = 1 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 − 1)))))
9	3, 8	eqeq12d 2751	. 2 ⊢ (𝑛 = 1 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 − 1))))))
10		oveq2 7413	. . . . 5 ⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘))
11	10	mpteq2dv 5215	. . . 4 ⊢ (𝑛 = 𝑘 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))
12	11	oveq2d 7421	. . 3 ⊢ (𝑛 = 𝑘 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))))
13		id 22	. . . . 5 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
14		oveq1 7412	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1))
15	14	oveq2d 7421	. . . . 5 ⊢ (𝑛 = 𝑘 → (𝑥↑(𝑛 − 1)) = (𝑥↑(𝑘 − 1)))
16	13, 15	oveq12d 7423	. . . 4 ⊢ (𝑛 = 𝑘 → (𝑛 · (𝑥↑(𝑛 − 1))) = (𝑘 · (𝑥↑(𝑘 − 1))))
17	16	mpteq2dv 5215	. . 3 ⊢ (𝑛 = 𝑘 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))))
18	12, 17	eqeq12d 2751	. 2 ⊢ (𝑛 = 𝑘 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))))
19		oveq2 7413	. . . . 5 ⊢ (𝑛 = (𝑘 + 1) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1)))
20	19	mpteq2dv 5215	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))
21	20	oveq2d 7421	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))))
22		id 22	. . . . 5 ⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
23		oveq1 7412	. . . . . 6 ⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1))
24	23	oveq2d 7421	. . . . 5 ⊢ (𝑛 = (𝑘 + 1) → (𝑥↑(𝑛 − 1)) = (𝑥↑((𝑘 + 1) − 1)))
25	22, 24	oveq12d 7423	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (𝑛 · (𝑥↑(𝑛 − 1))) = ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))))
26	25	mpteq2dv 5215	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))))
27	21, 26	eqeq12d 2751	. 2 ⊢ (𝑛 = (𝑘 + 1) → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))))))
28		oveq2 7413	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑥↑𝑛) = (𝑥↑𝑁))
29	28	mpteq2dv 5215	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑛)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)))
30	29	oveq2d 7421	. . 3 ⊢ (𝑛 = 𝑁 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))))
31		id 22	. . . . 5 ⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁)
32		oveq1 7412	. . . . . 6 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
33	32	oveq2d 7421	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑥↑(𝑛 − 1)) = (𝑥↑(𝑁 − 1)))
34	31, 33	oveq12d 7423	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 · (𝑥↑(𝑛 − 1))) = (𝑁 · (𝑥↑(𝑁 − 1))))
35	34	mpteq2dv 5215	. . 3 ⊢ (𝑛 = 𝑁 → (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
36	30, 35	eqeq12d 2751	. 2 ⊢ (𝑛 = 𝑁 → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑛))) = (𝑥 ∈ ℂ ↦ (𝑛 · (𝑥↑(𝑛 − 1)))) ↔ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))))
37		exp1 14085	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
38	37	mpteq2ia 5216	. . . . 5 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑1)) = (𝑥 ∈ ℂ ↦ 𝑥)
39		mptresid 6038	. . . . 5 ⊢ ( I ↾ ℂ) = (𝑥 ∈ ℂ ↦ 𝑥)
40	38, 39	eqtr4i 2761	. . . 4 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑1)) = ( I ↾ ℂ)
41	40	oveq2i 7416	. . 3 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1))) = (ℂ D ( I ↾ ℂ))
42		1m1e0 12312	. . . . . . . . . 10 ⊢ (1 − 1) = 0
43	42	oveq2i 7416	. . . . . . . . 9 ⊢ (𝑥↑(1 − 1)) = (𝑥↑0)
44		exp0 14083	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (𝑥↑0) = 1)
45	43, 44	eqtrid 2782	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (𝑥↑(1 − 1)) = 1)
46	45	oveq2d 7421	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → (1 · (𝑥↑(1 − 1))) = (1 · 1))
47		1t1e1 12402	. . . . . . 7 ⊢ (1 · 1) = 1
48	46, 47	eqtrdi 2786	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (1 · (𝑥↑(1 − 1))) = 1)
49	48	mpteq2ia 5216	. . . . 5 ⊢ (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 − 1)))) = (𝑥 ∈ ℂ ↦ 1)
50		fconstmpt 5716	. . . . 5 ⊢ (ℂ × {1}) = (𝑥 ∈ ℂ ↦ 1)
51	49, 50	eqtr4i 2761	. . . 4 ⊢ (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 − 1)))) = (ℂ × {1})
52		dvid 25871	. . . 4 ⊢ (ℂ D ( I ↾ ℂ)) = (ℂ × {1})
53	51, 52	eqtr4i 2761	. . 3 ⊢ (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 − 1)))) = (ℂ D ( I ↾ ℂ))
54	41, 53	eqtr4i 2761	. 2 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑1))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑(1 − 1))))
55		nncn 12248	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
56	55	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 𝑘 ∈ ℂ)
57		ax-1cn 11187	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
58		pncan 11488	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
59	56, 57, 58	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
60	59	oveq2d 7421	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑((𝑘 + 1) − 1)) = (𝑥↑𝑘))
61	60	oveq2d 7421	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑥↑𝑘)))
62	57	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
63		id 22	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
64		nnnn0 12508	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
65		expcl 14097	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑥↑𝑘) ∈ ℂ)
66	63, 64, 65	syl2anr 597	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑘) ∈ ℂ)
67	56, 62, 66	adddird 11260	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑𝑘)) = ((𝑘 · (𝑥↑𝑘)) + (1 · (𝑥↑𝑘))))
68	66	mullidd 11253	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (1 · (𝑥↑𝑘)) = (𝑥↑𝑘))
69	68	oveq2d 7421	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑𝑘)) + (1 · (𝑥↑𝑘))) = ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘)))
70	61, 67, 69	3eqtrd 2774	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1))) = ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘)))
71	70	mpteq2dva 5214	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘))))
72		cnex 11210	. . . . . . . 8 ⊢ ℂ ∈ V
73	72	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ℂ ∈ V)
74	56, 66	mulcld 11255	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑𝑘)) ∈ ℂ)
75		nnm1nn0 12542	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
76		expcl 14097	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ (𝑘 − 1) ∈ ℕ₀) → (𝑥↑(𝑘 − 1)) ∈ ℂ)
77	63, 75, 76	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑘 − 1)) ∈ ℂ)
78	56, 77	mulcld 11255	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑(𝑘 − 1))) ∈ ℂ)
79		simpr 484	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
80		eqidd 2736	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))))
81	39	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ( I ↾ ℂ) = (𝑥 ∈ ℂ ↦ 𝑥))
82	73, 78, 79, 80, 81	offval2 7691	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥)))
83	56, 77, 79	mulassd 11258	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥) = (𝑘 · ((𝑥↑(𝑘 − 1)) · 𝑥)))
84		expm1t 14108	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝑥↑𝑘) = ((𝑥↑(𝑘 − 1)) · 𝑥))
85	84	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑘) = ((𝑥↑(𝑘 − 1)) · 𝑥))
86	85	oveq2d 7421	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑘 · (𝑥↑𝑘)) = (𝑘 · ((𝑥↑(𝑘 − 1)) · 𝑥)))
87	83, 86	eqtr4d 2773	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥) = (𝑘 · (𝑥↑𝑘)))
88	87	mpteq2dva 5214	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑(𝑘 − 1))) · 𝑥)) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑𝑘))))
89	82, 88	eqtrd 2770	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑𝑘))))
90	52, 50	eqtri 2758	. . . . . . . . . 10 ⊢ (ℂ D ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ 1)
91	90	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (ℂ D ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ 1))
92		eqidd 2736	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))
93	73, 62, 66, 91, 92	offval2 7691	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑𝑘))))
94	68	mpteq2dva 5214	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (1 · (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))
95	93, 94	eqtrd 2770	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))
96	73, 74, 66, 89, 95	offval2 7691	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (𝑥 ∈ ℂ ↦ ((𝑘 · (𝑥↑𝑘)) + (𝑥↑𝑘))))
97	71, 96	eqtr4d 2773	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))))
98		oveq1 7412	. . . . . . 7 ⊢ ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘_f · ( I ↾ ℂ)) = ((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)))
99	98	oveq1d 7420	. . . . . 6 ⊢ ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))))
100	99	eqcomd 2741	. . . . 5 ⊢ ((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) → (((𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))))
101	97, 100	sylan9eq 2790	. . . 4 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ ((𝑘 + 1) · (𝑥↑((𝑘 + 1) − 1)))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))))
102		cnelprrecn 11222	. . . . . 6 ⊢ ℂ ∈ {ℝ, ℂ}
103	102	a1i 11	. . . . 5 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → ℂ ∈ {ℝ, ℂ})
104	66	fmpttd 7105	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)):ℂ⟶ℂ)
105	104	adantr 480	. . . . 5 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)):ℂ⟶ℂ)
106		f1oi 6856	. . . . . 6 ⊢ ( I ↾ ℂ):ℂ–1-1-onto→ℂ
107		f1of 6818	. . . . . 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 5885	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = dom (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))))
111	78	fmpttd 7105	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))):ℂ⟶ℂ)
112	111	adantr 480	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))):ℂ⟶ℂ)
113	112	fdmd 6716	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1)))) = ℂ)
114	110, 113	eqtrd 2770	. . . . 5 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = ℂ)
115		1ex 11231	. . . . . . . . 9 ⊢ 1 ∈ V
116	115	fconst 6764	. . . . . . . 8 ⊢ (ℂ × {1}):ℂ⟶{1}
117	52	feq1i 6697	. . . . . . . 8 ⊢ ((ℂ D ( I ↾ ℂ)):ℂ⟶{1} ↔ (ℂ × {1}):ℂ⟶{1})
118	116, 117	mpbir 231	. . . . . . 7 ⊢ (ℂ D ( I ↾ ℂ)):ℂ⟶{1}
119	118	fdmi 6717	. . . . . 6 ⊢ dom (ℂ D ( I ↾ ℂ)) = ℂ
120	119	a1i 11	. . . . 5 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → dom (ℂ D ( I ↾ ℂ)) = ℂ)
121	103, 105, 108, 114, 120	dvmulf 25898	. . . 4 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘_f · ( I ↾ ℂ))) = (((ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) ∘_f · ( I ↾ ℂ)) ∘_f + ((ℂ D ( I ↾ ℂ)) ∘_f · (𝑥 ∈ ℂ ↦ (𝑥↑𝑘)))))
122	73, 66, 79, 92, 81	offval2 7691	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘_f · ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ ((𝑥↑𝑘) · 𝑥)))
123		expp1 14086	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑥↑(𝑘 + 1)) = ((𝑥↑𝑘) · 𝑥))
124	63, 64, 123	syl2anr 597	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑘 + 1)) = ((𝑥↑𝑘) · 𝑥))
125	124	mpteq2dva 5214	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))) = (𝑥 ∈ ℂ ↦ ((𝑥↑𝑘) · 𝑥)))
126	122, 125	eqtr4d 2773	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘_f · ( I ↾ ℂ)) = (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1))))
127	126	oveq2d 7421	. . . . 5 ⊢ (𝑘 ∈ ℕ → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘_f · ( I ↾ ℂ))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))))
128	127	adantr 480	. . . 4 ⊢ ((𝑘 ∈ ℕ ∧ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑘))) = (𝑥 ∈ ℂ ↦ (𝑘 · (𝑥↑(𝑘 − 1))))) → (ℂ D ((𝑥 ∈ ℂ ↦ (𝑥↑𝑘)) ∘_f · ( I ↾ ℂ))) = (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑘 + 1)))))
129	101, 121, 128	3eqtr2rd 2777	. . 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 12258	1 ⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3459 {csn 4601 {cpr 4603 ↦ cmpt 5201 I cid 5547 × cxp 5652 dom cdm 5654 ↾ cres 5656 ⟶wf 6527 –1-1-onto→wf1o 6530 (class class class)co 7405 ∘_f cof 7669 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 − cmin 11466 ℕcn 12240 ℕ₀cn0 12501 ↑cexp 14079 D cdv 25816

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207 ax-addf 11208

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7671 df-om 7862 df-1st 7988 df-2nd 7989 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-er 8719 df-map 8842 df-pm 8843 df-ixp 8912 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fsupp 9374 df-fi 9423 df-sup 9454 df-inf 9455 df-oi 9524 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-z 12589 df-dec 12709 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-icc 13369 df-fz 13525 df-fzo 13672 df-seq 14020 df-exp 14080 df-hash 14349 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-starv 17286 df-sca 17287 df-vsca 17288 df-ip 17289 df-tset 17290 df-ple 17291 df-ds 17293 df-unif 17294 df-hom 17295 df-cco 17296 df-rest 17436 df-topn 17437 df-0g 17455 df-gsum 17456 df-topgen 17457 df-pt 17458 df-prds 17461 df-xrs 17516 df-qtop 17521 df-imas 17522 df-xps 17524 df-mre 17598 df-mrc 17599 df-acs 17601 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-submnd 18762 df-mulg 19051 df-cntz 19300 df-cmn 19763 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-fbas 21312 df-fg 21313 df-cnfld 21316 df-top 22832 df-topon 22849 df-topsp 22871 df-bases 22884 df-cld 22957 df-ntr 22958 df-cls 22959 df-nei 23036 df-lp 23074 df-perf 23075 df-cn 23165 df-cnp 23166 df-haus 23253 df-tx 23500 df-hmeo 23693 df-fil 23784 df-fm 23876 df-flim 23877 df-flf 23878 df-xms 24259 df-ms 24260 df-tms 24261 df-cncf 24822 df-limc 25819 df-dv 25820

This theorem is referenced by: dvexp2 25910 dvexp3 25934 itgpowd 26009 taylthlem2 26334 taylthlem2OLD 26335 advlogexp 26616 logdivsum 27496 log2sumbnd 27507 dvasin 37728 areacirclem1 37732 lcmineqlem8 42049 lcmineqlem10 42051 lcmineqlem12 42053 dvrelogpow2b 42081 aks4d1p1p6 42086 readvrec2 42404 lhe4.4ex1a 44353 dvsinexp 45940 dvxpaek 45969

W3C validator