Metamath Proof Explorer

Theorem etransclem18

Description: The given function is integrable. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem18.s 
|- ( ph -> RR e. { RR , CC } )
etransclem18.x 
|- ( ph -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
etransclem18.p 
|- ( ph -> P e. NN )
etransclem18.m 
|- ( ph -> M e. NN0 )
etransclem18.f 
|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem18.a 
|- ( ph -> A e. RR )
etransclem18.b 
|- ( ph -> B e. RR )
Assertion etransclem18 
|- ( ph -> ( x e. ( A (,) B ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. L^1 )

Proof

Step Hyp Ref Expression
1 etransclem18.s 
 |-  ( ph -> RR e. { RR , CC } )
2 etransclem18.x 
 |-  ( ph -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
3 etransclem18.p 
 |-  ( ph -> P e. NN )
4 etransclem18.m 
 |-  ( ph -> M e. NN0 )
5 etransclem18.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
6 etransclem18.a 
 |-  ( ph -> A e. RR )
7 etransclem18.b 
 |-  ( ph -> B e. RR )
8 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
9 8 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
10 ioombl 
 |-  ( A (,) B ) e. dom vol
11 10 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
12 ere 
 |-  _e e. RR
13 12 recni 
 |-  _e e. CC
14 13 a1i 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> _e e. CC )
15 6 7 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
16 15 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
17 16 recnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
18 17 negcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> -u x e. CC )
19 14 18 cxpcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( _e ^c -u x ) e. CC )
20 1 2 dvdmsscn 
 |-  ( ph -> RR C_ CC )
21 20 3 5 etransclem8 
 |-  ( ph -> F : RR --> CC )
22 21 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> F : RR --> CC )
23 22 16 ffvelrnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
24 19 23 mulcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( _e ^c -u x ) x. ( F ` x ) ) e. CC )
25 eqidd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( y e. CC |-> ( _e ^c y ) ) = ( y e. CC |-> ( _e ^c y ) ) )
26 oveq2 
 |-  ( y = -u x -> ( _e ^c y ) = ( _e ^c -u x ) )
27 26 adantl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ y = -u x ) -> ( _e ^c y ) = ( _e ^c -u x ) )
28 15 20 sstrd 
 |-  ( ph -> ( A [,] B ) C_ CC )
29 28 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
30 29 negcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> -u x e. CC )
31 13 a1i 
 |-  ( x e. CC -> _e e. CC )
32 negcl 
 |-  ( x e. CC -> -u x e. CC )
33 31 32 cxpcld 
 |-  ( x e. CC -> ( _e ^c -u x ) e. CC )
34 29 33 syl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( _e ^c -u x ) e. CC )
35 25 27 30 34 fvmptd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( y e. CC |-> ( _e ^c y ) ) ` -u x ) = ( _e ^c -u x ) )
36 35 eqcomd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( _e ^c -u x ) = ( ( y e. CC |-> ( _e ^c y ) ) ` -u x ) )
37 36 mpteq2dva 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( _e ^c -u x ) ) = ( x e. ( A [,] B ) |-> ( ( y e. CC |-> ( _e ^c y ) ) ` -u x ) ) )
38 epr 
 |-  _e e. RR+
39 mnfxr 
 |-  -oo e. RR*
40 39 a1i 
 |-  ( _e e. RR+ -> -oo e. RR* )
41 0red 
 |-  ( _e e. RR+ -> 0 e. RR )
42 rpxr 
 |-  ( _e e. RR+ -> _e e. RR* )
43 rpgt0 
 |-  ( _e e. RR+ -> 0 < _e )
44 40 41 42 43 gtnelioc 
 |-  ( _e e. RR+ -> -. _e e. ( -oo (,] 0 ) )
45 38 44 ax-mp 
 |-  -. _e e. ( -oo (,] 0 )
46 eldif 
 |-  ( _e e. ( CC \ ( -oo (,] 0 ) ) <-> ( _e e. CC /\ -. _e e. ( -oo (,] 0 ) ) )
47 13 45 46 mpbir2an 
 |-  _e e. ( CC \ ( -oo (,] 0 ) )
48 cxpcncf2 
 |-  ( _e e. ( CC \ ( -oo (,] 0 ) ) -> ( y e. CC |-> ( _e ^c y ) ) e. ( CC -cn-> CC ) )
49 47 48 mp1i 
 |-  ( ph -> ( y e. CC |-> ( _e ^c y ) ) e. ( CC -cn-> CC ) )
50 eqid 
 |-  ( x e. ( A [,] B ) |-> -u x ) = ( x e. ( A [,] B ) |-> -u x )
51 50 negcncf 
 |-  ( ( A [,] B ) C_ CC -> ( x e. ( A [,] B ) |-> -u x ) e. ( ( A [,] B ) -cn-> CC ) )
52 28 51 syl 
 |-  ( ph -> ( x e. ( A [,] B ) |-> -u x ) e. ( ( A [,] B ) -cn-> CC ) )
53 49 52 cncfmpt1f 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( y e. CC |-> ( _e ^c y ) ) ` -u x ) ) e. ( ( A [,] B ) -cn-> CC ) )
54 37 53 eqeltrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( _e ^c -u x ) ) e. ( ( A [,] B ) -cn-> CC ) )
55 ax-resscn 
 |-  RR C_ CC
56 55 a1i 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> RR C_ CC )
57 3 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> P e. NN )
58 4 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> M e. NN0 )
59 etransclem6 
 |-  ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) ) = ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) ) )
60 5 59 eqtri 
 |-  F = ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) ) )
61 56 57 58 60 16 etransclem13 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) = prod_ k e. ( 0 ... M ) ( ( x - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) )
62 61 mpteq2dva 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) = ( x e. ( A [,] B ) |-> prod_ k e. ( 0 ... M ) ( ( x - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )
63 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
64 17 3adant3 
 |-  ( ( ph /\ x e. ( A [,] B ) /\ k e. ( 0 ... M ) ) -> x e. CC )
65 elfzelz 
 |-  ( k e. ( 0 ... M ) -> k e. ZZ )
66 65 zcnd 
 |-  ( k e. ( 0 ... M ) -> k e. CC )
67 66 3ad2ant3 
 |-  ( ( ph /\ x e. ( A [,] B ) /\ k e. ( 0 ... M ) ) -> k e. CC )
68 64 67 subcld 
 |-  ( ( ph /\ x e. ( A [,] B ) /\ k e. ( 0 ... M ) ) -> ( x - k ) e. CC )
69 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
70 3 69 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
71 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
72 70 71 ifcld 
 |-  ( ph -> if ( k = 0 , ( P - 1 ) , P ) e. NN0 )
73 72 3ad2ant1 
 |-  ( ( ph /\ x e. ( A [,] B ) /\ k e. ( 0 ... M ) ) -> if ( k = 0 , ( P - 1 ) , P ) e. NN0 )
74 68 73 expcld 
 |-  ( ( ph /\ x e. ( A [,] B ) /\ k e. ( 0 ... M ) ) -> ( ( x - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) e. CC )
75 nfv 
 |-  F/ x ( ph /\ k e. ( 0 ... M ) )
76 ssid 
 |-  CC C_ CC
77 76 a1i 
 |-  ( ph -> CC C_ CC )
78 28 77 idcncfg 
 |-  ( ph -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
79 78 adantr 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
80 28 adantr 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( A [,] B ) C_ CC )
81 66 adantl 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> k e. CC )
82 76 a1i 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> CC C_ CC )
83 80 81 82 constcncfg 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( x e. ( A [,] B ) |-> k ) e. ( ( A [,] B ) -cn-> CC ) )
84 79 83 subcncf 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( x e. ( A [,] B ) |-> ( x - k ) ) e. ( ( A [,] B ) -cn-> CC ) )
85 expcncf 
 |-  ( if ( k = 0 , ( P - 1 ) , P ) e. NN0 -> ( y e. CC |-> ( y ^ if ( k = 0 , ( P - 1 ) , P ) ) ) e. ( CC -cn-> CC ) )
86 72 85 syl 
 |-  ( ph -> ( y e. CC |-> ( y ^ if ( k = 0 , ( P - 1 ) , P ) ) ) e. ( CC -cn-> CC ) )
87 86 adantr 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( y e. CC |-> ( y ^ if ( k = 0 , ( P - 1 ) , P ) ) ) e. ( CC -cn-> CC ) )
88 oveq1 
 |-  ( y = ( x - k ) -> ( y ^ if ( k = 0 , ( P - 1 ) , P ) ) = ( ( x - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) )
89 75 84 87 82 88 cncfcompt2 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( x e. ( A [,] B ) |-> ( ( x - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
90 28 63 74 89 fprodcncf 
 |-  ( ph -> ( x e. ( A [,] B ) |-> prod_ k e. ( 0 ... M ) ( ( x - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
91 62 90 eqeltrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
92 54 91 mulcncf 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
93 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. L^1 )
94 6 7 92 93 syl3anc 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. L^1 )
95 9 11 24 94 iblss 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. L^1 )