Step | Hyp | Ref
| Expression |
1 | | ax-resscn 10673 |
. . . . 5
⊢ ℝ
⊆ ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ⊆
ℂ) |
3 | | dvcj.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
4 | | dvcj.x |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
5 | | eqid 2738 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
6 | 5 | tgioo2 23556 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
7 | 2, 3, 4, 6, 5 | dvbssntr 24652 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆
((int‘(topGen‘ran (,)))‘𝑋)) |
8 | | dvcj.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹)) |
9 | 7, 8 | sseldd 3879 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋)) |
10 | 4, 1 | sstrdi 3890 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
11 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → ℝ ⊆
ℂ) |
12 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝐹:𝑋⟶ℂ) |
13 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝑋 ⊆ ℝ) |
14 | 11, 12, 13 | dvbss 24653 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → dom (ℝ D
𝐹) ⊆ 𝑋) |
15 | 3, 4, 14 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ 𝑋) |
16 | 15, 8 | sseldd 3879 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
17 | 3, 10, 16 | dvlem 24648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)) ∈ ℂ) |
18 | 17 | fmpttd 6890 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ) |
19 | | ssidd 3901 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
20 | 5 | cnfldtopon 23536 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
21 | 20 | toponrestid 21673 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
22 | | dvf 24659 |
. . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
23 | | ffun 6508 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun
(ℝ D 𝐹)) |
24 | | funfvbrb 6829 |
. . . . . . . 8
⊢ (Fun
(ℝ D 𝐹) → (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))) |
25 | 22, 23, 24 | mp2b 10 |
. . . . . . 7
⊢ (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)) |
26 | 8, 25 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)) |
27 | | eqid 2738 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) |
28 | 6, 5, 27, 2, 3, 4 | eldv 24650 |
. . . . . 6
⊢ (𝜑 → (𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶) ↔ (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
29 | 26, 28 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))) |
30 | 29 | simprd 499 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
31 | | cjcncf 23657 |
. . . . . 6
⊢ ∗
∈ (ℂ–cn→ℂ) |
32 | 5 | cncfcn1 23664 |
. . . . . 6
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
33 | 31, 32 | eleqtri 2831 |
. . . . 5
⊢ ∗
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
34 | 22 | ffvelrni 6861 |
. . . . . 6
⊢ (𝐶 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝐶) ∈ ℂ) |
35 | 8, 34 | syl 17 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ℂ) |
36 | | unicntop 23539 |
. . . . . 6
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
37 | 36 | cncnpi 22030 |
. . . . 5
⊢
((∗ ∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ℂ) → ∗ ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶))) |
38 | 33, 35, 37 | sylancr 590 |
. . . 4
⊢ (𝜑 → ∗ ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶))) |
39 | 18, 19, 5, 21, 30, 38 | limccnp 24643 |
. . 3
⊢ (𝜑 → (∗‘((ℝ
D 𝐹)‘𝐶)) ∈ ((∗ ∘
(𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶)) |
40 | | cjf 14554 |
. . . . . . 7
⊢
∗:ℂ⟶ℂ |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
∗:ℂ⟶ℂ) |
42 | 41, 17 | cofmpt 6905 |
. . . . 5
⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))))) |
43 | 3 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
44 | | eldifi 4018 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ∈ 𝑋) |
45 | 44 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ 𝑋) |
46 | 43, 45 | ffvelrnd 6863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝑥) ∈ ℂ) |
47 | 3, 16 | ffvelrnd 6863 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
48 | 47 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
49 | 46, 48 | subcld 11076 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑥) − (𝐹‘𝐶)) ∈ ℂ) |
50 | 4 | sselda 3878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℝ) |
51 | 44, 50 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℝ) |
52 | 4, 16 | sseldd 3879 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
53 | 52 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℝ) |
54 | 51, 53 | resubcld 11147 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℝ) |
55 | 54 | recnd 10748 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℂ) |
56 | 51 | recnd 10748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℂ) |
57 | 53 | recnd 10748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℂ) |
58 | | eldifsni 4679 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ≠ 𝐶) |
59 | 58 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ≠ 𝐶) |
60 | 56, 57, 59 | subne0d 11085 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ≠ 0) |
61 | 49, 55, 60 | cjdivd 14673 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶)))) |
62 | | cjsub 14599 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) →
(∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
63 | 46, 48, 62 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
64 | | fvco3 6768 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑥 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥))) |
65 | 3, 44, 64 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥))) |
66 | | fvco3 6768 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝐶 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
67 | 3, 16, 66 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
68 | 67 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
69 | 65, 68 | oveq12d 7189 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
70 | 63, 69 | eqtr4d 2776 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶))) |
71 | 54 | cjred 14676 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(𝑥 − 𝐶)) = (𝑥 − 𝐶)) |
72 | 70, 71 | oveq12d 7189 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
73 | 61, 72 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
74 | 73 | mpteq2dva 5126 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))) |
75 | 42, 74 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))) |
76 | 75 | oveq1d 7186 |
. . 3
⊢ (𝜑 → ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶) = ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
77 | 39, 76 | eleqtrd 2835 |
. 2
⊢ (𝜑 → (∗‘((ℝ
D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
78 | | eqid 2738 |
. . 3
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
79 | | fco 6529 |
. . . 4
⊢
((∗:ℂ⟶ℂ ∧ 𝐹:𝑋⟶ℂ) → (∗ ∘
𝐹):𝑋⟶ℂ) |
80 | 40, 3, 79 | sylancr 590 |
. . 3
⊢ (𝜑 → (∗ ∘ 𝐹):𝑋⟶ℂ) |
81 | 6, 5, 78, 2, 80, 4 | eldv 24650 |
. 2
⊢ (𝜑 → (𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶)) ↔ (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
(∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
82 | 9, 77, 81 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶))) |