Metamath Proof Explorer

Theorem etransclem21

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

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

Proof

Step Hyp Ref Expression
1 etransclem21.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 etransclem21.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem21.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4 etransclem21.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5 etransclem21.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
6 etransclem21.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7 etransclem21.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
8 1 2 3 4 5 6 etransclem17 ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
9 oveq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 − 𝐽 ) = ( 𝑌 − 𝐽 ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) = ( ( 𝑌 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑌 → ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) = ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑌 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) )
12 11 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 ) , 𝑃 ) − 𝑁 ) ) ) ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 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 ) , 𝑃 ) − 𝑁 ) ) ) ) )
14 0cnd ⊢ ( ( 𝜑 ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 0 ∈ ℂ )
15 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
16 3 15 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
17 3 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
18 16 17 ifcld ⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
19 18 faccld ⊢ ( 𝜑 → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℕ )
20 19 nncnd ⊢ ( 𝜑 → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
22 18 nn0zd ⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
23 6 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
24 22 23 zsubcld ⊢ ( 𝜑 → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ )
26 6 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 𝑁 ∈ ℝ )
28 18 nn0red ⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
29 28 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
30 simpr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
31 27 29 30 nltled ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 𝑁 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
32 29 27 subge0d ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ↔ 𝑁 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
33 31 32 mpbird ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) )
34 elnn0z ⊢ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 ↔ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) )
35 25 33 34 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 )
36 35 faccld ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℕ )
37 36 nncnd ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℂ )
38 36 nnne0d ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ≠ 0 )
39 21 37 38 divcld ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ℂ )
40 1 2 dvdmsscn ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
41 40 7 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
42 5 elfzelzd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
43 42 zcnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
44 41 43 subcld ⊢ ( 𝜑 → ( 𝑌 − 𝐽 ) ∈ ℂ )
45 44 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑌 − 𝐽 ) ∈ ℂ )
46 45 35 expcld ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( 𝑌 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℂ )
47 39 46 mulcld ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑌 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ℂ )
48 14 47 ifclda ⊢ ( 𝜑 → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑌 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ℂ )
49 8 13 7 48 fvmptd ⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) ‘ 𝑌 ) = if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑌 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) )