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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
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 )