Metamath Proof Explorer

Theorem itgpowd

Description: The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019) (Revised by Thierry Arnoux, 14-Jun-2019)

Ref Expression
Hypotheses itgpowd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
itgpowd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
itgpowd.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
itgpowd.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion itgpowd ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝑥 ↑ 𝑁 ) d 𝑥 = ( ( ( 𝐵 ↑ ( 𝑁 + 1 ) ) − ( 𝐴 ↑ ( 𝑁 + 1 ) ) ) / ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 itgpowd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 itgpowd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 itgpowd.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 itgpowd.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
6 4 5 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
7 6 nncnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
8 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
9 1 2 8 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
10 ax-resscn ⊢ ℝ ⊆ ℂ
11 9 10 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
12 11 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
13 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑁 ∈ ℕ0 )
14 12 13 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ↑ 𝑁 ) ∈ ℂ )
15 11 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑥 ↑ 𝑁 ) ) )
16 expcncf ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
17 4 16 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
18 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
19 11 17 18 sylc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
20 15 19 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
21 cnicciblnc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ 𝐿1 )
22 1 2 20 21 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ 𝐿1 )
23 14 22 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝑥 ↑ 𝑁 ) d 𝑥 ∈ ℂ )
24 6 nnne0d ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
25 7 14 22 itgmulc2 ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ∫ ( 𝐴 [,] 𝐵 ) ( 𝑥 ↑ 𝑁 ) d 𝑥 ) = ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) d 𝑥 )
26 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
27 oveq1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ↑ 𝑁 ) = ( 𝑥 ↑ 𝑁 ) )
28 27 oveq2d ⊢ ( 𝑡 = 𝑥 → ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) = ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑡 = 𝑥 ) → ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) = ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
31 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 + 1 ) ∈ ℂ )
32 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
33 32 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
34 33 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
35 34 14 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ↑ 𝑁 ) ∈ ℂ )
36 31 35 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) ∈ ℂ )
37 26 29 30 36 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) = ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) )
38 37 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) d 𝑥 )
39 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
40 39 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
41 10 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
42 41 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ )
43 1nn0 ⊢ 1 ∈ ℕ0
44 43 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
45 4 44 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑁 + 1 ) ∈ ℕ0 )
47 42 46 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
48 4 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑁 ∈ ℂ )
50 1cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℂ )
51 49 50 addcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑁 + 1 ) ∈ ℂ )
52 4 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑁 ∈ ℕ0 )
53 42 52 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 𝑁 ) ∈ ℂ )
54 51 53 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ∈ ℂ )
55 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑡 ∈ ℂ )
56 45 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑁 + 1 ) ∈ ℕ0 )
57 55 56 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
58 57 fmpttd ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) : ℂ ⟶ ℂ )
59 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
60 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑁 + 1 ) ∈ ℂ )
61 4 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
62 55 61 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 ↑ 𝑁 ) ∈ ℂ )
63 60 62 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ∈ ℂ )
64 63 fmpttd ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) : ℂ ⟶ ℂ )
65 dvexp ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) = ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ ( ( 𝑁 + 1 ) − 1 ) ) ) ) )
66 6 65 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) = ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ ( ( 𝑁 + 1 ) − 1 ) ) ) ) )
67 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
68 48 67 pncand ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
69 68 oveq2d ⊢ ( 𝜑 → ( 𝑡 ↑ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑡 ↑ 𝑁 ) )
70 69 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( 𝑡 ↑ ( ( 𝑁 + 1 ) − 1 ) ) ) = ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) )
71 70 mpteq2dv ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ ( ( 𝑁 + 1 ) − 1 ) ) ) ) = ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
72 66 71 eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) = ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
73 72 feq1d ⊢ ( 𝜑 → ( ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) : ℂ ⟶ ℂ ↔ ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) : ℂ ⟶ ℂ ) )
74 64 73 mpbird ⊢ ( 𝜑 → ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) : ℂ ⟶ ℂ )
75 74 fdmd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) = ℂ )
76 10 75 sseqtrrid ⊢ ( 𝜑 → ℝ ⊆ dom ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) )
77 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ) ) → ( ℝ D ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ↾ ℝ ) )
78 40 58 59 76 77 syl22anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ↾ ℝ ) )
79 72 reseq1d ⊢ ( 𝜑 → ( ( ℂ D ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ↾ ℝ ) = ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ↾ ℝ ) )
80 78 79 eqtrd ⊢ ( 𝜑 → ( ℝ D ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ℝ ) ) = ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ↾ ℝ ) )
81 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ℝ ) = ( 𝑡 ∈ ℝ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) )
82 10 81 mp1i ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ℝ ) = ( 𝑡 ∈ ℝ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) )
83 82 oveq2d ⊢ ( 𝜑 → ( ℝ D ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ℝ ) ) = ( ℝ D ( 𝑡 ∈ ℝ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) )
84 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ↾ ℝ ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
85 10 84 mp1i ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ↾ ℝ ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
86 80 83 85 3eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
87 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
88 87 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
89 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
90 1 2 89 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
91 40 47 54 86 9 88 87 90 dvmptres2 ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) )
92 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
93 92 10 sstri ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
94 93 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
95 cncfmptc ⊢ ( ( ( 𝑁 + 1 ) ∈ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑁 + 1 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
96 7 94 59 95 syl3anc ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑁 + 1 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
97 resmpt ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑡 ↑ 𝑁 ) ) )
98 93 97 mp1i ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑡 ↑ 𝑁 ) ) )
99 expcncf ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
100 4 99 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
101 rescncf ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) )
102 94 100 101 sylc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
103 98 102 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑡 ↑ 𝑁 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
104 96 103 mulcncf ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
105 91 104 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
106 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
107 106 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
108 48 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑁 ∈ ℂ )
109 1cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 1 ∈ ℂ )
110 108 109 addcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑁 + 1 ) ∈ ℂ )
111 11 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ℂ )
112 4 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑁 ∈ ℕ0 )
113 111 112 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ↑ 𝑁 ) ∈ ℂ )
114 110 113 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ∈ ℂ )
115 cncfmptc ⊢ ( ( ( 𝑁 + 1 ) ∈ ℂ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑁 + 1 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
116 7 11 59 115 syl3anc ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑁 + 1 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
117 11 resmptd ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ 𝑁 ) ) )
118 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
119 11 100 118 sylc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 𝑁 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
120 117 119 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ 𝑁 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
121 116 120 mulcncf ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
122 cnicciblnc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ∈ 𝐿1 )
123 1 2 121 122 syl3anc ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ∈ 𝐿1 )
124 33 107 114 123 iblss ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ∈ 𝐿1 )
125 91 124 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ∈ 𝐿1 )
126 11 resmptd ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) )
127 expcncf ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
128 45 127 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
129 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
130 11 128 129 sylc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
131 126 130 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
132 1 2 3 105 125 131 ftc2 ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ‘ 𝐵 ) − ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ‘ 𝐴 ) ) )
133 91 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) )
134 133 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) )
135 itgeq2 ⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) d 𝑥 )
136 134 135 syl ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) d 𝑥 )
137 eqidd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) )
138 simpr ⊢ ( ( 𝜑 ∧ 𝑡 = 𝐵 ) → 𝑡 = 𝐵 )
139 138 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 = 𝐵 ) → ( 𝑡 ↑ ( 𝑁 + 1 ) ) = ( 𝐵 ↑ ( 𝑁 + 1 ) ) )
140 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
141 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
142 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
143 140 141 3 142 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
144 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
145 144 45 expcld ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
146 137 139 143 145 fvmptd ⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ‘ 𝐵 ) = ( 𝐵 ↑ ( 𝑁 + 1 ) ) )
147 simpr ⊢ ( ( 𝜑 ∧ 𝑡 = 𝐴 ) → 𝑡 = 𝐴 )
148 147 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 = 𝐴 ) → ( 𝑡 ↑ ( 𝑁 + 1 ) ) = ( 𝐴 ↑ ( 𝑁 + 1 ) ) )
149 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
150 140 141 3 149 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
151 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
152 151 45 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
153 137 148 150 152 fvmptd ⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ‘ 𝐴 ) = ( 𝐴 ↑ ( 𝑁 + 1 ) ) )
154 146 153 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ‘ 𝐵 ) − ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 ↑ ( 𝑁 + 1 ) ) ) ‘ 𝐴 ) ) = ( ( 𝐵 ↑ ( 𝑁 + 1 ) ) − ( 𝐴 ↑ ( 𝑁 + 1 ) ) ) )
155 132 136 154 3eqtr3d ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + 1 ) · ( 𝑡 ↑ 𝑁 ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( 𝐵 ↑ ( 𝑁 + 1 ) ) − ( 𝐴 ↑ ( 𝑁 + 1 ) ) ) )
156 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑁 + 1 ) ∈ ℂ )
157 156 14 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) ∈ ℂ )
158 1 2 157 itgioo ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) d 𝑥 )
159 38 155 158 3eqtr3rd ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝑁 + 1 ) · ( 𝑥 ↑ 𝑁 ) ) d 𝑥 = ( ( 𝐵 ↑ ( 𝑁 + 1 ) ) − ( 𝐴 ↑ ( 𝑁 + 1 ) ) ) )
160 25 159 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ∫ ( 𝐴 [,] 𝐵 ) ( 𝑥 ↑ 𝑁 ) d 𝑥 ) = ( ( 𝐵 ↑ ( 𝑁 + 1 ) ) − ( 𝐴 ↑ ( 𝑁 + 1 ) ) ) )
161 7 23 24 160 mvllmuld ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝑥 ↑ 𝑁 ) d 𝑥 = ( ( ( 𝐵 ↑ ( 𝑁 + 1 ) ) − ( 𝐴 ↑ ( 𝑁 + 1 ) ) ) / ( 𝑁 + 1 ) ) )