dvnadd

Description: The N -th derivative of the M -th derivative of F is the same as the M + N -th derivative of F . (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	dvnadd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (M)) (N) = (S D^{n} F) (M + N)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ n = 0 \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} (S D^{n} F) (M)) (0)$
2		oveq2	$⊢ n = 0 \to M + n = M + 0$
3	2	fveq2d	$⊢ n = 0 \to (S D^{n} F) (M + n) = (S D^{n} F) (M + 0)$
4	1 3	eqeq12d	$⊢ n = 0 \to ((S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n) \leftrightarrow (S D^{n} (S D^{n} F) (M)) (0) = (S D^{n} F) (M + 0))$
5	4	imbi2d	$⊢ n = 0 \to ((((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n)) \leftrightarrow (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (0) = (S D^{n} F) (M + 0)))$
6		fveq2	$⊢ n = k \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} (S D^{n} F) (M)) (k)$
7		oveq2	$⊢ n = k \to M + n = M + k$
8	7	fveq2d	$⊢ n = k \to (S D^{n} F) (M + n) = (S D^{n} F) (M + k)$
9	6 8	eqeq12d	$⊢ n = k \to ((S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n) \leftrightarrow (S D^{n} (S D^{n} F) (M)) (k) = (S D^{n} F) (M + k))$
10	9	imbi2d	$⊢ n = k \to ((((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n)) \leftrightarrow (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (k) = (S D^{n} F) (M + k)))$
11		fveq2	$⊢ n = k + 1 \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} (S D^{n} F) (M)) (k + 1)$
12		oveq2	$⊢ n = k + 1 \to M + n = M + k + 1$
13	12	fveq2d	$⊢ n = k + 1 \to (S D^{n} F) (M + n) = (S D^{n} F) (M + k + 1)$
14	11 13	eqeq12d	$⊢ n = k + 1 \to ((S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n) \leftrightarrow (S D^{n} (S D^{n} F) (M)) (k + 1) = (S D^{n} F) (M + k + 1))$
15	14	imbi2d	$⊢ n = k + 1 \to ((((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n)) \leftrightarrow (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (k + 1) = (S D^{n} F) (M + k + 1)))$
16		fveq2	$⊢ n = N \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} (S D^{n} F) (M)) (N)$
17		oveq2	$⊢ n = N \to M + n = M + N$
18	17	fveq2d	$⊢ n = N \to (S D^{n} F) (M + n) = (S D^{n} F) (M + N)$
19	16 18	eqeq12d	$⊢ n = N \to ((S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n) \leftrightarrow (S D^{n} (S D^{n} F) (M)) (N) = (S D^{n} F) (M + N))$
20	19	imbi2d	$⊢ n = N \to ((((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (n) = (S D^{n} F) (M + n)) \leftrightarrow (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (N) = (S D^{n} F) (M + N)))$
21		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
22	21	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to S \subseteq ℂ$
23		ssidd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to ℂ \subseteq ℂ$
24		cnex	$⊢ ℂ \in V$
25		elpm2g	$⊢ (ℂ \in V \land S \in \{ℝ, ℂ\}) \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
26	24 25	mpan	$⊢ S \in \{ℝ, ℂ\} \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
27	26	simplbda	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to dom F \subseteq S$
28	24	a1i	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to ℂ \in V$
29		simpl	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S \in \{ℝ, ℂ\}$
30		pmss12g	$⊢ ((ℂ \subseteq ℂ \land dom F \subseteq S) \land (ℂ \in V \land S \in \{ℝ, ℂ\})) \to ℂ ↑_{𝑝𝑚} dom F \subseteq ℂ ↑_{𝑝𝑚} S$
31	23 27 28 29 30	syl22anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to ℂ ↑_{𝑝𝑚} dom F \subseteq ℂ ↑_{𝑝𝑚} S$
32	31	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to ℂ ↑_{𝑝𝑚} dom F \subseteq ℂ ↑_{𝑝𝑚} S$
33		dvnff	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F$
34	33	ffvelrnda	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} dom F)$
35	32 34	sseldd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S)$
36		dvn0	$⊢ (S \subseteq ℂ \land (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} (S D^{n} F) (M)) (0) = (S D^{n} F) (M)$
37	22 35 36	syl2anc	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (0) = (S D^{n} F) (M)$
38		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
39	38	adantl	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to M \in ℂ$
40	39	addid1d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to M + 0 = M$
41	40	fveq2d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} F) (M + 0) = (S D^{n} F) (M)$
42	37 41	eqtr4d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (0) = (S D^{n} F) (M + 0)$
43		oveq2	$⊢ (S D^{n} (S D^{n} F) (M)) (k) = (S D^{n} F) (M + k) \to S D (S D^{n} (S D^{n} F) (M)) (k) = S D (S D^{n} F) (M + k)$
44	22	adantr	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to S \subseteq ℂ$
45	35	adantr	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S)$
46		simpr	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
47		dvnp1	$⊢ (S \subseteq ℂ \land (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (k + 1) = S D (S D^{n} (S D^{n} F) (M)) (k)$
48	44 45 46 47	syl3anc	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (k + 1) = S D (S D^{n} (S D^{n} F) (M)) (k)$
49	39	adantr	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to M \in ℂ$
50		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
51	50	adantl	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℂ$
52		1cnd	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to 1 \in ℂ$
53	49 51 52	addassd	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to M + k + 1 = M + k + 1$
54	53	fveq2d	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (S D^{n} F) (M + k + 1) = (S D^{n} F) (M + k + 1)$
55		simpllr	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to F \in (ℂ ↑_{𝑝𝑚} S)$
56		nn0addcl	$⊢ (M \in ℕ_{0} \land k \in ℕ_{0}) \to M + k \in ℕ_{0}$
57	56	adantll	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to M + k \in ℕ_{0}$
58		dvnp1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land M + k \in ℕ_{0}) \to (S D^{n} F) (M + k + 1) = S D (S D^{n} F) (M + k)$
59	44 55 57 58	syl3anc	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (S D^{n} F) (M + k + 1) = S D (S D^{n} F) (M + k)$
60	54 59	eqtr3d	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (S D^{n} F) (M + k + 1) = S D (S D^{n} F) (M + k)$
61	48 60	eqeq12d	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to ((S D^{n} (S D^{n} F) (M)) (k + 1) = (S D^{n} F) (M + k + 1) \leftrightarrow S D (S D^{n} (S D^{n} F) (M)) (k) = S D (S D^{n} F) (M + k))$
62	43 61	syl5ibr	$⊢ (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to ((S D^{n} (S D^{n} F) (M)) (k) = (S D^{n} F) (M + k) \to (S D^{n} (S D^{n} F) (M)) (k + 1) = (S D^{n} F) (M + k + 1))$
63	62	expcom	$⊢ k \in ℕ_{0} \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to ((S D^{n} (S D^{n} F) (M)) (k) = (S D^{n} F) (M + k) \to (S D^{n} (S D^{n} F) (M)) (k + 1) = (S D^{n} F) (M + k + 1)))$
64	63	a2d	$⊢ k \in ℕ_{0} \to ((((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (k) = (S D^{n} F) (M + k)) \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (k + 1) = (S D^{n} F) (M + k + 1)))$
65	5 10 15 20 42 64	nn0ind	$⊢ N \in ℕ_{0} \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (S D^{n} (S D^{n} F) (M)) (N) = (S D^{n} F) (M + N))$
66	65	com12	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land M \in ℕ_{0}) \to (N \in ℕ_{0} \to (S D^{n} (S D^{n} F) (M)) (N) = (S D^{n} F) (M + N))$
67	66	impr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (M)) (N) = (S D^{n} F) (M + N)$

Metamath Proof Explorer

Theorem dvnadd

Proof