dvnmptconst

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

	Ref	Expression
Hypotheses	dvnmptconst.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvnmptconst.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	dvnmptconst.a	$⊢ φ \to A \in ℂ$
	dvnmptconst.n	$⊢ φ \to N \in ℕ$
Assertion	dvnmptconst	$⊢ φ \to (S D^{n} (x \in X ⟼ A)) (N) = (x \in X ⟼ 0)$

Proof

Step	Hyp	Ref	Expression
1		dvnmptconst.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvnmptconst.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		dvnmptconst.a	$⊢ φ \to A \in ℂ$
4		dvnmptconst.n	$⊢ φ \to N \in ℕ$
5		id	$⊢ φ \to φ$
6		fveq2	$⊢ n = 1 \to (S D^{n} (x \in X ⟼ A)) (n) = (S D^{n} (x \in X ⟼ A)) (1)$
7	6	eqeq1d	$⊢ n = 1 \to ((S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0) \leftrightarrow (S D^{n} (x \in X ⟼ A)) (1) = (x \in X ⟼ 0))$
8	7	imbi2d	$⊢ n = 1 \to ((φ \to (S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0)) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A)) (1) = (x \in X ⟼ 0)))$
9		fveq2	$⊢ n = m \to (S D^{n} (x \in X ⟼ A)) (n) = (S D^{n} (x \in X ⟼ A)) (m)$
10	9	eqeq1d	$⊢ n = m \to ((S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0) \leftrightarrow (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0))$
11	10	imbi2d	$⊢ n = m \to ((φ \to (S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0)) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)))$
12		fveq2	$⊢ n = m + 1 \to (S D^{n} (x \in X ⟼ A)) (n) = (S D^{n} (x \in X ⟼ A)) (m + 1)$
13	12	eqeq1d	$⊢ n = m + 1 \to ((S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0) \leftrightarrow (S D^{n} (x \in X ⟼ A)) (m + 1) = (x \in X ⟼ 0))$
14	13	imbi2d	$⊢ n = m + 1 \to ((φ \to (S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0)) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A)) (m + 1) = (x \in X ⟼ 0)))$
15		fveq2	$⊢ n = N \to (S D^{n} (x \in X ⟼ A)) (n) = (S D^{n} (x \in X ⟼ A)) (N)$
16	15	eqeq1d	$⊢ n = N \to ((S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0) \leftrightarrow (S D^{n} (x \in X ⟼ A)) (N) = (x \in X ⟼ 0))$
17	16	imbi2d	$⊢ n = N \to ((φ \to (S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ 0)) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A)) (N) = (x \in X ⟼ 0)))$
18		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
19	1 18	syl	$⊢ φ \to S \subseteq ℂ$
20	3	adantr	$⊢ (φ \land x \in X) \to A \in ℂ$
21		restsspw	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \subseteq 𝒫 S$
22	21 2	sselid	$⊢ φ \to X \in 𝒫 S$
23		elpwi	$⊢ X \in 𝒫 S \to X \subseteq S$
24	22 23	syl	$⊢ φ \to X \subseteq S$
25		cnex	$⊢ ℂ \in V$
26	25	a1i	$⊢ φ \to ℂ \in V$
27	20 24 26 1	mptelpm	$⊢ φ \to (x \in X ⟼ A) \in (ℂ ↑_{𝑝𝑚} S)$
28		dvn1	$⊢ (S \subseteq ℂ \land (x \in X ⟼ A) \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} (x \in X ⟼ A)) (1) = \frac{d (x \in X⟼ A)}{d_{S} x}$
29	19 27 28	syl2anc	$⊢ φ \to (S D^{n} (x \in X ⟼ A)) (1) = \frac{d (x \in X⟼ A)}{d_{S} x}$
30	1 2 3	dvmptconst	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ 0)$
31	29 30	eqtrd	$⊢ φ \to (S D^{n} (x \in X ⟼ A)) (1) = (x \in X ⟼ 0)$
32		simp3	$⊢ (m \in ℕ \land (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to φ$
33		simp1	$⊢ (m \in ℕ \land (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to m \in ℕ$
34		simpr	$⊢ ((φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to φ$
35		simpl	$⊢ ((φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0))$
36		pm3.35	$⊢ (φ \land (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0))) \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)$
37	34 35 36	syl2anc	$⊢ ((φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)$
38	37	3adant1	$⊢ (m \in ℕ \land (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)$
39	19	3ad2ant1	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to S \subseteq ℂ$
40	27	3ad2ant1	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to (x \in X ⟼ A) \in (ℂ ↑_{𝑝𝑚} S)$
41		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
42	41	3ad2ant2	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to m \in ℕ_{0}$
43		dvnp1	$⊢ (S \subseteq ℂ \land (x \in X ⟼ A) \in (ℂ ↑_{𝑝𝑚} S) \land m \in ℕ_{0}) \to (S D^{n} (x \in X ⟼ A)) (m + 1) = S D (S D^{n} (x \in X ⟼ A)) (m)$
44	39 40 42 43	syl3anc	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to (S D^{n} (x \in X ⟼ A)) (m + 1) = S D (S D^{n} (x \in X ⟼ A)) (m)$
45		oveq2	$⊢ (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0) \to S D (S D^{n} (x \in X ⟼ A)) (m) = \frac{d (x \in X⟼ 0)}{d_{S} x}$
46	45	3ad2ant3	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to S D (S D^{n} (x \in X ⟼ A)) (m) = \frac{d (x \in X⟼ 0)}{d_{S} x}$
47		0cnd	$⊢ φ \to 0 \in ℂ$
48	1 2 47	dvmptconst	$⊢ φ \to \frac{d (x \in X⟼ 0)}{d_{S} x} = (x \in X ⟼ 0)$
49	48	3ad2ant1	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to \frac{d (x \in X⟼ 0)}{d_{S} x} = (x \in X ⟼ 0)$
50	44 46 49	3eqtrd	$⊢ (φ \land m \in ℕ \land (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to (S D^{n} (x \in X ⟼ A)) (m + 1) = (x \in X ⟼ 0)$
51	32 33 38 50	syl3anc	$⊢ (m \in ℕ \land (φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \land φ) \to (S D^{n} (x \in X ⟼ A)) (m + 1) = (x \in X ⟼ 0)$
52	51	3exp	$⊢ m \in ℕ \to ((φ \to (S D^{n} (x \in X ⟼ A)) (m) = (x \in X ⟼ 0)) \to (φ \to (S D^{n} (x \in X ⟼ A)) (m + 1) = (x \in X ⟼ 0)))$
53	8 11 14 17 31 52	nnind	$⊢ N \in ℕ \to (φ \to (S D^{n} (x \in X ⟼ A)) (N) = (x \in X ⟼ 0))$
54	4 5 53	sylc	$⊢ φ \to (S D^{n} (x \in X ⟼ A)) (N) = (x \in X ⟼ 0)$

Metamath Proof Explorer

Theorem dvnmptconst

Proof