etransclem18

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

	Ref	Expression
Hypotheses	etransclem18.s	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
	etransclem18.x	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
	etransclem18.p	$⊢ φ \to P \in ℕ$
	etransclem18.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem18.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem18.a	$⊢ φ \to A \in ℝ$
	etransclem18.b	$⊢ φ \to B \in ℝ$
Assertion	etransclem18	$⊢ φ \to (x \in (A, B) ⟼ e^{- x} F (x)) \in 𝐿^{1}$

Proof

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

Metamath Proof Explorer

Theorem etransclem18

Proof