etransclem8

Description: F is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Step	Hyp	Ref	Expression
1		etransclem8.x	$⊢ φ \to X \subseteq ℂ$
2		etransclem8.p	$⊢ φ \to P \in ℕ$
3		etransclem8.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
4	1	sselda	$⊢ (φ \land x \in X) \to x \in ℂ$
5	2	adantr	$⊢ (φ \land x \in X) \to P \in ℕ$
6		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
7	5 6	syl	$⊢ (φ \land x \in X) \to P - 1 \in ℕ_{0}$
8	4 7	expcld	$⊢ (φ \land x \in X) \to x^{P - 1} \in ℂ$
9		fzfid	$⊢ (φ \land x \in X) \to (1 \dots M) \in Fin$
10	4	adantr	$⊢ ((φ \land x \in X) \land j \in (1 \dots M)) \to x \in ℂ$
11		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
12	11	zcnd	$⊢ j \in (1 \dots M) \to j \in ℂ$
13	12	adantl	$⊢ ((φ \land x \in X) \land j \in (1 \dots M)) \to j \in ℂ$
14	10 13	subcld	$⊢ ((φ \land x \in X) \land j \in (1 \dots M)) \to x - j \in ℂ$
15	2	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
16	15	ad2antrr	$⊢ ((φ \land x \in X) \land j \in (1 \dots M)) \to P \in ℕ_{0}$
17	14 16	expcld	$⊢ ((φ \land x \in X) \land j \in (1 \dots M)) \to {(x - j)}^{P} \in ℂ$
18	9 17	fprodcl	$⊢ (φ \land x \in X) \to \prod_{j = 1}^{M} {(x - j)}^{P} \in ℂ$
19	8 18	mulcld	$⊢ (φ \land x \in X) \to x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P} \in ℂ$
20	19 3	fmptd	$⊢ φ \to F : X ⟶ ℂ$

Metamath Proof Explorer