| Step | Hyp | Ref
| Expression |
| 1 | | itgpowd.4 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | | nn0p1nn 12565 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
| 4 | 3 | nncnd 12282 |
. 2
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
| 5 | | itgpowd.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 6 | | itgpowd.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 7 | | iccssre 13469 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
| 8 | 5, 6, 7 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 9 | | ax-resscn 11212 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
| 10 | 8, 9 | sstrdi 3996 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
| 11 | 10 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
| 12 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑁 ∈
ℕ0) |
| 13 | 11, 12 | expcld 14186 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥↑𝑁) ∈ ℂ) |
| 14 | 10 | resmptd 6058 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁))) |
| 15 | | expcncf 24953 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈ ℂ
↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 17 | | rescncf 24923 |
. . . . . 6
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
| 18 | 10, 16, 17 | sylc 65 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 19 | 14, 18 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 20 | | cnicciblnc 25878 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈
𝐿1) |
| 21 | 5, 6, 19, 20 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥↑𝑁)) ∈
𝐿1) |
| 22 | 13, 21 | itgcl 25819 |
. 2
⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 ∈ ℂ) |
| 23 | 3 | nnne0d 12316 |
. 2
⊢ (𝜑 → (𝑁 + 1) ≠ 0) |
| 24 | 4, 13, 21 | itgmulc2 25869 |
. . 3
⊢ (𝜑 → ((𝑁 + 1) · ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥) = ∫(𝐴[,]𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥) |
| 25 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 26 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑡 = 𝑥 → (𝑡↑𝑁) = (𝑥↑𝑁)) |
| 27 | 26 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = 𝑥 → ((𝑁 + 1) · (𝑡↑𝑁)) = ((𝑁 + 1) · (𝑥↑𝑁))) |
| 28 | 27 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑡 = 𝑥) → ((𝑁 + 1) · (𝑡↑𝑁)) = ((𝑁 + 1) · (𝑥↑𝑁))) |
| 29 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
| 30 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑁 + 1) ∈ ℂ) |
| 31 | | ioossicc 13473 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
| 33 | 32 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
| 34 | 33, 13 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥↑𝑁) ∈ ℂ) |
| 35 | 30, 34 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝑁 + 1) · (𝑥↑𝑁)) ∈ ℂ) |
| 36 | 25, 28, 29, 35 | fvmptd 7023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) = ((𝑁 + 1) · (𝑥↑𝑁))) |
| 37 | 36 | itgeq2dv 25817 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥) |
| 38 | | itgpowd.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 39 | | reelprrecn 11247 |
. . . . . . . . 9
⊢ ℝ
∈ {ℝ, ℂ} |
| 40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 41 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 42 | 41 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ) |
| 43 | | 1nn0 12542 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
| 44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ0) |
| 45 | 1, 44 | nn0addcld 12591 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
| 46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑁 + 1) ∈
ℕ0) |
| 47 | 42, 46 | expcld 14186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑡↑(𝑁 + 1)) ∈ ℂ) |
| 48 | 1 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 49 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ∈ ℂ) |
| 50 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈
ℂ) |
| 51 | 49, 50 | addcld 11280 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑁 + 1) ∈ ℂ) |
| 52 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ∈
ℕ0) |
| 53 | 42, 52 | expcld 14186 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑡↑𝑁) ∈ ℂ) |
| 54 | 51, 53 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝑁 + 1) · (𝑡↑𝑁)) ∈ ℂ) |
| 55 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → 𝑡 ∈ ℂ) |
| 56 | 45 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑁 + 1) ∈
ℕ0) |
| 57 | 55, 56 | expcld 14186 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑡↑(𝑁 + 1)) ∈ ℂ) |
| 58 | 57 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 +
1))):ℂ⟶ℂ) |
| 59 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 60 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑁 + 1) ∈ ℂ) |
| 61 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → 𝑁 ∈
ℕ0) |
| 62 | 55, 61 | expcld 14186 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑡↑𝑁) ∈ ℂ) |
| 63 | 60, 62 | mulcld 11281 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → ((𝑁 + 1) · (𝑡↑𝑁)) ∈ ℂ) |
| 64 | 63 | fmpttd 7135 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))):ℂ⟶ℂ) |
| 65 | | dvexp 25991 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ∈ ℕ →
(ℂ D (𝑡 ∈
ℂ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1))))) |
| 66 | 3, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1))))) |
| 67 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℂ) |
| 68 | 48, 67 | pncand 11621 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
| 69 | 68 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡↑((𝑁 + 1) − 1)) = (𝑡↑𝑁)) |
| 70 | 69 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1))) = ((𝑁 + 1) · (𝑡↑𝑁))) |
| 71 | 70 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑((𝑁 + 1) − 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 72 | 66, 71 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 73 | 72 | feq1d 6720 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))):ℂ⟶ℂ ↔
(𝑡 ∈ ℂ ↦
((𝑁 + 1) · (𝑡↑𝑁))):ℂ⟶ℂ)) |
| 74 | 64, 73 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 +
1)))):ℂ⟶ℂ) |
| 75 | 74 | fdmd 6746 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) = ℂ) |
| 76 | 9, 75 | sseqtrrid 4027 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑡 ∈
ℂ ↦ (𝑡↑(𝑁 + 1))))) |
| 77 | | dvres3 25948 |
. . . . . . . . . . 11
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))):ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))))) → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = ((ℂ D
(𝑡 ∈ ℂ ↦
(𝑡↑(𝑁 + 1)))) ↾ ℝ)) |
| 78 | 40, 58, 59, 76, 77 | syl22anc 839 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = ((ℂ D
(𝑡 ∈ ℂ ↦
(𝑡↑(𝑁 + 1)))) ↾ ℝ)) |
| 79 | 72 | reseq1d 5996 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂ D (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1)))) ↾ ℝ) = ((𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ↾ ℝ)) |
| 80 | 78, 79 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = ((𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ↾ ℝ)) |
| 81 | | resmpt 6055 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ((𝑡
∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ (𝑡↑(𝑁 + 1)))) |
| 82 | 9, 81 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ (𝑡↑(𝑁 + 1)))) |
| 83 | 82 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ ℝ)) = (ℝ D
(𝑡 ∈ ℝ ↦
(𝑡↑(𝑁 + 1))))) |
| 84 | | resmpt 6055 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ → ((𝑡
∈ ℂ ↦ ((𝑁
+ 1) · (𝑡↑𝑁))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 85 | 9, 84 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ↾ ℝ) = (𝑡 ∈ ℝ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 86 | 80, 83, 85 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ ℝ ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 87 | | tgioo4 24826 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 88 | | eqid 2737 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 89 | | iccntr 24843 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
| 90 | 5, 6, 89 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
| 91 | 40, 47, 54, 86, 8, 87, 88, 90 | dvmptres2 26000 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))) |
| 92 | | ioossre 13448 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 93 | 92, 9 | sstri 3993 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ ℂ |
| 94 | 93 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
| 95 | | cncfmptc 24938 |
. . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℂ ∧
(𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴(,)𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 96 | 4, 94, 59, 95 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 97 | | resmpt 6055 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡↑𝑁))) |
| 98 | 93, 97 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡↑𝑁))) |
| 99 | | expcncf 24953 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑡 ∈ ℂ
↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 100 | 1, 99 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 101 | | rescncf 24923 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
| 102 | 94, 100, 101 | sylc 65 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 103 | 98, 102 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡↑𝑁)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 104 | 96, 103 | mulcncf 25480 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 105 | 91, 104 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 106 | | ioombl 25600 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ∈ dom vol |
| 107 | 106 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
| 108 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑁 ∈ ℂ) |
| 109 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ) |
| 110 | 108, 109 | addcld 11280 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑁 + 1) ∈ ℂ) |
| 111 | 10 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℂ) |
| 112 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑁 ∈
ℕ0) |
| 113 | 111, 112 | expcld 14186 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡↑𝑁) ∈ ℂ) |
| 114 | 110, 113 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → ((𝑁 + 1) · (𝑡↑𝑁)) ∈ ℂ) |
| 115 | | cncfmptc 24938 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℂ ∧
(𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴[,]𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 116 | 4, 10, 59, 115 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑁 + 1)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 117 | 10 | resmptd 6058 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑𝑁))) |
| 118 | | rescncf 24923 |
. . . . . . . . . . . 12
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
| 119 | 10, 100, 118 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑𝑁)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 120 | 117, 119 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑𝑁)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 121 | 116, 120 | mulcncf 25480 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 122 | | cnicciblnc 25878 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈
𝐿1) |
| 123 | 5, 6, 121, 122 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈
𝐿1) |
| 124 | 32, 107, 114, 123 | iblss 25840 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁))) ∈
𝐿1) |
| 125 | 91, 124 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) ∈
𝐿1) |
| 126 | 10 | resmptd 6058 |
. . . . . . 7
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) |
| 127 | | expcncf 24953 |
. . . . . . . . 9
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑡 ∈ ℂ
↦ (𝑡↑(𝑁 + 1))) ∈
(ℂ–cn→ℂ)) |
| 128 | 45, 127 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ∈ (ℂ–cn→ℂ)) |
| 129 | | rescncf 24923 |
. . . . . . . 8
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
| 130 | 10, 128, 129 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡↑(𝑁 + 1))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 131 | 126, 130 | eqeltrrd 2842 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 132 | 5, 6, 38, 105, 125, 131 | ftc2 26085 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) d𝑥 = (((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐵) − ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐴))) |
| 133 | 91 | fveq1d 6908 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥)) |
| 134 | 133 | ralrimivw 3150 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥)) |
| 135 | | itgeq2 25813 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) → ∫(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥) |
| 136 | 134, 135 | syl 17 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))))‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥) |
| 137 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))) |
| 138 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 𝐵) → 𝑡 = 𝐵) |
| 139 | 138 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 𝐵) → (𝑡↑(𝑁 + 1)) = (𝐵↑(𝑁 + 1))) |
| 140 | 5 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 141 | 6 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 142 | | ubicc2 13505 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
| 143 | 140, 141,
38, 142 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
| 144 | 6 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 145 | 144, 45 | expcld 14186 |
. . . . . . 7
⊢ (𝜑 → (𝐵↑(𝑁 + 1)) ∈ ℂ) |
| 146 | 137, 139,
143, 145 | fvmptd 7023 |
. . . . . 6
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐵) = (𝐵↑(𝑁 + 1))) |
| 147 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 𝐴) → 𝑡 = 𝐴) |
| 148 | 147 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 𝐴) → (𝑡↑(𝑁 + 1)) = (𝐴↑(𝑁 + 1))) |
| 149 | | lbicc2 13504 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
| 150 | 140, 141,
38, 149 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
| 151 | 5 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 152 | 151, 45 | expcld 14186 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑(𝑁 + 1)) ∈ ℂ) |
| 153 | 137, 148,
150, 152 | fvmptd 7023 |
. . . . . 6
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐴) = (𝐴↑(𝑁 + 1))) |
| 154 | 146, 153 | oveq12d 7449 |
. . . . 5
⊢ (𝜑 → (((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐵) − ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡↑(𝑁 + 1)))‘𝐴)) = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
| 155 | 132, 136,
154 | 3eqtr3d 2785 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑡 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + 1) · (𝑡↑𝑁)))‘𝑥) d𝑥 = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
| 156 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑁 + 1) ∈ ℂ) |
| 157 | 156, 13 | mulcld 11281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑁 + 1) · (𝑥↑𝑁)) ∈ ℂ) |
| 158 | 5, 6, 157 | itgioo 25851 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥 = ∫(𝐴[,]𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥) |
| 159 | 37, 155, 158 | 3eqtr3rd 2786 |
. . 3
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝑁 + 1) · (𝑥↑𝑁)) d𝑥 = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
| 160 | 24, 159 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝑁 + 1) · ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥) = ((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1)))) |
| 161 | 4, 22, 23, 160 | mvllmuld 12099 |
1
⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1))) |