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 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )