Proof of Theorem dvidlem
Step | Hyp | Ref
| Expression |
1 | | dvfcn 23478 |
. . . 4
⊢ (ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ |
2 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
4 | | dvidlem.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
5 | 3, 4, 3 | dvbss 23471 |
. . . . . 6
⊢ (𝜑 → dom (ℂ D 𝐹) ⊆
ℂ) |
6 | | reldv 23440 |
. . . . . . . . 9
⊢ Rel
(ℂ D 𝐹) |
7 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
8 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
9 | 8 | cnfldtop 22397 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈ Top |
10 | 8 | cnfldtopon 22396 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
11 | 10 | toponunii 20547 |
. . . . . . . . . . . . 13
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
12 | 11 | ntrtop 20684 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ∈ Top →
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ) |
13 | 9, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ |
14 | 7, 13 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
((int‘(TopOpen‘ℂfld))‘ℂ)) |
15 | | limcresi 23455 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ↦ 𝐵) limℂ 𝑥) ⊆ (((𝑧 ∈ ℂ ↦ 𝐵) ↾ (ℂ ∖ {𝑥})) limℂ 𝑥) |
16 | | dvidlem.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 ∈ ℂ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
18 | 2 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ℂ ⊆
ℂ) |
19 | | cncfmptc 22522 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℂ ∧ ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ ℂ ↦ 𝐵) ∈ (ℂ–cn→ℂ)) |
20 | 17, 18, 18, 19 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑧 ∈ ℂ ↦ 𝐵) ∈ (ℂ–cn→ℂ)) |
21 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → 𝐵 = 𝐵) |
22 | 20, 7, 21 | cnmptlimc 23460 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ((𝑧 ∈ ℂ ↦ 𝐵) limℂ 𝑥)) |
23 | 15, 22 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ (((𝑧 ∈ ℂ ↦ 𝐵) ↾ (ℂ ∖ {𝑥})) limℂ 𝑥)) |
24 | | eldifsn 4260 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (ℂ ∖ {𝑥}) ↔ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) |
25 | | dvidlem.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵) |
26 | 25 | 3exp2 1277 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ ℂ → (𝑧 ∈ ℂ → (𝑧 ≠ 𝑥 → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)))) |
27 | 26 | imp43 619 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵) |
28 | 24, 27 | sylan2b 491 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑧 ∈ (ℂ ∖ {𝑥})) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵) |
29 | 28 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (ℂ ∖ {𝑥}) ↦ 𝐵)) |
30 | | difss 3699 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {𝑥}) ⊆
ℂ |
31 | | resmpt 5369 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
∖ {𝑥}) ⊆
ℂ → ((𝑧 ∈
ℂ ↦ 𝐵) ↾
(ℂ ∖ {𝑥})) =
(𝑧 ∈ (ℂ ∖
{𝑥}) ↦ 𝐵)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ↦ 𝐵) ↾ (ℂ ∖
{𝑥})) = (𝑧 ∈ (ℂ ∖ {𝑥}) ↦ 𝐵) |
33 | 29, 32 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = ((𝑧 ∈ ℂ ↦ 𝐵) ↾ (ℂ ∖ {𝑥}))) |
34 | 33 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥) = (((𝑧 ∈ ℂ ↦ 𝐵) ↾ (ℂ ∖ {𝑥})) limℂ 𝑥)) |
35 | 23, 34 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ((𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) |
36 | 11 | restid 15917 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
37 | 9, 36 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
38 | 37 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
39 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
40 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐹:ℂ⟶ℂ) |
41 | 38, 8, 39, 18, 40, 18 | eldv 23468 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥(ℂ D 𝐹)𝐵 ↔ (𝑥 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 𝐵 ∈ ((𝑧 ∈ (ℂ ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
42 | 14, 35, 41 | mpbir2and 959 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥(ℂ D 𝐹)𝐵) |
43 | | releldm 5279 |
. . . . . . . . 9
⊢ ((Rel
(ℂ D 𝐹) ∧ 𝑥(ℂ D 𝐹)𝐵) → 𝑥 ∈ dom (ℂ D 𝐹)) |
44 | 6, 42, 43 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ dom (ℂ D 𝐹)) |
45 | 44 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D 𝐹))) |
46 | 45 | ssrdv 3574 |
. . . . . 6
⊢ (𝜑 → ℂ ⊆ dom
(ℂ D 𝐹)) |
47 | 5, 46 | eqssd 3585 |
. . . . 5
⊢ (𝜑 → dom (ℂ D 𝐹) = ℂ) |
48 | 47 | feq2d 5944 |
. . . 4
⊢ (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ
D 𝐹):ℂ⟶ℂ)) |
49 | 1, 48 | mpbii 222 |
. . 3
⊢ (𝜑 → (ℂ D 𝐹):ℂ⟶ℂ) |
50 | | ffn 5958 |
. . 3
⊢ ((ℂ
D 𝐹):ℂ⟶ℂ
→ (ℂ D 𝐹) Fn
ℂ) |
51 | 49, 50 | syl 17 |
. 2
⊢ (𝜑 → (ℂ D 𝐹) Fn ℂ) |
52 | | fnconstg 6006 |
. . 3
⊢ (𝐵 ∈ ℂ → (ℂ
× {𝐵}) Fn
ℂ) |
53 | 16, 52 | mp1i 13 |
. 2
⊢ (𝜑 → (ℂ × {𝐵}) Fn ℂ) |
54 | | ffun 5961 |
. . . . . 6
⊢ ((ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ → Fun
(ℂ D 𝐹)) |
55 | 1, 54 | mp1i 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → Fun (ℂ D 𝐹)) |
56 | | funbrfvb 6148 |
. . . . 5
⊢ ((Fun
(ℂ D 𝐹) ∧ 𝑥 ∈ dom (ℂ D 𝐹)) → (((ℂ D 𝐹)‘𝑥) = 𝐵 ↔ 𝑥(ℂ D 𝐹)𝐵)) |
57 | 55, 44, 56 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D 𝐹)‘𝑥) = 𝐵 ↔ 𝑥(ℂ D 𝐹)𝐵)) |
58 | 42, 57 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((ℂ D 𝐹)‘𝑥) = 𝐵) |
59 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℂ) |
60 | | fvconst2g 6372 |
. . . 4
⊢ ((𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
((ℂ × {𝐵})‘𝑥) = 𝐵) |
61 | 59, 60 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((ℂ ×
{𝐵})‘𝑥) = 𝐵) |
62 | 58, 61 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((ℂ D 𝐹)‘𝑥) = ((ℂ × {𝐵})‘𝑥)) |
63 | 51, 53, 62 | eqfnfvd 6222 |
1
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵})) |