Step |
Hyp |
Ref |
Expression |
1 |
|
etransclem36.s |
⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) |
2 |
|
etransclem36.x |
⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) |
3 |
|
etransclem36.p |
⊢ ( 𝜑 → 𝑃 ∈ ℕ ) |
4 |
|
etransclem36.m |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
5 |
|
etransclem36.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) |
6 |
|
etransclem36.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
7 |
|
etransclem36.h |
⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) |
8 |
|
etransclem36.jx |
⊢ ( 𝜑 → 𝐽 ∈ 𝑋 ) |
9 |
|
etransclem36.jz |
⊢ ( 𝜑 → 𝐽 ∈ ℤ ) |
10 |
|
etransclem36.10 |
⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) |
11 |
1 2 3 4 5 6 7 10 8
|
etransclem31 |
⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) ) |
12 |
10 6
|
etransclem16 |
⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ∈ Fin ) |
13 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑃 ∈ ℕ ) |
14 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 ) |
15 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 ) |
16 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝐽 ∈ ℤ ) |
17 |
|
etransclem11 |
⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) |
18 |
|
etransclem11 |
⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑒 ‘ 𝑗 ) = 𝑛 } ) |
19 |
10 17 18
|
3eqtri |
⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑒 ‘ 𝑗 ) = 𝑛 } ) |
20 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) |
21 |
13 14 15 16 19 20
|
etransclem26 |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ ) |
22 |
12 21
|
fsumzcl |
⊢ ( 𝜑 → Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ ) |
23 |
11 22
|
eqeltrd |
⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) ∈ ℤ ) |