dvnmptconst

Description: The N -th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvnmptconst.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvnmptconst.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
	dvnmptconst.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	dvnmptconst.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	dvnmptconst	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		dvnmptconst.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvnmptconst.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
3		dvnmptconst.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		dvnmptconst.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		id	⊢ ( 𝜑 → 𝜑 )
6		fveq2	⊢ ( 𝑛 = 1 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 1 ) )
7	6	eqeq1d	⊢ ( 𝑛 = 1 → ( ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ↔ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 1 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
8	7	imbi2d	⊢ ( 𝑛 = 1 → ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ↔ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 1 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ) )
9		fveq2	⊢ ( 𝑛 = 𝑚 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) )
10	9	eqeq1d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ↔ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
11	10	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ↔ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ) )
12		fveq2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) )
13	12	eqeq1d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ↔ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
14	13	imbi2d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ↔ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ) )
15		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑁 ) )
16	15	eqeq1d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ↔ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
17	16	imbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ↔ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ) )
18		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
19	1 18	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
21		restsspw	⊢ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) ⊆ 𝒫 𝑆
22	21 2	sseldi	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝑆 )
23		elpwi	⊢ ( 𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆 )
24	22 23	syl	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
25		cnex	⊢ ℂ ∈ V
26	25	a1i	⊢ ( 𝜑 → ℂ ∈ V )
27	20 24 26 1	mptelpm	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑_pm 𝑆 ) )
28		dvn1	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑_pm 𝑆 ) ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 1 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
29	19 27 28	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 1 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
30	1 2 3	dvmptconst	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
31	29 30	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 1 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
32		simp3	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → 𝜑 )
33		simp1	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → 𝑚 ∈ ℕ )
34		simpr	⊢ ( ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → 𝜑 )
35		simpl	⊢ ( ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
36		pm3.35	⊢ ( ( 𝜑 ∧ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
37	34 35 36	syl2anc	⊢ ( ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
38	37	3adant1	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
39	19	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → 𝑆 ⊆ ℂ )
40	27	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑_pm 𝑆 ) )
41		nnnn0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀ )
42	41	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → 𝑚 ∈ ℕ₀ )
43		dvnp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) ) )
44	39 40 42 43	syl3anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) ) )
45		oveq2	⊢ ( ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) → ( 𝑆 D ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
46	45	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → ( 𝑆 D ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
47		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
48	1 2 47	dvmptconst	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
49	48	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
50	44 46 49	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
51	32 33 38 50	syl3anc	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ∧ 𝜑 ) → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
52	51	3exp	⊢ ( 𝑚 ∈ ℕ → ( ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) → ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) ) )
53	8 11 14 17 31 52	nnind	⊢ ( 𝑁 ∈ ℕ → ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
54	4 5 53	sylc	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )

Metamath Proof Explorer

Theorem dvnmptconst

Proof