This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ ℂ ) ) ) )