# Metamath Proof Explorer

## Theorem etransclem17

Description: The N -th derivative of H . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem17.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
etransclem17.x ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem17.p ( 𝜑𝑃 ∈ ℕ )
etransclem17.1 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
etransclem17.J ( 𝜑𝐽 ∈ ( 0 ... 𝑀 ) )
etransclem17.n ( 𝜑𝑁 ∈ ℕ0 )
Assertion etransclem17 ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻𝐽 ) ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 etransclem17.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 etransclem17.x ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem17.p ( 𝜑𝑃 ∈ ℕ )
4 etransclem17.1 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5 etransclem17.J ( 𝜑𝐽 ∈ ( 0 ... 𝑀 ) )
6 etransclem17.n ( 𝜑𝑁 ∈ ℕ0 )
7 1 2 dvdmsscn ( 𝜑𝑋 ⊆ ℂ )
8 7 sselda ( ( 𝜑𝑥𝑋 ) → 𝑥 ∈ ℂ )
9 8 adantlr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥𝑋 ) → 𝑥 ∈ ℂ )
10 elfzelz ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
11 10 zcnd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℂ )
12 11 ad2antlr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥𝑋 ) → 𝑗 ∈ ℂ )
13 9 12 negsubd ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥𝑋 ) → ( 𝑥 + - 𝑗 ) = ( 𝑥𝑗 ) )
14 13 eqcomd ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥𝑋 ) → ( 𝑥𝑗 ) = ( 𝑥 + - 𝑗 ) )
15 14 oveq1d ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥𝑋 ) → ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
16 15 mpteq2dva ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
17 16 mpteq2dva ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) )
18 4 17 syl5eq ( 𝜑𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) )
19 negeq ( 𝑗 = 𝐽 → - 𝑗 = - 𝐽 )
20 19 oveq2d ( 𝑗 = 𝐽 → ( 𝑥 + - 𝑗 ) = ( 𝑥 + - 𝐽 ) )
21 eqeq1 ( 𝑗 = 𝐽 → ( 𝑗 = 0 ↔ 𝐽 = 0 ) )
22 21 ifbid ( 𝑗 = 𝐽 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
23 20 22 oveq12d ( 𝑗 = 𝐽 → ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
24 23 mpteq2dv ( 𝑗 = 𝐽 → ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
25 24 adantl ( ( 𝜑𝑗 = 𝐽 ) → ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
26 mptexg ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) → ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
27 2 26 syl ( 𝜑 → ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
28 18 25 5 27 fvmptd ( 𝜑 → ( 𝐻𝐽 ) = ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
29 28 oveq2d ( 𝜑 → ( 𝑆 D𝑛 ( 𝐻𝐽 ) ) = ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) )
30 29 fveq1d ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻𝐽 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑁 ) )
31 elfzelz ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ∈ ℤ )
32 31 zcnd ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ∈ ℂ )
33 5 32 syl ( 𝜑𝐽 ∈ ℂ )
34 33 negcld ( 𝜑 → - 𝐽 ∈ ℂ )
35 nnm1nn0 ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
36 3 35 syl ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
37 3 nnnn0d ( 𝜑𝑃 ∈ ℕ0 )
38 36 37 ifcld ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
39 eqid ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
40 1 2 34 38 39 dvnxpaek ( ( 𝜑𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 + - 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
41 6 40 mpdan ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝑥 + - 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 + - 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
42 33 adantr ( ( 𝜑𝑥𝑋 ) → 𝐽 ∈ ℂ )
43 8 42 negsubd ( ( 𝜑𝑥𝑋 ) → ( 𝑥 + - 𝐽 ) = ( 𝑥𝐽 ) )
44 43 oveq1d ( ( 𝜑𝑥𝑋 ) → ( ( 𝑥 + - 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) = ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) )
45 44 oveq2d ( ( 𝜑𝑥𝑋 ) → ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 + - 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) = ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) )
46 45 ifeq2d ( ( 𝜑𝑥𝑋 ) → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 + - 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) = if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) )
47 46 mpteq2dva ( 𝜑 → ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 + - 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) = ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
48 30 41 47 3eqtrd ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻𝐽 ) ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )