Step |
Hyp |
Ref |
Expression |
1 |
|
etranslemdvnf2lemlem.s |
⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) |
2 |
|
etransclem29.a |
⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) |
3 |
|
etransclem29.p |
⊢ ( 𝜑 → 𝑃 ∈ ℕ ) |
4 |
|
etransclem29.m |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
5 |
|
etransclem29.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) |
6 |
|
etransclem29.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
7 |
|
etransclem29.h |
⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) |
8 |
|
etransclem29.c |
⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) |
9 |
|
etransclem29.e |
⊢ 𝐸 = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) ) |
10 |
1 2
|
dvdmsscn |
⊢ ( 𝜑 → 𝑋 ⊆ ℂ ) |
11 |
10 3 4 5 7 9
|
etransclem4 |
⊢ ( 𝜑 → 𝐹 = 𝐸 ) |
12 |
11
|
oveq2d |
⊢ ( 𝜑 → ( 𝑆 D𝑛 𝐹 ) = ( 𝑆 D𝑛 𝐸 ) ) |
13 |
12
|
fveq1d |
⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐸 ) ‘ 𝑁 ) ) |
14 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin ) |
15 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ⊆ ℂ ) |
16 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ ) |
17 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) ) |
18 |
15 16 7 17
|
etransclem1 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) |
19 |
1
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } ) |
20 |
2
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) |
21 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑃 ∈ ℕ ) |
22 |
|
etransclem5 |
⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) |
23 |
7 22
|
eqtri |
⊢ 𝐻 = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) |
24 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) ) |
25 |
|
elfznn0 |
⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) → 𝑖 ∈ ℕ0 ) |
26 |
25
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ℕ0 ) |
27 |
19 20 21 23 24 26
|
etransclem20 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑖 ) : 𝑋 ⟶ ℂ ) |
28 |
1 2 14 18 6 27 9 8
|
dvnprod |
⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐸 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) ) |
29 |
13 28
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) ) |