cpnord - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cpnord		Structured version Visualization version GIF version

Theorem cpnord 26164

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

**Assertion**
Ref	Expression
cpnord	⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) → ((𝓑C^𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))

Proof of Theorem cpnord Dummy variables 𝑓 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6882	. . . . . 6 ⊢ (𝑛 = 𝑀 → ((𝓑C^𝑛‘𝑆)‘𝑛) = ((𝓑C^𝑛‘𝑆)‘𝑀))
2	1	sseq1d 3965	. . . . 5 ⊢ (𝑛 = 𝑀 → (((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) ↔ ((𝓑C^𝑛‘𝑆)‘𝑀) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
3	2	imbi2d 343	. . . 4 ⊢ (𝑛 = 𝑀 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑀) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))))
4		fveq2 6882	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝓑C^𝑛‘𝑆)‘𝑛) = ((𝓑C^𝑛‘𝑆)‘𝑚))
5	4	sseq1d 3965	. . . . 5 ⊢ (𝑛 = 𝑚 → (((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) ↔ ((𝓑C^𝑛‘𝑆)‘𝑚) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
6	5	imbi2d 343	. . . 4 ⊢ (𝑛 = 𝑚 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑚) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))))
7		fveq2 6882	. . . . . 6 ⊢ (𝑛 = (𝑚 + 1) → ((𝓑C^𝑛‘𝑆)‘𝑛) = ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)))
8	7	sseq1d 3965	. . . . 5 ⊢ (𝑛 = (𝑚 + 1) → (((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) ↔ ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
9	8	imbi2d 343	. . . 4 ⊢ (𝑛 = (𝑚 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))))
10		fveq2 6882	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((𝓑C^𝑛‘𝑆)‘𝑛) = ((𝓑C^𝑛‘𝑆)‘𝑁))
11	10	sseq1d 3965	. . . . 5 ⊢ (𝑛 = 𝑁 → (((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) ↔ ((𝓑C^𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
12	11	imbi2d 343	. . . 4 ⊢ (𝑛 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑛) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))))
13		ssid 3956	. . . . 5 ⊢ ((𝓑C^𝑛‘𝑆)‘𝑀) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)
14	13	2a1i 12	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑀) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
15		simprl 783	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑓 ∈ (ℂ ↑_pm 𝑆))
16		recnprss 26133	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
17	16	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑆 ⊆ ℂ)
18	17	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ⊆ ℂ)
19		simplll 787	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ∈ {ℝ, ℂ})
20		eluznn0 12969	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ ℕ₀)
21	20	adantll 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ ℕ₀)
22	21	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑚 ∈ ℕ₀)
23		dvnf 26156	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑚 ∈ ℕ₀) → ((𝑆 D^𝑛 𝑓)‘𝑚):dom ((𝑆 D^𝑛 𝑓)‘𝑚)⟶ℂ)
24	19, 15, 22, 23	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D^𝑛 𝑓)‘𝑚):dom ((𝑆 D^𝑛 𝑓)‘𝑚)⟶ℂ)
25		dvnbss 26157	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑚 ∈ ℕ₀) → dom ((𝑆 D^𝑛 𝑓)‘𝑚) ⊆ dom 𝑓)
26	19, 15, 22, 25	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D^𝑛 𝑓)‘𝑚) ⊆ dom 𝑓)
27		dvnp1 26154	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ⊆ ℂ ∧ 𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑚 ∈ ℕ₀) → ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)))
28	18, 15, 22, 27	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)))
29		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))
30	28, 29	eqeltrrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ))
31		cncff 25122	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ) → (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ)
32	30, 31	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ)
33	32	fdmd 6717	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)) = dom 𝑓)
34		cnex 11208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ∈ V
35		elpm2g 8846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → (𝑓 ∈ (ℂ ↑_pm 𝑆) ↔ (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆)))
36	34, 19, 35	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑_pm 𝑆) ↔ (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆)))
37	15, 36	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆))
38	37	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ 𝑆)
39	26, 38	sstrd 3944	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D^𝑛 𝑓)‘𝑚) ⊆ 𝑆)
40	18, 24, 39	dvbss 26130	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)) ⊆ dom ((𝑆 D^𝑛 𝑓)‘𝑚))
41	33, 40	eqsstrrd 3969	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ dom ((𝑆 D^𝑛 𝑓)‘𝑚))
42	26, 41	eqssd 3951	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D^𝑛 𝑓)‘𝑚) = dom 𝑓)
43	42	feq2d 6690	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (((𝑆 D^𝑛 𝑓)‘𝑚):dom ((𝑆 D^𝑛 𝑓)‘𝑚)⟶ℂ ↔ ((𝑆 D^𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ))
44	24, 43	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D^𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ)
45		dvcn 26150	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆) ∧ dom (𝑆 D ((𝑆 D^𝑛 𝑓)‘𝑚)) = dom 𝑓) → ((𝑆 D^𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))
46	18, 44, 38, 33, 45	syl31anc 1400	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D^𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))
47	15, 46	jca 521	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))
48	47	ex 418	. . . . . . . . 9 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) → (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))))
49		peano2nn0 12571	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
50	21, 49	syl 18	. . . . . . . . . 10 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑚 + 1) ∈ ℕ₀)
51		elcpn 26163	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (𝑓 ∈ ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ↔ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))))
52	17, 50, 51	syl2anc 596	. . . . . . . . 9 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑓 ∈ ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ↔ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))))
53		elcpn 26163	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ 𝑚 ∈ ℕ₀) → (𝑓 ∈ ((𝓑C^𝑛‘𝑆)‘𝑚) ↔ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))))
54	17, 21, 53	syl2anc 596	. . . . . . . . 9 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑓 ∈ ((𝓑C^𝑛‘𝑆)‘𝑚) ↔ (𝑓 ∈ (ℂ ↑_pm 𝑆) ∧ ((𝑆 D^𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))))
55	48, 52, 54	3imtr4d 297	. . . . . . . 8 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑓 ∈ ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) → 𝑓 ∈ ((𝓑C^𝑛‘𝑆)‘𝑚)))
56	55	ssrdv 3940	. . . . . . 7 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑚))
57		sstr2 3941	. . . . . . 7 ⊢ (((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑚) → (((𝓑C^𝑛‘𝑆)‘𝑚) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) → ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
58	56, 57	syl 18	. . . . . 6 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (((𝓑C^𝑛‘𝑆)‘𝑚) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) → ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
59	58	expcom 419	. . . . 5 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → (((𝓑C^𝑛‘𝑆)‘𝑚) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀) → ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))))
60	59	a2d 30	. . . 4 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑚) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘(𝑚 + 1)) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))))
61	3, 6, 9, 12, 14, 60	uzind4 12958	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → ((𝓑C^𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
62	61	com12 33	. 2 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀) → (𝑁 ∈ (ℤ_≥‘𝑀) → ((𝓑C^𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀)))
63	62	3impia 1135	1 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) → ((𝓑C^𝑛‘𝑆)‘𝑁) ⊆ ((𝓑C^𝑛‘𝑆)‘𝑀))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 Vcvv 3453 ⊆ wss 3902 {cpr 4589 dom cdm 5659 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ↑_pm cpm 8830 ℂcc 11125 ℝcr 11126 1c1 11128 + caddc 11130 ℕ₀cn0 12531 ℤcz 12618 ℤ_≥cuz 12890 –cn→ccncf 25105 D cdv 26092 D^𝑛 cdvn 26093 𝓑C^𝑛ccpn 26094

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13045 df-xneg 13165 df-xadd 13166 df-xmul 13167 df-icc 13407 df-fz 13564 df-fzo 13712 df-seq 14068 df-exp 14128 df-hash 14397 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-hom 17370 df-cco 17371 df-rest 17511 df-topn 17512 df-0g 17530 df-gsum 17531 df-topgen 17532 df-pt 17533 df-prds 17536 df-xrs 17592 df-qtop 17597 df-imas 17598 df-xps 17600 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-limc 26095 df-dv 26096 df-dvn 26097 df-cpn 26098

This theorem is used by: cpncn 26165 c1lip2 26227

W3C validator