Metamath Proof Explorer


Theorem etransclem19

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

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

Proof

Step Hyp Ref Expression
1 etransclem19.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 etransclem19.x ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem19.p ( 𝜑𝑃 ∈ ℕ )
4 etransclem19.1 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5 etransclem19.J ( 𝜑𝐽 ∈ ( 0 ... 𝑀 ) )
6 etransclem19.n ( 𝜑𝑁 ∈ ℤ )
7 etransclem19.7 ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
8 0red ( 𝜑 → 0 ∈ ℝ )
9 6 zred ( 𝜑𝑁 ∈ ℝ )
10 nnm1nn0 ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
11 3 10 syl ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
12 11 nn0red ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
13 3 nnred ( 𝜑𝑃 ∈ ℝ )
14 12 13 ifcld ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
15 11 nn0ge0d ( 𝜑 → 0 ≤ ( 𝑃 − 1 ) )
16 15 adantr ( ( 𝜑𝐽 = 0 ) → 0 ≤ ( 𝑃 − 1 ) )
17 iftrue ( 𝐽 = 0 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑃 − 1 ) )
18 17 eqcomd ( 𝐽 = 0 → ( 𝑃 − 1 ) = if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
19 18 adantl ( ( 𝜑𝐽 = 0 ) → ( 𝑃 − 1 ) = if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
20 16 19 breqtrd ( ( 𝜑𝐽 = 0 ) → 0 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
21 3 nnnn0d ( 𝜑𝑃 ∈ ℕ0 )
22 21 nn0ge0d ( 𝜑 → 0 ≤ 𝑃 )
23 22 adantr ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 0 ≤ 𝑃 )
24 iffalse ( ¬ 𝐽 = 0 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
25 24 eqcomd ( ¬ 𝐽 = 0 → 𝑃 = if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
26 25 adantl ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝑃 = if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
27 23 26 breqtrd ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 0 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
28 20 27 pm2.61dan ( 𝜑 → 0 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
29 8 14 9 28 7 lelttrd ( 𝜑 → 0 < 𝑁 )
30 8 9 29 ltled ( 𝜑 → 0 ≤ 𝑁 )
31 elnn0z ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
32 6 30 31 sylanbrc ( 𝜑𝑁 ∈ ℕ0 )
33 1 2 3 4 5 32 etransclem17 ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻𝐽 ) ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
34 7 iftrued ( 𝜑 → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) = 0 )
35 34 mpteq2dv ( 𝜑 → ( 𝑥𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) = ( 𝑥𝑋 ↦ 0 ) )
36 33 35 eqtrd ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻𝐽 ) ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ 0 ) )