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