Metamath Proof Explorer


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 ( 𝜑𝐹 : 𝑋 ⟶ ℂ )