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	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑛 = 𝑀 → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) = ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) )
2	1	sseq1d	⊢ ( 𝑛 = 𝑀 → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ↔ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
3	2	imbi2d	⊢ ( 𝑛 = 𝑀 → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ↔ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ) )
4		fveq2	⊢ ( 𝑛 = 𝑚 → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) = ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) )
5	4	sseq1d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ↔ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
6	5	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ↔ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ) )
7		fveq2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) = ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) )
8	7	sseq1d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ↔ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
9	8	imbi2d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ↔ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ) )
10		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) = ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) )
11	10	sseq1d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ↔ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
12	11	imbi2d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑛 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ↔ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ) )
13		ssid	⊢ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 )
14	13	2a1i	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
15		simprl	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) )
16		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
17	16	ad2antrr	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑆 ⊆ ℂ )
18	17	adantr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → 𝑆 ⊆ ℂ )
19		simplll	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → 𝑆 ∈ { ℝ , ℂ } )
20		eluznn0	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑚 ∈ ℕ₀ )
21	20	adantll	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑚 ∈ ℕ₀ )
22	21	adantr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → 𝑚 ∈ ℕ₀ )
23		dvnf	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) : dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ⟶ ℂ )
24	19 15 22 23	syl3anc	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) : dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ⟶ ℂ )
25		dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑚 ∈ ℕ₀ ) → dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ⊆ dom 𝑓 )
26	19 15 22 25	syl3anc	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ⊆ dom 𝑓 )
27		dvnp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) )
28	18 15 22 27	syl3anc	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) )
29		simprr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) )
30	28 29	eqeltrrd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) )
31		cncff	⊢ ( ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) → ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) : dom 𝑓 ⟶ ℂ )
32	30 31	syl	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) : dom 𝑓 ⟶ ℂ )
33	32	fdmd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) = dom 𝑓 )
34		cnex	⊢ ℂ ∈ V
35		elpm2g	⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) → ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ↔ ( 𝑓 : dom 𝑓 ⟶ ℂ ∧ dom 𝑓 ⊆ 𝑆 ) ) )
36	34 19 35	sylancr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ↔ ( 𝑓 : dom 𝑓 ⟶ ℂ ∧ dom 𝑓 ⊆ 𝑆 ) ) )
37	15 36	mpbid	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( 𝑓 : dom 𝑓 ⟶ ℂ ∧ dom 𝑓 ⊆ 𝑆 ) )
38	37	simprd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom 𝑓 ⊆ 𝑆 )
39	26 38	sstrd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ⊆ 𝑆 )
40	18 24 39	dvbss	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) ⊆ dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) )
41	33 40	eqsstrrd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom 𝑓 ⊆ dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) )
42	26 41	eqssd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) = dom 𝑓 )
43	42	feq2d	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) : dom ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ⟶ ℂ ↔ ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) : dom 𝑓 ⟶ ℂ ) )
44	24 43	mpbid	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) : dom 𝑓 ⟶ ℂ )
45		dvcn	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) : dom 𝑓 ⟶ ℂ ∧ dom 𝑓 ⊆ 𝑆 ) ∧ dom ( 𝑆 D ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ) = dom 𝑓 ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ∈ ( dom 𝑓 –cn→ ℂ ) )
46	18 44 38 33 45	syl31anc	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ∈ ( dom 𝑓 –cn→ ℂ ) )
47	15 46	jca	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) ∧ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) → ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ∈ ( dom 𝑓 –cn→ ℂ ) ) )
48	47	ex	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) → ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) )
49		peano2nn0	⊢ ( 𝑚 ∈ ℕ₀ → ( 𝑚 + 1 ) ∈ ℕ₀ )
50	21 49	syl	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝑚 + 1 ) ∈ ℕ₀ )
51		elcpn	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑚 + 1 ) ∈ ℕ₀ ) → ( 𝑓 ∈ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ↔ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) )
52	17 50 51	syl2anc	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝑓 ∈ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ↔ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ ( 𝑚 + 1 ) ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) )
53		elcpn	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑚 ∈ ℕ₀ ) → ( 𝑓 ∈ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ↔ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) )
54	17 21 53	syl2anc	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝑓 ∈ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ↔ ( 𝑓 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 𝑓 ) ‘ 𝑚 ) ∈ ( dom 𝑓 –cn→ ℂ ) ) ) )
55	48 52 54	3imtr4d	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝑓 ∈ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) → 𝑓 ∈ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ) )
56	55	ssrdv	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) )
57		sstr2	⊢ ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
58	56 57	syl	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
59	58	expcom	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ) )
60	59	a2d	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑚 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) → ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ ( 𝑚 + 1 ) ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) ) )
61	3 6 9 12 14 60	uzind4	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
62	61	com12	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ) → ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) ) )
63	62	3impia	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝒞^𝑛 ‘ 𝑆 ) ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem cpnord

Proof