Theorem etransclem8

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

	Ref	Expression
Hypotheses	etransclem8.x	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
	etransclem8.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem8.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
Assertion	etransclem8	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		etransclem8.x	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
2		etransclem8.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
3		etransclem8.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
4	1	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ ℕ )
6		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
7	5 6	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 − 1 ) ∈ ℕ0 )
8	4 7	expcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ↑ ( 𝑃 − 1 ) ) ∈ ℂ )
9		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 1 ... 𝑀 ) ∈ Fin )
10	4	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑥 ∈ ℂ )
11		elfzelz	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
12	11	zcnd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℂ )
13	12	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ℂ )
14	10 13	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑥 − 𝑗 ) ∈ ℂ )
15	2	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
16	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ0 )
17	14 16	expcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ∈ ℂ )
18	9 17	fprodcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ∈ ℂ )
19	8 18	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ∈ ℂ )
20	19 3	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )