Step | Hyp | Ref
| Expression |
1 | | itgpowd.4 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | nn0p1nn 11538 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
4 | 3 | nncnd 11241 |
. 2
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
5 | | itgpowd.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | | itgpowd.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | iccssre 12459 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
8 | 5, 6, 7 | syl2anc 573 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
9 | | ax-resscn 10198 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
10 | 8, 9 | syl6ss 3764 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
11 | 10 | sselda 3752 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
12 | 1 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑁 ∈
ℕ0) |
13 | 11, 12 | expcld 13214 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥↑𝑁) ∈ ℂ) |
14 | 10 | resmptd 5592 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁))) |
15 | | expcncf 22944 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈ ℂ
↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) |
17 | | rescncf 22919 |
. . . . . 6
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
18 | 10, 16, 17 | sylc 65 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
19 | 14, 18 | eqeltrrd 2851 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
20 | | cniccibl 23826 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈
𝐿1) |
21 | 5, 6, 19, 20 | syl3anc 1476 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈
𝐿1) |
22 | 13, 21 | itgcl 23769 |
. 2
⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 ∈ ℂ) |
23 | 3 | nnne0d 11270 |
. 2
⊢ (𝜑 → (𝑁 + 1) ≠ 0) |
24 | 4, 13, 21 | itgmulc2 23819 |
. . 3
⊢ (𝜑 → ((𝑁 + 1) · ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥) = ∫(𝐴[,]𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥) |
25 | | eqidd 2772 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
26 | | oveq1 6802 |
. . . . . . . 8
⊢ (𝑡 = 𝑥 → (𝑡↑𝑁) = (𝑥↑𝑁)) |
27 | 26 | oveq2d 6811 |
. . . . . . 7
⊢ (𝑡 = 𝑥 → ((𝑁 + 1) · (𝑡↑𝑁)) = ((𝑁 + 1) · (𝑥↑𝑁))) |
28 | 27 | adantl 467 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑡 = 𝑥) → ((𝑁 + 1) · (𝑡↑𝑁)) = ((𝑁 + 1) · (𝑥↑𝑁))) |
29 | | simpr 471 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
30 | 4 | adantr 466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑁 + 1) ∈ ℂ) |
31 | | ioossicc 12463 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
33 | 32 | sselda 3752 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
34 | 33, 13 | syldan 579 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥↑𝑁) ∈ ℂ) |
35 | 30, 34 | mulcld 10265 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝑁 + 1) · (𝑥↑𝑁)) ∈ ℂ) |
36 | 25, 28, 29, 35 | fvmptd 6432 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) = ((𝑁 + 1) · (𝑥↑𝑁))) |
37 | 36 | itgeq2dv 23767 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥) |
38 | | itgpowd.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
39 | | reelprrecn 10233 |
. . . . . . . . 9
⊢ ℝ
∈ {ℝ, ℂ} |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
41 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
42 | 41 | sselda 3752 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ) |
43 | | 1nn0 11514 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ0) |
45 | 1, 44 | nn0addcld 11561 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
46 | 45 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑁 + 1) ∈
ℕ0) |
47 | 42, 46 | expcld 13214 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑡↑(𝑁 + 1)) ∈ ℂ) |
48 | 1 | nn0cnd 11559 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
49 | 48 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ∈ ℂ) |
50 | | 1cnd 10261 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈
ℂ) |
51 | 49, 50 | addcld 10264 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑁 + 1) ∈ ℂ) |
52 | 1 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ∈
ℕ0) |
53 | 42, 52 | expcld 13214 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑡↑𝑁) ∈ ℂ) |
54 | 51, 53 | mulcld 10265 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝑁 + 1) · (𝑡↑𝑁)) ∈ ℂ) |
55 | | simpr 471 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → 𝑡 ∈ ℂ) |
56 | 45 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑁 + 1) ∈
ℕ0) |
57 | 55, 56 | expcld 13214 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑡↑(𝑁 + 1)) ∈ ℂ) |
58 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) = (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) |
59 | 57, 58 | fmptd 6529 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 +
1))):ℂ⟶ℂ) |
60 | | ssid 3773 |
. . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ |
61 | 60 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℂ ⊆
ℂ) |
62 | 4 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑁 + 1) ∈ ℂ) |
63 | 1 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → 𝑁 ∈
ℕ0) |
64 | 55, 63 | expcld 13214 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑡↑𝑁) ∈ ℂ) |
65 | 62, 64 | mulcld 10265 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → ((𝑁 + 1) · (𝑡↑𝑁)) ∈ ℂ) |
66 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) |
67 | 65, 66 | fmptd 6529 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))):ℂ⟶ℂ) |
68 | | dvexp 23935 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ∈ ℕ →
(ℂ D (𝑡 ∈
ℂ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1))))) |
69 | 3, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1))))) |
70 | | 1cnd 10261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℂ) |
71 | 48, 70 | pncand 10598 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
72 | 71 | oveq2d 6811 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡↑((𝑁 + 1) − 1)) = (𝑡↑𝑁)) |
73 | 72 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1))) = ((𝑁 + 1) · (𝑡↑𝑁))) |
74 | 73 | mpteq2dv 4880 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
75 | 69, 74 | eqtrd 2805 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
76 | 75 | feq1d 6169 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))):ℂ⟶ℂ ↔
(𝑡 ∈ ℂ ↦
((𝑁 + 1) · (𝑡↑𝑁))):ℂ⟶ℂ)) |
77 | 67, 76 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 +
1)))):ℂ⟶ℂ) |
78 | 77 | fdmd 6193 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) = ℂ) |
79 | 9, 78 | syl5sseqr 3803 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑡 ∈
ℂ ↦ (𝑡↑(𝑁 + 1))))) |
80 | | dvres3 23896 |
. . . . . . . . . . 11
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))):ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))))) → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = ((ℂ D
(𝑡 ∈ ℂ ↦
(𝑡↑(𝑁 + 1)))) ↾ ℝ)) |
81 | 40, 59, 61, 79, 80 | syl22anc 1477 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = ((ℂ D
(𝑡 ∈ ℂ ↦
(𝑡↑(𝑁 + 1)))) ↾ ℝ)) |
82 | 75 | reseq1d 5532 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) ↾ ℝ) = ((𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ↾ ℝ)) |
83 | 81, 82 | eqtrd 2805 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = ((𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ↾ ℝ)) |
84 | | resmpt 5589 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ((𝑡
∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ (𝑡↑(𝑁 + 1)))) |
85 | 9, 84 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ (𝑡↑(𝑁 + 1)))) |
86 | 85 | oveq2d 6811 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = (ℝ D
(𝑡 ∈ ℝ ↦
(𝑡↑(𝑁 + 1))))) |
87 | | resmpt 5589 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ → ((𝑡
∈ ℂ ↦ ((𝑁
+ 1) · (𝑡↑𝑁))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
88 | 9, 87 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
89 | 83, 86, 88 | 3eqtr3d 2813 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℝ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
90 | | eqid 2771 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
91 | 90 | tgioo2 22825 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
92 | | iccntr 22843 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
93 | 5, 6, 92 | syl2anc 573 |
. . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
94 | 40, 47, 54, 89, 8, 91, 90, 93 | dvmptres2 23944 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
95 | | ioossre 12439 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ⊆ ℝ |
96 | 95, 9 | sstri 3761 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ ℂ |
97 | 96 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
98 | | cncfmptc 22933 |
. . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℂ ∧
(𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴(,)𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
99 | 4, 97, 61, 98 | syl3anc 1476 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
100 | | resmpt 5589 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡↑𝑁))) |
101 | 96, 100 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡↑𝑁))) |
102 | | expcncf 22944 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑡 ∈ ℂ
↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ)) |
103 | 1, 102 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ)) |
104 | | rescncf 22919 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
105 | 97, 103, 104 | sylc 65 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
106 | 101, 105 | eqeltrrd 2851 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡↑𝑁)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
107 | 99, 106 | mulcncf 23433 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
108 | 94, 107 | eqeltrd 2850 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
109 | | ioombl 23552 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ∈ dom vol |
110 | 109 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
111 | 48 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑁 ∈ ℂ) |
112 | | 1cnd 10261 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ) |
113 | 111, 112 | addcld 10264 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑁 + 1) ∈ ℂ) |
114 | 10 | sselda 3752 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℂ) |
115 | 1 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑁 ∈
ℕ0) |
116 | 114, 115 | expcld 13214 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡↑𝑁) ∈ ℂ) |
117 | 113, 116 | mulcld 10265 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → ((𝑁 + 1) · (𝑡↑𝑁)) ∈ ℂ) |
118 | | cncfmptc 22933 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℂ ∧
(𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴[,]𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
119 | 4, 10, 61, 118 | syl3anc 1476 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
120 | 10 | resmptd 5592 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑𝑁))) |
121 | | rescncf 22919 |
. . . . . . . . . . . 12
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
122 | 10, 103, 121 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
123 | 120, 122 | eqeltrrd 2851 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑𝑁)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
124 | 119, 123 | mulcncf 23433 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
125 | | cniccibl 23826 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈
𝐿1) |
126 | 5, 6, 124, 125 | syl3anc 1476 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈
𝐿1) |
127 | 32, 110, 117, 126 | iblss 23790 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈
𝐿1) |
128 | 94, 127 | eqeltrd 2850 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) ∈
𝐿1) |
129 | 10 | resmptd 5592 |
. . . . . . 7
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) |
130 | | expcncf 22944 |
. . . . . . . . 9
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑡 ∈ ℂ
↦ (𝑡↑(𝑁 + 1))) ∈
(ℂ–cn→ℂ)) |
131 | 45, 130 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ∈ (ℂ–cn→ℂ)) |
132 | | rescncf 22919 |
. . . . . . . 8
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
133 | 10, 131, 132 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
134 | 129, 133 | eqeltrrd 2851 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
135 | 5, 6, 38, 108, 128, 134 | ftc2 24026 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) d𝑥 = (((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐵) − ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐴))) |
136 | 94 | fveq1d 6335 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥)) |
137 | 136 | ralrimivw 3116 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥)) |
138 | | itgeq2 23763 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) → ∫(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥) |
139 | 137, 138 | syl 17 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥) |
140 | | eqidd 2772 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) |
141 | | simpr 471 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 𝐵) → 𝑡 = 𝐵) |
142 | 141 | oveq1d 6810 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 𝐵) → (𝑡↑(𝑁 + 1)) = (𝐵↑(𝑁 + 1))) |
143 | 5 | rexrd 10294 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
144 | 6 | rexrd 10294 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
145 | | ubicc2 12495 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
146 | 143, 144,
38, 145 | syl3anc 1476 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
147 | 6 | recnd 10273 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
148 | 147, 45 | expcld 13214 |
. . . . . . 7
⊢ (𝜑 → (𝐵↑(𝑁 + 1)) ∈ ℂ) |
149 | 140, 142,
146, 148 | fvmptd 6432 |
. . . . . 6
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐵) = (𝐵↑(𝑁 + 1))) |
150 | | simpr 471 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 𝐴) → 𝑡 = 𝐴) |
151 | 150 | oveq1d 6810 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 𝐴) → (𝑡↑(𝑁 + 1)) = (𝐴↑(𝑁 + 1))) |
152 | | lbicc2 12494 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
153 | 143, 144,
38, 152 | syl3anc 1476 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
154 | 5 | recnd 10273 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
155 | 154, 45 | expcld 13214 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑(𝑁 + 1)) ∈ ℂ) |
156 | 140, 151,
153, 155 | fvmptd 6432 |
. . . . . 6
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐴) = (𝐴↑(𝑁 + 1))) |
157 | 149, 156 | oveq12d 6813 |
. . . . 5
⊢ (𝜑 → (((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐵) − ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐴)) = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
158 | 135, 139,
157 | 3eqtr3d 2813 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥 = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
159 | 4 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑁 + 1) ∈ ℂ) |
160 | 159, 13 | mulcld 10265 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑁 + 1) · (𝑥↑𝑁)) ∈ ℂ) |
161 | 5, 6, 160 | itgioo 23801 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥 = ∫(𝐴[,]𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥) |
162 | 37, 158, 161 | 3eqtr3rd 2814 |
. . 3
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥 = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
163 | 24, 162 | eqtrd 2805 |
. 2
⊢ (𝜑 → ((𝑁 + 1) · ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥) = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
164 | 4, 22, 23, 163 | mvllmuld 11062 |
1
⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1))) |