Step | Hyp | Ref
| Expression |
1 | | ax-resscn 9872 |
. . . . 5
⊢ ℝ
⊆ ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ⊆
ℂ) |
3 | | dvcj.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
4 | | dvcj.x |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
5 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
6 | 5 | tgioo2 22414 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
7 | 2, 3, 4, 6, 5 | dvbssntr 23470 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆
((int‘(topGen‘ran (,)))‘𝑋)) |
8 | | dvcj.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹)) |
9 | 7, 8 | sseldd 3569 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋)) |
10 | 4, 1 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
11 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → ℝ ⊆
ℂ) |
12 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝐹:𝑋⟶ℂ) |
13 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝑋 ⊆ ℝ) |
14 | 11, 12, 13 | dvbss 23471 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → dom (ℝ D
𝐹) ⊆ 𝑋) |
15 | 3, 4, 14 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ 𝑋) |
16 | 15, 8 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
17 | 3, 10, 16 | dvlem 23466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)) ∈ ℂ) |
18 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) |
19 | 17, 18 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ) |
20 | | ssid 3587 |
. . . . 5
⊢ ℂ
⊆ ℂ |
21 | 20 | a1i 11 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
22 | 5 | cnfldtopon 22396 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
23 | 22 | toponunii 20547 |
. . . . . . 7
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
24 | 23 | restid 15917 |
. . . . . 6
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
25 | 22, 24 | ax-mp 5 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
26 | 25 | eqcomi 2619 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
27 | | dvf 23477 |
. . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
28 | | ffun 5961 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun
(ℝ D 𝐹)) |
29 | | funfvbrb 6238 |
. . . . . . . 8
⊢ (Fun
(ℝ D 𝐹) → (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))) |
30 | 27, 28, 29 | mp2b 10 |
. . . . . . 7
⊢ (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)) |
31 | 8, 30 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)) |
32 | 6, 5, 18, 2, 3, 4 | eldv 23468 |
. . . . . 6
⊢ (𝜑 → (𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶) ↔ (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
33 | 31, 32 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))) |
34 | 33 | simprd 478 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
35 | | cjcncf 22515 |
. . . . . 6
⊢ ∗
∈ (ℂ–cn→ℂ) |
36 | 5 | cncfcn1 22521 |
. . . . . 6
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
37 | 35, 36 | eleqtri 2686 |
. . . . 5
⊢ ∗
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
38 | 27 | ffvelrni 6266 |
. . . . . 6
⊢ (𝐶 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝐶) ∈ ℂ) |
39 | 8, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ℂ) |
40 | 23 | cncnpi 20892 |
. . . . 5
⊢
((∗ ∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ℂ) → ∗ ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶))) |
41 | 37, 39, 40 | sylancr 694 |
. . . 4
⊢ (𝜑 → ∗ ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶))) |
42 | 19, 21, 5, 26, 34, 41 | limccnp 23461 |
. . 3
⊢ (𝜑 → (∗‘((ℝ
D 𝐹)‘𝐶)) ∈ ((∗ ∘
(𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶)) |
43 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) |
44 | | cjf 13692 |
. . . . . . . 8
⊢
∗:ℂ⟶ℂ |
45 | 44 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
∗:ℂ⟶ℂ) |
46 | 45 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → ∗ = (𝑦 ∈ ℂ ↦
(∗‘𝑦))) |
47 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)) → (∗‘𝑦) = (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) |
48 | 17, 43, 46, 47 | fmptco 6303 |
. . . . 5
⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))))) |
49 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
50 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ∈ 𝑋) |
51 | 50 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ 𝑋) |
52 | 49, 51 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝑥) ∈ ℂ) |
53 | 3, 16 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
54 | 53 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
55 | 52, 54 | subcld 10271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑥) − (𝐹‘𝐶)) ∈ ℂ) |
56 | 4 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℝ) |
57 | 50, 56 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℝ) |
58 | 4, 16 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
59 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℝ) |
60 | 57, 59 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℝ) |
61 | 60 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℂ) |
62 | 57 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℂ) |
63 | 59 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℂ) |
64 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ≠ 𝐶) |
65 | 64 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ≠ 𝐶) |
66 | 62, 63, 65 | subne0d 10280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ≠ 0) |
67 | 55, 61, 66 | cjdivd 13811 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶)))) |
68 | | cjsub 13737 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) →
(∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
69 | 52, 54, 68 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
70 | | fvco3 6185 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑥 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥))) |
71 | 3, 50, 70 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥))) |
72 | | fvco3 6185 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝐶 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
73 | 3, 16, 72 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶))) |
75 | 71, 74 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶)))) |
76 | 69, 75 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶))) |
77 | 60 | cjred 13814 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(𝑥 − 𝐶)) = (𝑥 − 𝐶)) |
78 | 76, 77 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
79 | 67, 78 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
80 | 79 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))) |
81 | 48, 80 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))) |
82 | 81 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶) = ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
83 | 42, 82 | eleqtrd 2690 |
. 2
⊢ (𝜑 → (∗‘((ℝ
D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)) |
84 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) |
85 | | fco 5971 |
. . . 4
⊢
((∗:ℂ⟶ℂ ∧ 𝐹:𝑋⟶ℂ) → (∗ ∘
𝐹):𝑋⟶ℂ) |
86 | 44, 3, 85 | sylancr 694 |
. . 3
⊢ (𝜑 → (∗ ∘ 𝐹):𝑋⟶ℂ) |
87 | 6, 5, 84, 2, 86, 4 | eldv 23468 |
. 2
⊢ (𝜑 → (𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶)) ↔ (𝐶 ∈ ((int‘(topGen‘ran
(,)))‘𝑋) ∧
(∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
88 | 9, 83, 87 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶))) |