Theorem elcpn

Description: Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	elcpn	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpnfval	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
2	1	fveq1d	⊢ ( 𝑆 ⊆ ℂ → ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) = ( ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) ‘ 𝑁 ) )
3		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) )
4	3	eleq1d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) ↔ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) ) )
5	4	rabbidv	⊢ ( 𝑛 = 𝑁 → { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } = { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
6		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
7		ovex	⊢ ( ℂ ↑pm 𝑆 ) ∈ V
8	7	rabex	⊢ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ∈ V
9	5 6 8	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) ‘ 𝑁 ) = { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
10	2 9	sylan9eq	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) = { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
11	10	eleq2d	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
12		oveq2	⊢ ( 𝑓 = 𝐹 → ( 𝑆 D𝑛 𝑓 ) = ( 𝑆 D𝑛 𝐹 ) )
13	12	fveq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
14		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
15	14	oveq1d	⊢ ( 𝑓 = 𝐹 → ( dom 𝑓 –cn→ ℂ ) = ( dom 𝐹 –cn→ ℂ ) )
16	13 15	eleq12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) )
17	16	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑁 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ↔ ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) )
18	11 17	bitrdi	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )