Metamath Proof Explorer

Theorem dvcjbr

Description: The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj . (This doesn't follow from dvcobr because * is not a function on the reals, and even if we used complex derivatives, * is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvcj.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvcj.x ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
dvcj.c ⊢ ( 𝜑 → 𝐶 ∈ dom ( ℝ D 𝐹 ) )
Assertion dvcjbr ( 𝜑 → 𝐶 ( ℝ D ( ∗ ∘ 𝐹 ) ) ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dvcj.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
2 dvcj.x ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
3 dvcj.c ⊢ ( 𝜑 → 𝐶 ∈ dom ( ℝ D 𝐹 ) )
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 4 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
6 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
7 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
8 5 1 2 6 7 dvbssntr ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) )
9 8 3 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) )
10 2 4 sstrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
11 4 a1i ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ℝ ⊆ ℂ )
12 simpl ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → 𝐹 : 𝑋 ⟶ ℂ )
13 simpr ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → 𝑋 ⊆ ℝ )
14 11 12 13 dvbss ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → dom ( ℝ D 𝐹 ) ⊆ 𝑋 )
15 1 2 14 syl2anc ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ 𝑋 )
16 15 3 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
17 1 10 16 dvlem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ∈ ℂ )
18 17 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) : ( 𝑋 ∖ { 𝐶 } ) ⟶ ℂ )
19 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
20 7 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
21 20 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
22 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
23 ffun ⊢ ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ → Fun ( ℝ D 𝐹 ) )
24 funfvbrb ⊢ ( Fun ( ℝ D 𝐹 ) → ( 𝐶 ∈ dom ( ℝ D 𝐹 ) ↔ 𝐶 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) )
25 22 23 24 mp2b ⊢ ( 𝐶 ∈ dom ( ℝ D 𝐹 ) ↔ 𝐶 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝐶 ) )
26 3 25 sylib ⊢ ( 𝜑 → 𝐶 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝐶 ) )
27 eqid ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) = ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) )
28 6 7 27 5 1 2 eldv ⊢ ( 𝜑 → ( 𝐶 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ↔ ( 𝐶 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
29 26 28 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
30 29 simprd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) limℂ 𝐶 ) )
31 cjcncf ⊢ ∗ ∈ ( ℂ –cn→ ℂ )
32 7 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
33 31 32 eleqtri ⊢ ∗ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
34 22 ffvelcdmi ⊢ ( 𝐶 ∈ dom ( ℝ D 𝐹 ) → ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ∈ ℂ )
35 3 34 syl ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ∈ ℂ )
36 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
37 36 cncnpi ⊢ ( ( ∗ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ∈ ℂ ) → ∗ ∈ ( ( ( TopOpen ‘ ℂfld ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) )
38 33 35 37 sylancr ⊢ ( 𝜑 → ∗ ∈ ( ( ( TopOpen ‘ ℂfld ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) )
39 18 19 7 21 30 38 limccnp ⊢ ( 𝜑 → ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( ∗ ∘ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) ) limℂ 𝐶 ) )
40 cjf ⊢ ∗ : ℂ ⟶ ℂ
41 40 a1i ⊢ ( 𝜑 → ∗ : ℂ ⟶ ℂ )
42 41 17 cofmpt ⊢ ( 𝜑 → ( ∗ ∘ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) ) = ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ∗ ‘ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) ) )
43 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝐹 : 𝑋 ⟶ ℂ )
44 eldifi ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) → 𝑥 ∈ 𝑋 )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑥 ∈ 𝑋 )
46 43 45 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
47 1 16 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
49 46 48 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
50 2 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℝ )
51 44 50 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑥 ∈ ℝ )
52 2 16 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝐶 ∈ ℝ )
54 51 53 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝑥 − 𝐶 ) ∈ ℝ )
55 54 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝑥 − 𝐶 ) ∈ ℂ )
56 51 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑥 ∈ ℂ )
57 53 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
58 eldifsni ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) → 𝑥 ≠ 𝐶 )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑥 ≠ 𝐶 )
60 56 57 59 subne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝑥 − 𝐶 ) ≠ 0 )
61 49 55 60 cjdivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ∗ ‘ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) = ( ( ∗ ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) ) / ( ∗ ‘ ( 𝑥 − 𝐶 ) ) ) )
62 cjsub ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℂ ) → ( ∗ ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) − ( ∗ ‘ ( 𝐹 ‘ 𝐶 ) ) ) )
63 46 48 62 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ∗ ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) − ( ∗ ‘ ( 𝐹 ‘ 𝐶 ) ) ) )
64 fvco3 ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) )
65 1 44 64 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) )
66 fvco3 ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) = ( ∗ ‘ ( 𝐹 ‘ 𝐶 ) ) )
67 1 16 66 syl2anc ⊢ ( 𝜑 → ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) = ( ∗ ‘ ( 𝐹 ‘ 𝐶 ) ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) = ( ∗ ‘ ( 𝐹 ‘ 𝐶 ) ) )
69 65 68 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) − ( ∗ ‘ ( 𝐹 ‘ 𝐶 ) ) ) )
70 63 69 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ∗ ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) )
71 54 cjred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ∗ ‘ ( 𝑥 − 𝐶 ) ) = ( 𝑥 − 𝐶 ) )
72 70 71 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ∗ ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) ) / ( ∗ ‘ ( 𝑥 − 𝐶 ) ) ) = ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) )
73 61 72 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ∗ ‘ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) = ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) )
74 73 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ∗ ‘ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) ) = ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) )
75 42 74 eqtrd ⊢ ( 𝜑 → ( ∗ ∘ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) ) = ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) )
76 75 oveq1d ⊢ ( 𝜑 → ( ( ∗ ∘ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) ) limℂ 𝐶 ) = ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) limℂ 𝐶 ) )
77 39 76 eleqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) limℂ 𝐶 ) )
78 eqid ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) = ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) )
79 fco ⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ) → ( ∗ ∘ 𝐹 ) : 𝑋 ⟶ ℂ )
80 40 1 79 sylancr ⊢ ( 𝜑 → ( ∗ ∘ 𝐹 ) : 𝑋 ⟶ ℂ )
81 6 7 78 5 80 2 eldv ⊢ ( 𝜑 → ( 𝐶 ( ℝ D ( ∗ ∘ 𝐹 ) ) ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) ↔ ( 𝐶 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ∧ ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( ( ∗ ∘ 𝐹 ) ‘ 𝑥 ) − ( ( ∗ ∘ 𝐹 ) ‘ 𝐶 ) ) / ( 𝑥 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
82 9 77 81 mpbir2and ⊢ ( 𝜑 → 𝐶 ( ℝ D ( ∗ ∘ 𝐹 ) ) ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝐶 ) ) )