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	$⊢ φ \to A \in ℝ$
	itgpowd.2	$⊢ φ \to B \in ℝ$
	itgpowd.3	$⊢ φ \to A \leq B$
	itgpowd.4	$⊢ φ \to N \in ℕ_{0}$
Assertion	itgpowd	$⊢ φ \to \int_{[A, B]} x^{N} d x = \frac{B^{N + 1} - A^{N + 1}}{N + 1}$

Proof

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

Metamath Proof Explorer

Theorem itgpowd

Proof