etransclem4

Description: F expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem4.a	$⊢ φ \to A \subseteq ℂ$
	etransclem4.p	$⊢ φ \to P \in ℕ$
	etransclem4.M	$⊢ φ \to M \in ℕ_{0}$
	etransclem4.f	$⊢ F = (x \in A ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem4.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
	etransclem4.e	$⊢ E = (x \in A ⟼ \prod_{j = 0}^{M} H (j) (x))$
Assertion	etransclem4	$⊢ φ \to F = E$

Proof

Step	Hyp	Ref	Expression
1		etransclem4.a	$⊢ φ \to A \subseteq ℂ$
2		etransclem4.p	$⊢ φ \to P \in ℕ$
3		etransclem4.M	$⊢ φ \to M \in ℕ_{0}$
4		etransclem4.f	$⊢ F = (x \in A ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
5		etransclem4.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
6		etransclem4.e	$⊢ E = (x \in A ⟼ \prod_{j = 0}^{M} H (j) (x))$
7		simpr	$⊢ (φ \land j \in (0 \dots M)) \to j \in (0 \dots M)$
8		cnex	$⊢ ℂ \in V$
9	8	ssex	$⊢ A \subseteq ℂ \to A \in V$
10		mptexg	$⊢ A \in V \to (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)}) \in V$
11	1 9 10	3syl	$⊢ φ \to (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)}) \in V$
12	11	adantr	$⊢ (φ \land j \in (0 \dots M)) \to (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)}) \in V$
13	5	fvmpt2	$⊢ (j \in (0 \dots M) \land (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)}) \in V) \to H (j) = (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)})$
14	7 12 13	syl2anc	$⊢ (φ \land j \in (0 \dots M)) \to H (j) = (x \in A ⟼ {(x - j)}^{if (j = 0, P - 1, P)})$
15		ovexd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in A) \to {(x - j)}^{if (j = 0, P - 1, P)} \in V$
16	14 15	fvmpt2d	$⊢ ((φ \land j \in (0 \dots M)) \land x \in A) \to H (j) (x) = {(x - j)}^{if (j = 0, P - 1, P)}$
17	16	an32s	$⊢ ((φ \land x \in A) \land j \in (0 \dots M)) \to H (j) (x) = {(x - j)}^{if (j = 0, P - 1, P)}$
18	17	prodeq2dv	$⊢ (φ \land x \in A) \to \prod_{j = 0}^{M} H (j) (x) = \prod_{j = 0}^{M} {(x - j)}^{if (j = 0, P - 1, P)}$
19		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
20	3 19	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
21	20	adantr	$⊢ (φ \land x \in A) \to M \in ℤ_{\geq 0}$
22	1	sselda	$⊢ (φ \land x \in A) \to x \in ℂ$
23	22	adantr	$⊢ ((φ \land x \in A) \land j \in (0 \dots M)) \to x \in ℂ$
24		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
25	24	zcnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
26	25	adantl	$⊢ ((φ \land x \in A) \land j \in (0 \dots M)) \to j \in ℂ$
27	23 26	subcld	$⊢ ((φ \land x \in A) \land j \in (0 \dots M)) \to x - j \in ℂ$
28		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
29	2 28	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
30	2	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
31	29 30	ifcld	$⊢ φ \to if (j = 0, P - 1, P) \in ℕ_{0}$
32	31	ad2antrr	$⊢ ((φ \land x \in A) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) \in ℕ_{0}$
33	27 32	expcld	$⊢ ((φ \land x \in A) \land j \in (0 \dots M)) \to {(x - j)}^{if (j = 0, P - 1, P)} \in ℂ$
34		oveq2	$⊢ j = 0 \to x - j = x - 0$
35		iftrue	$⊢ j = 0 \to if (j = 0, P - 1, P) = P - 1$
36	34 35	oveq12d	$⊢ j = 0 \to {(x - j)}^{if (j = 0, P - 1, P)} = {(x - 0)}^{P - 1}$
37	21 33 36	fprod1p	$⊢ (φ \land x \in A) \to \prod_{j = 0}^{M} {(x - j)}^{if (j = 0, P - 1, P)} = {(x - 0)}^{P - 1} \prod_{j = 0 + 1}^{M} {(x - j)}^{if (j = 0, P - 1, P)}$
38	22	subid1d	$⊢ (φ \land x \in A) \to x - 0 = x$
39	38	oveq1d	$⊢ (φ \land x \in A) \to {(x - 0)}^{P - 1} = x^{P - 1}$
40		0p1e1	$⊢ 0 + 1 = 1$
41	40	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
42	41	a1i	$⊢ φ \to (0 + 1 \dots M) = (1 \dots M)$
43		0red	$⊢ j \in (1 \dots M) \to 0 \in ℝ$
44		1red	$⊢ j \in (1 \dots M) \to 1 \in ℝ$
45		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
46	45	zred	$⊢ j \in (1 \dots M) \to j \in ℝ$
47		0lt1	$⊢ 0 < 1$
48	47	a1i	$⊢ j \in (1 \dots M) \to 0 < 1$
49		elfzle1	$⊢ j \in (1 \dots M) \to 1 \leq j$
50	43 44 46 48 49	ltletrd	$⊢ j \in (1 \dots M) \to 0 < j$
51	50	gt0ne0d	$⊢ j \in (1 \dots M) \to j \neq 0$
52	51	neneqd	$⊢ j \in (1 \dots M) \to \neg j = 0$
53	52	iffalsed	$⊢ j \in (1 \dots M) \to if (j = 0, P - 1, P) = P$
54	53	oveq2d	$⊢ j \in (1 \dots M) \to {(x - j)}^{if (j = 0, P - 1, P)} = {(x - j)}^{P}$
55	54	adantl	$⊢ (φ \land j \in (1 \dots M)) \to {(x - j)}^{if (j = 0, P - 1, P)} = {(x - j)}^{P}$
56	42 55	prodeq12rdv	$⊢ φ \to \prod_{j = 0 + 1}^{M} {(x - j)}^{if (j = 0, P - 1, P)} = \prod_{j = 1}^{M} {(x - j)}^{P}$
57	56	adantr	$⊢ (φ \land x \in A) \to \prod_{j = 0 + 1}^{M} {(x - j)}^{if (j = 0, P - 1, P)} = \prod_{j = 1}^{M} {(x - j)}^{P}$
58	39 57	oveq12d	$⊢ (φ \land x \in A) \to {(x - 0)}^{P - 1} \prod_{j = 0 + 1}^{M} {(x - j)}^{if (j = 0, P - 1, P)} = x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P}$
59	18 37 58	3eqtrrd	$⊢ (φ \land x \in A) \to x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P} = \prod_{j = 0}^{M} H (j) (x)$
60	59	mpteq2dva	$⊢ φ \to (x \in A ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P}) = (x \in A ⟼ \prod_{j = 0}^{M} H (j) (x))$
61	60 4 6	3eqtr4g	$⊢ φ \to F = E$

Metamath Proof Explorer

Theorem etransclem4

Proof