cpnord

Description: C^n conditions are ordered by strength. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	cpnord	$⊢ (S \in \{ℝ, ℂ\} \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to C^{n} (S) (N) \subseteq C^{n} (S) (M)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ n = M \to C^{n} (S) (n) = C^{n} (S) (M)$
2	1	sseq1d	$⊢ n = M \to (C^{n} (S) (n) \subseteq C^{n} (S) (M) \leftrightarrow C^{n} (S) (M) \subseteq C^{n} (S) (M))$
3	2	imbi2d	$⊢ n = M \to (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (n) \subseteq C^{n} (S) (M)) \leftrightarrow ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (M) \subseteq C^{n} (S) (M)))$
4		fveq2	$⊢ n = m \to C^{n} (S) (n) = C^{n} (S) (m)$
5	4	sseq1d	$⊢ n = m \to (C^{n} (S) (n) \subseteq C^{n} (S) (M) \leftrightarrow C^{n} (S) (m) \subseteq C^{n} (S) (M))$
6	5	imbi2d	$⊢ n = m \to (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (n) \subseteq C^{n} (S) (M)) \leftrightarrow ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (m) \subseteq C^{n} (S) (M)))$
7		fveq2	$⊢ n = m + 1 \to C^{n} (S) (n) = C^{n} (S) (m + 1)$
8	7	sseq1d	$⊢ n = m + 1 \to (C^{n} (S) (n) \subseteq C^{n} (S) (M) \leftrightarrow C^{n} (S) (m + 1) \subseteq C^{n} (S) (M))$
9	8	imbi2d	$⊢ n = m + 1 \to (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (n) \subseteq C^{n} (S) (M)) \leftrightarrow ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (m + 1) \subseteq C^{n} (S) (M)))$
10		fveq2	$⊢ n = N \to C^{n} (S) (n) = C^{n} (S) (N)$
11	10	sseq1d	$⊢ n = N \to (C^{n} (S) (n) \subseteq C^{n} (S) (M) \leftrightarrow C^{n} (S) (N) \subseteq C^{n} (S) (M))$
12	11	imbi2d	$⊢ n = N \to (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (n) \subseteq C^{n} (S) (M)) \leftrightarrow ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (N) \subseteq C^{n} (S) (M)))$
13		ssid	$⊢ C^{n} (S) (M) \subseteq C^{n} (S) (M)$
14	13	2a1i	$⊢ M \in ℤ \to ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (M) \subseteq C^{n} (S) (M))$
15		simprl	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to f \in (ℂ ↑_{𝑝𝑚} S)$
16		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
17	16	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to S \subseteq ℂ$
18	17	adantr	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to S \subseteq ℂ$
19		simplll	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to S \in \{ℝ, ℂ\}$
20		eluznn0	$⊢ (M \in ℕ_{0} \land m \in ℤ_{\geq M}) \to m \in ℕ_{0}$
21	20	adantll	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to m \in ℕ_{0}$
22	21	adantr	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to m \in ℕ_{0}$
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	19 15 22 23	syl3anc	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \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	19 15 22 25	syl3anc	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom (S D^{n} f) (m) \subseteq dom f$
27		dvnp1	$⊢ (S \subseteq ℂ \land f \in (ℂ ↑_{𝑝𝑚} S) \land m \in ℕ_{0}) \to (S D^{n} f) (m + 1) = S D (S D^{n} f) (m)$
28	18 15 22 27	syl3anc	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (S D^{n} f) (m + 1) = S D (S D^{n} f) (m)$
29		simprr	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ$
30	28 29	eqeltrrd	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to {(S D^{n} f) (m)}_{S}^{'} : dom f \underset{cn}{⟶} ℂ$
31		cncff	$⊢ {(S D^{n} f) (m)}_{S}^{'} : dom f \underset{cn}{⟶} ℂ \to {(S D^{n} f) (m)}_{S}^{'} : dom f ⟶ ℂ$
32	30 31	syl	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to {(S D^{n} f) (m)}_{S}^{'} : dom f ⟶ ℂ$
33	32	fdmd	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom {(S D^{n} f) (m)}_{S}^{'} = dom f$
34		cnex	$⊢ ℂ \in V$
35		elpm2g	$⊢ (ℂ \in V \land S \in \{ℝ, ℂ\}) \to (f \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (f : dom f ⟶ ℂ \land dom f \subseteq S))$
36	34 19 35	sylancr	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (f \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (f : dom f ⟶ ℂ \land dom f \subseteq S))$
37	15 36	mpbid	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (f : dom f ⟶ ℂ \land dom f \subseteq S)$
38	37	simprd	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom f \subseteq S$
39	26 38	sstrd	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom (S D^{n} f) (m) \subseteq S$
40	18 24 39	dvbss	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom {(S D^{n} f) (m)}_{S}^{'} \subseteq dom (S D^{n} f) (m)$
41	33 40	eqsstrrd	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom f \subseteq dom (S D^{n} f) (m)$
42	26 41	eqssd	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to dom (S D^{n} f) (m) = dom f$
43	42	feq2d	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to ((S D^{n} f) (m) : dom (S D^{n} f) (m) ⟶ ℂ \leftrightarrow (S D^{n} f) (m) : dom f ⟶ ℂ)$
44	24 43	mpbid	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (S D^{n} f) (m) : dom f ⟶ ℂ$
45		dvcn	$⊢ ((S \subseteq ℂ \land (S D^{n} f) (m) : dom f ⟶ ℂ \land dom f \subseteq S) \land dom {(S D^{n} f) (m)}_{S}^{'} = dom f) \to (S D^{n} f) (m) : dom f \underset{cn}{⟶} ℂ$
46	18 44 38 33 45	syl31anc	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (S D^{n} f) (m) : dom f \underset{cn}{⟶} ℂ$
47	15 46	jca	$⊢ (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \land (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ)) \to (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m) : dom f \underset{cn}{⟶} ℂ)$
48	47	ex	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to ((f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ) \to (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m) : dom f \underset{cn}{⟶} ℂ))$
49		peano2nn0	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ_{0}$
50	21 49	syl	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to m + 1 \in ℕ_{0}$
51		elcpn	$⊢ (S \subseteq ℂ \land m + 1 \in ℕ_{0}) \to (f \in C^{n} (S) (m + 1) \leftrightarrow (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ))$
52	17 50 51	syl2anc	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to (f \in C^{n} (S) (m + 1) \leftrightarrow (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m + 1) : dom f \underset{cn}{⟶} ℂ))$
53		elcpn	$⊢ (S \subseteq ℂ \land m \in ℕ_{0}) \to (f \in C^{n} (S) (m) \leftrightarrow (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m) : dom f \underset{cn}{⟶} ℂ))$
54	17 21 53	syl2anc	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to (f \in C^{n} (S) (m) \leftrightarrow (f \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} f) (m) : dom f \underset{cn}{⟶} ℂ))$
55	48 52 54	3imtr4d	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to (f \in C^{n} (S) (m + 1) \to f \in C^{n} (S) (m))$
56	55	ssrdv	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to C^{n} (S) (m + 1) \subseteq C^{n} (S) (m)$
57		sstr2	$⊢ C^{n} (S) (m + 1) \subseteq C^{n} (S) (m) \to (C^{n} (S) (m) \subseteq C^{n} (S) (M) \to C^{n} (S) (m + 1) \subseteq C^{n} (S) (M))$
58	56 57	syl	$⊢ ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \land m \in ℤ_{\geq M}) \to (C^{n} (S) (m) \subseteq C^{n} (S) (M) \to C^{n} (S) (m + 1) \subseteq C^{n} (S) (M))$
59	58	expcom	$⊢ m \in ℤ_{\geq M} \to ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to (C^{n} (S) (m) \subseteq C^{n} (S) (M) \to C^{n} (S) (m + 1) \subseteq C^{n} (S) (M)))$
60	59	a2d	$⊢ m \in ℤ_{\geq M} \to (((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (m) \subseteq C^{n} (S) (M)) \to ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (m + 1) \subseteq C^{n} (S) (M)))$
61	3 6 9 12 14 60	uzind4	$⊢ N \in ℤ_{\geq M} \to ((S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to C^{n} (S) (N) \subseteq C^{n} (S) (M))$
62	61	com12	$⊢ (S \in \{ℝ, ℂ\} \land M \in ℕ_{0}) \to (N \in ℤ_{\geq M} \to C^{n} (S) (N) \subseteq C^{n} (S) (M))$
63	62	3impia	$⊢ (S \in \{ℝ, ℂ\} \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to C^{n} (S) (N) \subseteq C^{n} (S) (M)$

Metamath Proof Explorer

Theorem cpnord

Proof