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 ) ) )