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 φA
itgpowd.2 φB
itgpowd.3 φAB
itgpowd.4 φN0
Assertion itgpowd φABxNdx=BN+1AN+1N+1

Proof

Step Hyp Ref Expression
1 itgpowd.1 φA
2 itgpowd.2 φB
3 itgpowd.3 φAB
4 itgpowd.4 φN0
5 nn0p1nn N0N+1
6 4 5 syl φN+1
7 6 nncnd φN+1
8 iccssre ABAB
9 1 2 8 syl2anc φAB
10 ax-resscn
11 9 10 sstrdi φAB
12 11 sselda φxABx
13 4 adantr φxABN0
14 12 13 expcld φxABxN
15 11 resmptd φxxNAB=xABxN
16 expcncf N0xxN:cn
17 4 16 syl φxxN:cn
18 rescncf ABxxN:cnxxNAB:ABcn
19 11 17 18 sylc φxxNAB:ABcn
20 15 19 eqeltrrd φxABxN:ABcn
21 cnicciblnc ABxABxN:ABcnxABxN𝐿1
22 1 2 20 21 syl3anc φxABxN𝐿1
23 14 22 itgcl φABxNdx
24 6 nnne0d φN+10
25 7 14 22 itgmulc2 φN+1ABxNdx=ABN+1xNdx
26 eqidd φxABtABN+1tN=tABN+1tN
27 oveq1 t=xtN=xN
28 27 oveq2d t=xN+1tN=N+1xN
29 28 adantl φxABt=xN+1tN=N+1xN
30 simpr φxABxAB
31 7 adantr φxABN+1
32 ioossicc ABAB
33 32 a1i φABAB
34 33 sselda φxABxAB
35 34 14 syldan φxABxN
36 31 35 mulcld φxABN+1xN
37 26 29 30 36 fvmptd φxABtABN+1tNx=N+1xN
38 37 itgeq2dv φABtABN+1tNxdx=ABN+1xNdx
39 reelprrecn
40 39 a1i φ
41 10 a1i φ
42 41 sselda φtt
43 1nn0 10
44 43 a1i φ10
45 4 44 nn0addcld φN+10
46 45 adantr φtN+10
47 42 46 expcld φttN+1
48 4 nn0cnd φN
49 48 adantr φtN
50 1cnd φt1
51 49 50 addcld φtN+1
52 4 adantr φtN0
53 42 52 expcld φttN
54 51 53 mulcld φtN+1tN
55 simpr φtt
56 45 adantr φtN+10
57 55 56 expcld φttN+1
58 57 fmpttd φttN+1:
59 ssidd φ
60 7 adantr φtN+1
61 4 adantr φtN0
62 55 61 expcld φttN
63 60 62 mulcld φtN+1tN
64 63 fmpttd φtN+1tN:
65 dvexp N+1dttN+1dt=tN+1tN+1-1
66 6 65 syl φdttN+1dt=tN+1tN+1-1
67 1cnd φ1
68 48 67 pncand φN+1-1=N
69 68 oveq2d φtN+1-1=tN
70 69 oveq2d φN+1tN+1-1=N+1tN
71 70 mpteq2dv φtN+1tN+1-1=tN+1tN
72 66 71 eqtrd φdttN+1dt=tN+1tN
73 72 feq1d φdttN+1dt:tN+1tN:
74 64 73 mpbird φdttN+1dt:
75 74 fdmd φdomdttN+1dt=
76 10 75 sseqtrrid φdomdttN+1dt
77 dvres3 ttN+1:domdttN+1dtDttN+1=dttN+1dt
78 40 58 59 76 77 syl22anc φDttN+1=dttN+1dt
79 72 reseq1d φdttN+1dt=tN+1tN
80 78 79 eqtrd φDttN+1=tN+1tN
81 resmpt ttN+1=ttN+1
82 10 81 mp1i φttN+1=ttN+1
83 82 oveq2d φDttN+1=dttN+1dt
84 resmpt tN+1tN=tN+1tN
85 10 84 mp1i φtN+1tN=tN+1tN
86 80 83 85 3eqtr3d φdttN+1dt=tN+1tN
87 eqid TopOpenfld=TopOpenfld
88 87 tgioo2 topGenran.=TopOpenfld𝑡
89 iccntr ABinttopGenran.AB=AB
90 1 2 89 syl2anc φinttopGenran.AB=AB
91 40 47 54 86 9 88 87 90 dvmptres2 φdtABtN+1dt=tABN+1tN
92 ioossre AB
93 92 10 sstri AB
94 93 a1i φAB
95 cncfmptc N+1ABtABN+1:ABcn
96 7 94 59 95 syl3anc φtABN+1:ABcn
97 resmpt ABttNAB=tABtN
98 93 97 mp1i φttNAB=tABtN
99 expcncf N0ttN:cn
100 4 99 syl φttN:cn
101 rescncf ABttN:cnttNAB:ABcn
102 94 100 101 sylc φttNAB:ABcn
103 98 102 eqeltrrd φtABtN:ABcn
104 96 103 mulcncf φtABN+1tN:ABcn
105 91 104 eqeltrd φdtABtN+1dt:ABcn
106 ioombl ABdomvol
107 106 a1i φABdomvol
108 48 adantr φtABN
109 1cnd φtAB1
110 108 109 addcld φtABN+1
111 11 sselda φtABt
112 4 adantr φtABN0
113 111 112 expcld φtABtN
114 110 113 mulcld φtABN+1tN
115 cncfmptc N+1ABtABN+1:ABcn
116 7 11 59 115 syl3anc φtABN+1:ABcn
117 11 resmptd φttNAB=tABtN
118 rescncf ABttN:cnttNAB:ABcn
119 11 100 118 sylc φttNAB:ABcn
120 117 119 eqeltrrd φtABtN:ABcn
121 116 120 mulcncf φtABN+1tN:ABcn
122 cnicciblnc ABtABN+1tN:ABcntABN+1tN𝐿1
123 1 2 121 122 syl3anc φtABN+1tN𝐿1
124 33 107 114 123 iblss φtABN+1tN𝐿1
125 91 124 eqeltrd φdtABtN+1dt𝐿1
126 11 resmptd φttN+1AB=tABtN+1
127 expcncf N+10ttN+1:cn
128 45 127 syl φttN+1:cn
129 rescncf ABttN+1:cnttN+1AB:ABcn
130 11 128 129 sylc φttN+1AB:ABcn
131 126 130 eqeltrrd φtABtN+1:ABcn
132 1 2 3 105 125 131 ftc2 φABdtABtN+1dtxdx=tABtN+1BtABtN+1A
133 91 fveq1d φdtABtN+1dtx=tABN+1tNx
134 133 ralrimivw φxABdtABtN+1dtx=tABN+1tNx
135 itgeq2 xABdtABtN+1dtx=tABN+1tNxABdtABtN+1dtxdx=ABtABN+1tNxdx
136 134 135 syl φABdtABtN+1dtxdx=ABtABN+1tNxdx
137 eqidd φtABtN+1=tABtN+1
138 simpr φt=Bt=B
139 138 oveq1d φt=BtN+1=BN+1
140 1 rexrd φA*
141 2 rexrd φB*
142 ubicc2 A*B*ABBAB
143 140 141 3 142 syl3anc φBAB
144 2 recnd φB
145 144 45 expcld φBN+1
146 137 139 143 145 fvmptd φtABtN+1B=BN+1
147 simpr φt=At=A
148 147 oveq1d φt=AtN+1=AN+1
149 lbicc2 A*B*ABAAB
150 140 141 3 149 syl3anc φAAB
151 1 recnd φA
152 151 45 expcld φAN+1
153 137 148 150 152 fvmptd φtABtN+1A=AN+1
154 146 153 oveq12d φtABtN+1BtABtN+1A=BN+1AN+1
155 132 136 154 3eqtr3d φABtABN+1tNxdx=BN+1AN+1
156 7 adantr φxABN+1
157 156 14 mulcld φxABN+1xN
158 1 2 157 itgioo φABN+1xNdx=ABN+1xNdx
159 38 155 158 3eqtr3rd φABN+1xNdx=BN+1AN+1
160 25 159 eqtrd φN+1ABxNdx=BN+1AN+1
161 7 23 24 160 mvllmuld φABxNdx=BN+1AN+1N+1