dvn2bss

Description: An N-times differentiable point is an M-times differentiable point, if M <_ N . (Contributed by Mario Carneiro, 30-Dec-2016)

		Ref	Expression
	Assertion	dvn2bss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (M)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to S \in \{ℝ, ℂ\}$
2		simp2	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
3		elfznn0	$⊢ M \in (0 \dots N) \to M \in ℕ_{0}$
4	3	3ad2ant3	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to M \in ℕ_{0}$
5		elfzuz3	$⊢ M \in (0 \dots N) \to N \in ℤ_{\geq M}$
6	5	3ad2ant3	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to N \in ℤ_{\geq M}$
7		uznn0sub	$⊢ N \in ℤ_{\geq M} \to N - M \in ℕ_{0}$
8	6 7	syl	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to N - M \in ℕ_{0}$
9		dvnadd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (M \in ℕ_{0} \land N - M \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (M)) (N - M) = (S D^{n} F) (M + N - M)$
10	1 2 4 8 9	syl22anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to (S D^{n} (S D^{n} F) (M)) (N - M) = (S D^{n} F) (M + N - M)$
11	4	nn0cnd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to M \in ℂ$
12		elfzuz2	$⊢ M \in (0 \dots N) \to N \in ℤ_{\geq 0}$
13	12	3ad2ant3	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to N \in ℤ_{\geq 0}$
14		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
15	13 14	eleqtrrdi	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to N \in ℕ_{0}$
16	15	nn0cnd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to N \in ℂ$
17	11 16	pncan3d	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to M + N - M = N$
18	17	fveq2d	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to (S D^{n} F) (M + N - M) = (S D^{n} F) (N)$
19	10 18	eqtrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to (S D^{n} (S D^{n} F) (M)) (N - M) = (S D^{n} F) (N)$
20	19	dmeqd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom (S D^{n} (S D^{n} F) (M)) (N - M) = dom (S D^{n} F) (N)$
21		cnex	$⊢ ℂ \in V$
22	21	a1i	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to ℂ \in V$
23		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in ℕ_{0}) \to (S D^{n} F) (M) : dom (S D^{n} F) (M) ⟶ ℂ$
24	3 23	syl3an3	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to (S D^{n} F) (M) : dom (S D^{n} F) (M) ⟶ ℂ$
25		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in ℕ_{0}) \to dom (S D^{n} F) (M) \subseteq dom F$
26	3 25	syl3an3	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom (S D^{n} F) (M) \subseteq dom F$
27		elpmi	$⊢ F \in (ℂ ↑_{𝑝𝑚} S) \to (F : dom F ⟶ ℂ \land dom F \subseteq S)$
28	27	3ad2ant2	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to (F : dom F ⟶ ℂ \land dom F \subseteq S)$
29	28	simprd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom F \subseteq S$
30	26 29	sstrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom (S D^{n} F) (M) \subseteq S$
31		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land ((S D^{n} F) (M) : dom (S D^{n} F) (M) ⟶ ℂ \land dom (S D^{n} F) (M) \subseteq S)) \to (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S)$
32	22 1 24 30 31	syl22anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S)$
33		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land (S D^{n} F) (M) \in (ℂ ↑_{𝑝𝑚} S) \land N - M \in ℕ_{0}) \to dom (S D^{n} (S D^{n} F) (M)) (N - M) \subseteq dom (S D^{n} F) (M)$
34	1 32 8 33	syl3anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom (S D^{n} (S D^{n} F) (M)) (N - M) \subseteq dom (S D^{n} F) (M)$
35	20 34	eqsstrrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (M)$

Metamath Proof Explorer

Theorem dvn2bss

Proof