Theorem etransclem22

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem22.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		etransclem22.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		etransclem22.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4		etransclem22.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5		etransclem22.J	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
6		etransclem22.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7	1 2 3 4 5 6	etransclem17	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
8		simpr	⊢ ( ( 𝜑 ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
9	8	iftrued	⊢ ( ( 𝜑 ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) = 0 )
10	9	mpteq2dv	⊢ ( ( 𝜑 ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
11	1 2	dvdmsscn	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
12		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
13		ssid	⊢ ℂ ⊆ ℂ
14	13	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
15	11 12 14	constcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 0 ) ∈ ( 𝑋 –cn→ ℂ ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ 0 ) ∈ ( 𝑋 –cn→ ℂ ) )
17	10 16	eqeltrd	⊢ ( ( 𝜑 ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
18		simpr	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
19	18	iffalsed	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) = ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) )
20	19	mpteq2dv	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) )
21		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
22	11 14	idcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( 𝑋 –cn→ ℂ ) )
23	5	elfzelzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
24	23	zcnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
25	11 24 14	constcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐽 ) ∈ ( 𝑋 –cn→ ℂ ) )
26	22 25	subcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 − 𝐽 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 − 𝐽 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
28	13	a1i	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ℂ ⊆ ℂ )
29		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
30	3 29	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
31	3	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
32	30 31	ifcld	⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
33	32	faccld	⊢ ( 𝜑 → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℕ )
34	33	nncnd	⊢ ( 𝜑 → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
35	34	adantr	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
36	32	nn0zd	⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
37	6	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
38	36 37	zsubcld	⊢ ( 𝜑 → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ )
39	38	adantr	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ )
40	6	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
41	40	adantr	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 𝑁 ∈ ℝ )
42	32	nn0red	⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
43	42	adantr	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
44	41 43 18	nltled	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 𝑁 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
45	43 41	subge0d	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ↔ 𝑁 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
46	44 45	mpbird	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) )
47		elnn0z	⊢ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 ↔ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) )
48	39 46 47	sylanbrc	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 )
49	48	faccld	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℕ )
50	49	nncnd	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℂ )
51	49	nnne0d	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ≠ 0 )
52	35 50 51	divcld	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ℂ )
53	28 52 28	constcncfg	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑦 ∈ ℂ ↦ ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
54		expcncf	⊢ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
55	48 54	syl	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
56	53 55	mulcncf	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑦 ∈ ℂ ↦ ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( 𝑦 ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
57		oveq1	⊢ ( 𝑦 = ( 𝑥 − 𝐽 ) → ( 𝑦 ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) = ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) )
58	57	oveq2d	⊢ ( 𝑦 = ( 𝑥 − 𝐽 ) → ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( 𝑦 ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) = ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) )
59	21 27 56 28 58	cncfcompt2	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
60	20 59	eqeltrd	⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
61	17 60	pm2.61dan	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
62	7 61	eqeltrd	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) ∈ ( 𝑋 –cn→ ℂ ) )