dvnres

Description: Multiple derivative version of dvres3a . (Contributed by Mario Carneiro, 11-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = 0 \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (0)$
2	1	dmeqd	$⊢ x = 0 \to dom (ℂ D^{n} F) (x) = dom (ℂ D^{n} F) (0)$
3	2	eqeq1d	$⊢ x = 0 \to (dom (ℂ D^{n} F) (x) = dom F \leftrightarrow dom (ℂ D^{n} F) (0) = dom F)$
4		fveq2	$⊢ x = 0 \to (S D^{n} ({F ↾}_{S})) (x) = (S D^{n} ({F ↾}_{S})) (0)$
5	1	reseq1d	$⊢ x = 0 \to {(ℂ D^{n} F) (x) ↾}_{S} = {(ℂ D^{n} F) (0) ↾}_{S}$
6	4 5	eqeq12d	$⊢ x = 0 \to ((S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S} \leftrightarrow (S D^{n} ({F ↾}_{S})) (0) = {(ℂ D^{n} F) (0) ↾}_{S})$
7	3 6	imbi12d	$⊢ x = 0 \to ((dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S}) \leftrightarrow (dom (ℂ D^{n} F) (0) = dom F \to (S D^{n} ({F ↾}_{S})) (0) = {(ℂ D^{n} F) (0) ↾}_{S}))$
8	7	imbi2d	$⊢ x = 0 \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S})) \leftrightarrow ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (0) = dom F \to (S D^{n} ({F ↾}_{S})) (0) = {(ℂ D^{n} F) (0) ↾}_{S})))$
9		fveq2	$⊢ x = n \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (n)$
10	9	dmeqd	$⊢ x = n \to dom (ℂ D^{n} F) (x) = dom (ℂ D^{n} F) (n)$
11	10	eqeq1d	$⊢ x = n \to (dom (ℂ D^{n} F) (x) = dom F \leftrightarrow dom (ℂ D^{n} F) (n) = dom F)$
12		fveq2	$⊢ x = n \to (S D^{n} ({F ↾}_{S})) (x) = (S D^{n} ({F ↾}_{S})) (n)$
13	9	reseq1d	$⊢ x = n \to {(ℂ D^{n} F) (x) ↾}_{S} = {(ℂ D^{n} F) (n) ↾}_{S}$
14	12 13	eqeq12d	$⊢ x = n \to ((S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S} \leftrightarrow (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S})$
15	11 14	imbi12d	$⊢ x = n \to ((dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S}) \leftrightarrow (dom (ℂ D^{n} F) (n) = dom F \to (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S}))$
16	15	imbi2d	$⊢ x = n \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S})) \leftrightarrow ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (n) = dom F \to (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S})))$
17		fveq2	$⊢ x = n + 1 \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (n + 1)$
18	17	dmeqd	$⊢ x = n + 1 \to dom (ℂ D^{n} F) (x) = dom (ℂ D^{n} F) (n + 1)$
19	18	eqeq1d	$⊢ x = n + 1 \to (dom (ℂ D^{n} F) (x) = dom F \leftrightarrow dom (ℂ D^{n} F) (n + 1) = dom F)$
20		fveq2	$⊢ x = n + 1 \to (S D^{n} ({F ↾}_{S})) (x) = (S D^{n} ({F ↾}_{S})) (n + 1)$
21	17	reseq1d	$⊢ x = n + 1 \to {(ℂ D^{n} F) (x) ↾}_{S} = {(ℂ D^{n} F) (n + 1) ↾}_{S}$
22	20 21	eqeq12d	$⊢ x = n + 1 \to ((S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S} \leftrightarrow (S D^{n} ({F ↾}_{S})) (n + 1) = {(ℂ D^{n} F) (n + 1) ↾}_{S})$
23	19 22	imbi12d	$⊢ x = n + 1 \to ((dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S}) \leftrightarrow (dom (ℂ D^{n} F) (n + 1) = dom F \to (S D^{n} ({F ↾}_{S})) (n + 1) = {(ℂ D^{n} F) (n + 1) ↾}_{S}))$
24	23	imbi2d	$⊢ x = n + 1 \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S})) \leftrightarrow ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (n + 1) = dom F \to (S D^{n} ({F ↾}_{S})) (n + 1) = {(ℂ D^{n} F) (n + 1) ↾}_{S})))$
25		fveq2	$⊢ x = N \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (N)$
26	25	dmeqd	$⊢ x = N \to dom (ℂ D^{n} F) (x) = dom (ℂ D^{n} F) (N)$
27	26	eqeq1d	$⊢ x = N \to (dom (ℂ D^{n} F) (x) = dom F \leftrightarrow dom (ℂ D^{n} F) (N) = dom F)$
28		fveq2	$⊢ x = N \to (S D^{n} ({F ↾}_{S})) (x) = (S D^{n} ({F ↾}_{S})) (N)$
29	25	reseq1d	$⊢ x = N \to {(ℂ D^{n} F) (x) ↾}_{S} = {(ℂ D^{n} F) (N) ↾}_{S}$
30	28 29	eqeq12d	$⊢ x = N \to ((S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S} \leftrightarrow (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S})$
31	27 30	imbi12d	$⊢ x = N \to ((dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S}) \leftrightarrow (dom (ℂ D^{n} F) (N) = dom F \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S}))$
32	31	imbi2d	$⊢ x = N \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (x) = dom F \to (S D^{n} ({F ↾}_{S})) (x) = {(ℂ D^{n} F) (x) ↾}_{S})) \leftrightarrow ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (N) = dom F \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S})))$
33		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
34	33	adantr	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to S \subseteq ℂ$
35		pmresg	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to {F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S)$
36		dvn0	$⊢ (S \subseteq ℂ \land {F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} ({F ↾}_{S})) (0) = {F ↾}_{S}$
37	34 35 36	syl2anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (S D^{n} ({F ↾}_{S})) (0) = {F ↾}_{S}$
38		ssidd	$⊢ S \in \{ℝ, ℂ\} \to ℂ \subseteq ℂ$
39		dvn0	$⊢ (ℂ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (ℂ D^{n} F) (0) = F$
40	38 39	sylan	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (ℂ D^{n} F) (0) = F$
41	40	reseq1d	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to {(ℂ D^{n} F) (0) ↾}_{S} = {F ↾}_{S}$
42	37 41	eqtr4d	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (S D^{n} ({F ↾}_{S})) (0) = {(ℂ D^{n} F) (0) ↾}_{S}$
43	42	a1d	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (0) = dom F \to (S D^{n} ({F ↾}_{S})) (0) = {(ℂ D^{n} F) (0) ↾}_{S})$
44		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
45		simplr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
46		simprl	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to n \in ℕ_{0}$
47		dvnbss	$⊢ (ℂ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land n \in ℕ_{0}) \to dom (ℂ D^{n} F) (n) \subseteq dom F$
48	44 45 46 47	mp3an2i	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n) \subseteq dom F$
49		simprr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n + 1) = dom F$
50		ssidd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to ℂ \subseteq ℂ$
51		dvnp1	$⊢ (ℂ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n + 1) = ℂ D (ℂ D^{n} F) (n)$
52	50 45 46 51	syl3anc	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to (ℂ D^{n} F) (n + 1) = ℂ D (ℂ D^{n} F) (n)$
53	52	dmeqd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n + 1) = dom {(ℂ D^{n} F) (n)}_{ℂ}^{'}$
54	49 53	eqtr3d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom F = dom {(ℂ D^{n} F) (n)}_{ℂ}^{'}$
55		dvnf	$⊢ (ℂ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n) : dom (ℂ D^{n} F) (n) ⟶ ℂ$
56	44 45 46 55	mp3an2i	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to (ℂ D^{n} F) (n) : dom (ℂ D^{n} F) (n) ⟶ ℂ$
57		cnex	$⊢ ℂ \in V$
58	57 57	elpm2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℂ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℂ)$
59	58	simprbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℂ) \to dom F \subseteq ℂ$
60	45 59	syl	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom F \subseteq ℂ$
61	48 60	sstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n) \subseteq ℂ$
62	50 56 61	dvbss	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom {(ℂ D^{n} F) (n)}_{ℂ}^{'} \subseteq dom (ℂ D^{n} F) (n)$
63	54 62	eqsstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom F \subseteq dom (ℂ D^{n} F) (n)$
64	48 63	eqssd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n) = dom F$
65	64	expr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land n \in ℕ_{0}) \to (dom (ℂ D^{n} F) (n + 1) = dom F \to dom (ℂ D^{n} F) (n) = dom F)$
66	65	imim1d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land n \in ℕ_{0}) \to ((dom (ℂ D^{n} F) (n) = dom F \to (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S}) \to (dom (ℂ D^{n} F) (n + 1) = dom F \to (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S}))$
67		oveq2	$⊢ (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S} \to S D (S D^{n} ({F ↾}_{S})) (n) = S D ({(ℂ D^{n} F) (n) ↾}_{S})$
68	34	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to S \subseteq ℂ$
69	35	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to {F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S)$
70		dvnp1	$⊢ (S \subseteq ℂ \land {F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S) \land n \in ℕ_{0}) \to (S D^{n} ({F ↾}_{S})) (n + 1) = S D (S D^{n} ({F ↾}_{S})) (n)$
71	68 69 46 70	syl3anc	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to (S D^{n} ({F ↾}_{S})) (n + 1) = S D (S D^{n} ({F ↾}_{S})) (n)$
72	52	reseq1d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to {(ℂ D^{n} F) (n + 1) ↾}_{S} = {{(ℂ D^{n} F) (n)}_{ℂ}^{'} ↾}_{S}$
73		simpll	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to S \in \{ℝ, ℂ\}$
74		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
75	74	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
76		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
77	76	ntrss2	$⊢ (TopOpen (ℂ_{fld}) \in Top \land dom (ℂ D^{n} F) (n) \subseteq ℂ) \to int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n)) \subseteq dom (ℂ D^{n} F) (n)$
78	75 61 77	sylancr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n)) \subseteq dom (ℂ D^{n} F) (n)$
79	74	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
80	79	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
81	50 56 61 80 74	dvbssntr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom {(ℂ D^{n} F) (n)}_{ℂ}^{'} \subseteq int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n))$
82	54 81	eqsstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom F \subseteq int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n))$
83	48 82	sstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n) \subseteq int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n))$
84	78 83	eqssd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n)) = dom (ℂ D^{n} F) (n)$
85	76	isopn3	$⊢ (TopOpen (ℂ_{fld}) \in Top \land dom (ℂ D^{n} F) (n) \subseteq ℂ) \to (dom (ℂ D^{n} F) (n) \in TopOpen (ℂ_{fld}) \leftrightarrow int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n)) = dom (ℂ D^{n} F) (n))$
86	75 61 85	sylancr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to (dom (ℂ D^{n} F) (n) \in TopOpen (ℂ_{fld}) \leftrightarrow int (TopOpen (ℂ_{fld})) (dom (ℂ D^{n} F) (n)) = dom (ℂ D^{n} F) (n))$
87	84 86	mpbird	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom (ℂ D^{n} F) (n) \in TopOpen (ℂ_{fld})$
88	64 54	eqtr2d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to dom {(ℂ D^{n} F) (n)}_{ℂ}^{'} = dom (ℂ D^{n} F) (n)$
89	74	dvres3a	$⊢ ((S \in \{ℝ, ℂ\} \land (ℂ D^{n} F) (n) : dom (ℂ D^{n} F) (n) ⟶ ℂ) \land (dom (ℂ D^{n} F) (n) \in TopOpen (ℂ_{fld}) \land dom {(ℂ D^{n} F) (n)}_{ℂ}^{'} = dom (ℂ D^{n} F) (n))) \to S D ({(ℂ D^{n} F) (n) ↾}_{S}) = {{(ℂ D^{n} F) (n)}_{ℂ}^{'} ↾}_{S}$
90	73 56 87 88 89	syl22anc	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to S D ({(ℂ D^{n} F) (n) ↾}_{S}) = {{(ℂ D^{n} F) (n)}_{ℂ}^{'} ↾}_{S}$
91	72 90	eqtr4d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to {(ℂ D^{n} F) (n + 1) ↾}_{S} = S D ({(ℂ D^{n} F) (n) ↾}_{S})$
92	71 91	eqeq12d	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to ((S D^{n} ({F ↾}_{S})) (n + 1) = {(ℂ D^{n} F) (n + 1) ↾}_{S} \leftrightarrow S D (S D^{n} ({F ↾}_{S})) (n) = S D ({(ℂ D^{n} F) (n) ↾}_{S}))$
93	67 92	imbitrrid	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land (n \in ℕ_{0} \land dom (ℂ D^{n} F) (n + 1) = dom F)) \to ((S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S} \to (S D^{n} ({F ↾}_{S})) (n + 1) = {(ℂ D^{n} F) (n + 1) ↾}_{S})$
94	66 93	animpimp2impd	$⊢ n \in ℕ_{0} \to (((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (n) = dom F \to (S D^{n} ({F ↾}_{S})) (n) = {(ℂ D^{n} F) (n) ↾}_{S})) \to ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (n + 1) = dom F \to (S D^{n} ({F ↾}_{S})) (n + 1) = {(ℂ D^{n} F) (n + 1) ↾}_{S})))$
95	8 16 24 32 43 94	nn0ind	$⊢ N \in ℕ_{0} \to ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (dom (ℂ D^{n} F) (N) = dom F \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S}))$
96	95	com12	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (N \in ℕ_{0} \to (dom (ℂ D^{n} F) (N) = dom F \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S}))$
97	96	3impia	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land N \in ℕ_{0}) \to (dom (ℂ D^{n} F) (N) = dom F \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S})$
98	97	imp	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land N \in ℕ_{0}) \land dom (ℂ D^{n} F) (N) = dom F) \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S}$

Metamath Proof Explorer

Theorem dvnres

Proof