Step | Hyp | Ref
| Expression |
1 | | ax-resscn 10956 |
. . . . 5
⊢ ℝ
⊆ ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ⊆
ℂ) |
3 | | dvcj.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
4 | | dvcj.x |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
5 | | eqid 2733 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
6 | 5 | tgioo2 23994 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
7 | 2, 3, 4, 6, 5 | dvbssntr 25092 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆
((int‘(topGen‘ran (,)))‘𝑋)) |
8 | | dvcj.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹)) |
9 | 7, 8 | sseldd 3924 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋)) |
10 | 4, 1 | sstrdi 3935 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
11 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → ℝ ⊆
ℂ) |
12 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝐹:𝑋⟶ℂ) |
13 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝑋 ⊆ ℝ) |
14 | 11, 12, 13 | dvbss 25093 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → dom (ℝ D
𝐹) ⊆ 𝑋) |
15 | 3, 4, 14 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ 𝑋) |
16 | 15, 8 | sseldd 3924 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
17 | 3, 10, 16 | dvlem 25088 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)) ∈ ℂ) |
18 | 17 | fmpttd 7009 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ) |
19 | | ssidd 3946 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
20 | 5 | cnfldtopon 23974 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
21 | 20 | toponrestid 22098 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
22 | | dvf 25099 |
. . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
23 | | ffun 6621 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun
(ℝ D 𝐹)) |
24 | | funfvbrb 6948 |
. . . . . . . 8
⊢ (Fun
(ℝ D 𝐹) → (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))) |
25 | 22, 23, 24 | mp2b 10 |
. . . . . . 7
⊢ (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)) |
26 | 8, 25 | sylib 217 |
. . . . . 6
⊢ (𝜑 → 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)) |
27 | | eqid 2733 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) |
28 | 6, 5, 27, 2, 3, 4 | eldv 25090 |
. . . . . 6
⊢ (𝜑 → (𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶) ↔ (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
29 | 26, 28 | mpbid 231 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))) |
30 | 29 | simprd 495 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
31 | | cjcncf 24095 |
. . . . . 6
⊢ ∗
∈ (ℂ–cn→ℂ) |
32 | 5 | cncfcn1 24102 |
. . . . . 6
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
33 | 31, 32 | eleqtri 2832 |
. . . . 5
⊢ ∗
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
34 | 22 | ffvelcdmi 6980 |
. . . . . 6
⊢ (𝐶 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝐶) ∈ ℂ) |
35 | 8, 34 | syl 17 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ℂ) |
36 | | unicntop 23977 |
. . . . . 6
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
37 | 36 | cncnpi 22457 |
. . . . 5
⊢
((∗ ∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ℂ) → ∗ ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶))) |
38 | 33, 35, 37 | sylancr 586 |
. . . 4
⊢ (𝜑 → ∗ ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶))) |
39 | 18, 19, 5, 21, 30, 38 | limccnp 25083 |
. . 3
⊢ (𝜑 → (∗‘((ℝ
D 𝐹)‘𝐶)) ∈ ((∗ ∘
(𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶)) |
40 | | cjf 14843 |
. . . . . . 7
⊢
∗:ℂ⟶ℂ |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
∗:ℂ⟶ℂ) |
42 | 41, 17 | cofmpt 7024 |
. . . . 5
⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))))) |
43 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
44 | | eldifi 4064 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ∈ 𝑋) |
45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ 𝑋) |
46 | 43, 45 | ffvelcdmd 6982 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝑥) ∈ ℂ) |
47 | 3, 16 | ffvelcdmd 6982 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
48 | 47 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
49 | 46, 48 | subcld 11360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑥) − (𝐹‘𝐶)) ∈ ℂ) |
50 | 4 | sselda 3923 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℝ) |
51 | 44, 50 | sylan2 592 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℝ) |
52 | 4, 16 | sseldd 3924 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
53 | 52 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℝ) |
54 | 51, 53 | resubcld 11431 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℝ) |
55 | 54 | recnd 11031 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℂ) |
56 | 51 | recnd 11031 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℂ) |
57 | 53 | recnd 11031 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℂ) |
58 | | eldifsni 4726 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ≠ 𝐶) |
59 | 58 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ≠ 𝐶) |
60 | 56, 57, 59 | subne0d 11369 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ≠ 0) |
61 | 49, 55, 60 | cjdivd 14962 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶)))) |
62 | | cjsub 14888 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) →
(∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
63 | 46, 48, 62 | syl2anc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
64 | | fvco3 6887 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑥 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥))) |
65 | 3, 44, 64 | syl2an 595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥))) |
66 | | fvco3 6887 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝐶 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
67 | 3, 16, 66 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
68 | 67 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
69 | 65, 68 | oveq12d 7313 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
70 | 63, 69 | eqtr4d 2776 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶))) |
71 | 54 | cjred 14965 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(𝑥 − 𝐶)) = (𝑥 − 𝐶)) |
72 | 70, 71 | oveq12d 7313 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
73 | 61, 72 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
74 | 73 | mpteq2dva 5177 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))) |
75 | 42, 74 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))) |
76 | 75 | oveq1d 7310 |
. . 3
⊢ (𝜑 → ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶) = ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
77 | 39, 76 | eleqtrd 2836 |
. 2
⊢ (𝜑 → (∗‘((ℝ
D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
78 | | eqid 2733 |
. . 3
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
79 | | fco 6642 |
. . . 4
⊢
((∗:ℂ⟶ℂ ∧ 𝐹:𝑋⟶ℂ) → (∗ ∘
𝐹):𝑋⟶ℂ) |
80 | 40, 3, 79 | sylancr 586 |
. . 3
⊢ (𝜑 → (∗ ∘ 𝐹):𝑋⟶ℂ) |
81 | 6, 5, 78, 2, 80, 4 | eldv 25090 |
. 2
⊢ (𝜑 → (𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶)) ↔ (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
(∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
82 | 9, 77, 81 | mpbir2and 709 |
1
⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶))) |