dvnres

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

		Ref	Expression
	Assertion	dvnres	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ 𝑁 ∈ ℕ₀ ) ∧ dom ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) = dom 𝐹 ) → ( ( 𝑆 D^𝑛 ( 𝐹 ↾ 𝑆 ) ) ‘ 𝑁 ) = ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) )

Proof

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

Metamath Proof Explorer

Theorem dvnres

Proof