Metamath Proof Explorer

Theorem etransclem18

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

Ref Expression
Hypotheses etransclem18.s ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
etransclem18.x ⊢ ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
etransclem18.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem18.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem18.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem18.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
etransclem18.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion etransclem18 ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 etransclem18.s ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
2 etransclem18.x ⊢ ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
3 etransclem18.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4 etransclem18.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 etransclem18.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
6 etransclem18.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7 etransclem18.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
8 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
9 8 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
10 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
11 10 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
12 ere ⊢ e ∈ ℝ
13 12 recni ⊢ e ∈ ℂ
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → e ∈ ℂ )
15 6 7 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
16 15 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
18 17 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → - 𝑥 ∈ ℂ )
19 14 18 cxpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( e ↑𝑐 - 𝑥 ) ∈ ℂ )
20 1 2 dvdmsscn ⊢ ( 𝜑 → ℝ ⊆ ℂ )
21 20 3 5 etransclem8 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℂ )
23 22 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
24 19 23 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
25 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) )
26 oveq2 ⊢ ( 𝑦 = - 𝑥 → ( e ↑𝑐 𝑦 ) = ( e ↑𝑐 - 𝑥 ) )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 = - 𝑥 ) → ( e ↑𝑐 𝑦 ) = ( e ↑𝑐 - 𝑥 ) )
28 15 20 sstrd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
29 28 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
30 29 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → - 𝑥 ∈ ℂ )
31 13 a1i ⊢ ( 𝑥 ∈ ℂ → e ∈ ℂ )
32 negcl ⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
33 31 32 cxpcld ⊢ ( 𝑥 ∈ ℂ → ( e ↑𝑐 - 𝑥 ) ∈ ℂ )
34 29 33 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( e ↑𝑐 - 𝑥 ) ∈ ℂ )
35 25 27 30 34 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) ‘ - 𝑥 ) = ( e ↑𝑐 - 𝑥 ) )
36 35 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( e ↑𝑐 - 𝑥 ) = ( ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) ‘ - 𝑥 ) )
37 36 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( e ↑𝑐 - 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) ‘ - 𝑥 ) ) )
38 epr ⊢ e ∈ ℝ+
39 mnfxr ⊢ -∞ ∈ ℝ*
40 39 a1i ⊢ ( e ∈ ℝ+ → -∞ ∈ ℝ* )
41 0red ⊢ ( e ∈ ℝ+ → 0 ∈ ℝ )
42 rpxr ⊢ ( e ∈ ℝ+ → e ∈ ℝ* )
43 rpgt0 ⊢ ( e ∈ ℝ+ → 0 < e )
44 40 41 42 43 gtnelioc ⊢ ( e ∈ ℝ+ → ¬ e ∈ ( -∞ (,] 0 ) )
45 38 44 ax-mp ⊢ ¬ e ∈ ( -∞ (,] 0 )
46 eldif ⊢ ( e ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( e ∈ ℂ ∧ ¬ e ∈ ( -∞ (,] 0 ) ) )
47 13 45 46 mpbir2an ⊢ e ∈ ( ℂ ∖ ( -∞ (,] 0 ) )
48 cxpcncf2 ⊢ ( e ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) )
49 47 48 mp1i ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) )
50 eqid ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - 𝑥 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - 𝑥 )
51 50 negcncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
52 28 51 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
53 49 52 cncfmpt1f ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 ∈ ℂ ↦ ( e ↑𝑐 𝑦 ) ) ‘ - 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
54 37 53 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( e ↑𝑐 - 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
55 ax-resscn ⊢ ℝ ⊆ ℂ
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ℝ ⊆ ℂ )
57 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑃 ∈ ℕ )
58 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑀 ∈ ℕ0 )
59 etransclem6 ⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )
60 5 59 eqtri ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )
61 56 57 58 60 16 etransclem13 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
62 61 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
63 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
64 17 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ℂ )
65 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℤ )
66 65 zcnd ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℂ )
67 66 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℂ )
68 64 67 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − 𝑘 ) ∈ ℂ )
69 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
70 3 69 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
71 3 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
72 70 71 ifcld ⊢ ( 𝜑 → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
73 72 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
74 68 73 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
75 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) )
76 ssid ⊢ ℂ ⊆ ℂ
77 76 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
78 28 77 idcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
80 28 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
81 66 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℂ )
82 76 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ℂ ⊆ ℂ )
83 80 81 82 constcncfg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑘 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
84 79 83 subcncf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑥 − 𝑘 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
85 expcncf ⊢ ( if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
86 72 85 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
88 oveq1 ⊢ ( 𝑦 = ( 𝑥 − 𝑘 ) → ( 𝑦 ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
89 75 84 87 82 88 cncfcompt2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
90 28 63 74 89 fprodcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
91 62 90 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
92 54 91 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
93 cniccibl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
94 6 7 92 93 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
95 9 11 24 94 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )