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 ) )