Proof of Theorem dvlog
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
2 | 1 | cnfldtop 22587 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈ Top |
3 | 1 | cnfldtopon 22586 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
4 | 3 | toponunii 20721 |
. . . . . . 7
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
5 | 4 | restid 16094 |
. . . . . 6
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
6 | 2, 5 | ax-mp 5 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
7 | 6 | eqcomi 2631 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
8 | | cnelprrecn 10029 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
9 | 8 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
10 | | logcn.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
11 | 10 | logdmopn 24395 |
. . . . 5
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
13 | | logf1o 24311 |
. . . . . . . . 9
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
14 | | f1of1 6136 |
. . . . . . . . 9
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})–1-1→ran log) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . 8
⊢
log:(ℂ ∖ {0})–1-1→ran log |
16 | 10 | logdmss 24388 |
. . . . . . . 8
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
17 | | f1ores 6151 |
. . . . . . . 8
⊢
((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷)) |
18 | 15, 16, 17 | mp2an 708 |
. . . . . . 7
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) |
19 | | f1ocnv 6149 |
. . . . . . 7
⊢ ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) → ◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
⊢ ◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 |
21 | | df-log 24303 |
. . . . . . . . . . 11
⊢ log =
◡(exp ↾ (◡ℑ “
(-π(,]π))) |
22 | 21 | reseq1i 5392 |
. . . . . . . . . 10
⊢ (log
↾ 𝐷) = (◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) |
23 | 22 | cnveqi 5297 |
. . . . . . . . 9
⊢ ◡(log ↾ 𝐷) = ◡(◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) |
24 | | eff 14812 |
. . . . . . . . . . 11
⊢
exp:ℂ⟶ℂ |
25 | | cnvimass 5485 |
. . . . . . . . . . . 12
⊢ (◡ℑ “ (-π(,]π)) ⊆ dom
ℑ |
26 | | imf 13853 |
. . . . . . . . . . . . 13
⊢
ℑ:ℂ⟶ℝ |
27 | 26 | fdmi 6052 |
. . . . . . . . . . . 12
⊢ dom
ℑ = ℂ |
28 | 25, 27 | sseqtri 3637 |
. . . . . . . . . . 11
⊢ (◡ℑ “ (-π(,]π)) ⊆
ℂ |
29 | | fssres 6070 |
. . . . . . . . . . 11
⊢
((exp:ℂ⟶ℂ ∧ (◡ℑ “ (-π(,]π)) ⊆
ℂ) → (exp ↾ (◡ℑ
“ (-π(,]π))):(◡ℑ
“ (-π(,]π))⟶ℂ) |
30 | 24, 28, 29 | mp2an 708 |
. . . . . . . . . 10
⊢ (exp
↾ (◡ℑ “
(-π(,]π))):(◡ℑ “
(-π(,]π))⟶ℂ |
31 | | ffun 6048 |
. . . . . . . . . 10
⊢ ((exp
↾ (◡ℑ “
(-π(,]π))):(◡ℑ “
(-π(,]π))⟶ℂ → Fun (exp ↾ (◡ℑ “
(-π(,]π)))) |
32 | | funcnvres2 5969 |
. . . . . . . . . 10
⊢ (Fun (exp
↾ (◡ℑ “
(-π(,]π))) → ◡(◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) = ((exp ↾ (◡ℑ “ (-π(,]π))) ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷))) |
33 | 30, 31, 32 | mp2b 10 |
. . . . . . . . 9
⊢ ◡(◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) = ((exp ↾ (◡ℑ “ (-π(,]π))) ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
34 | | cnvimass 5485 |
. . . . . . . . . . 11
⊢ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) ⊆ dom (exp ↾
(◡ℑ “
(-π(,]π))) |
35 | 30 | fdmi 6052 |
. . . . . . . . . . 11
⊢ dom (exp
↾ (◡ℑ “
(-π(,]π))) = (◡ℑ “
(-π(,]π)) |
36 | 34, 35 | sseqtri 3637 |
. . . . . . . . . 10
⊢ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) ⊆ (◡ℑ “
(-π(,]π)) |
37 | | resabs1 5427 |
. . . . . . . . . 10
⊢ ((◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) ⊆ (◡ℑ “ (-π(,]π)) → ((exp
↾ (◡ℑ “
(-π(,]π))) ↾ (◡(exp ↾
(◡ℑ “ (-π(,]π)))
“ 𝐷)) = (exp ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷))) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢ ((exp
↾ (◡ℑ “
(-π(,]π))) ↾ (◡(exp ↾
(◡ℑ “ (-π(,]π)))
“ 𝐷)) = (exp ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
39 | 23, 33, 38 | 3eqtri 2648 |
. . . . . . . 8
⊢ ◡(log ↾ 𝐷) = (exp ↾ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
40 | 21 | imaeq1i 5463 |
. . . . . . . . 9
⊢ (log
“ 𝐷) = (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) |
41 | 40 | reseq2i 5393 |
. . . . . . . 8
⊢ (exp
↾ (log “ 𝐷)) =
(exp ↾ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
42 | 39, 41 | eqtr4i 2647 |
. . . . . . 7
⊢ ◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷)) |
43 | | f1oeq1 6127 |
. . . . . . 7
⊢ (◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷)) → (◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 ↔ (exp ↾ (log
“ 𝐷)):(log “
𝐷)–1-1-onto→𝐷)) |
44 | 42, 43 | ax-mp 5 |
. . . . . 6
⊢ (◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 ↔ (exp ↾ (log
“ 𝐷)):(log “
𝐷)–1-1-onto→𝐷) |
45 | 20, 44 | mpbi 220 |
. . . . 5
⊢ (exp
↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷 |
46 | 45 | a1i 11 |
. . . 4
⊢ (⊤
→ (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷) |
47 | 42 | cnveqi 5297 |
. . . . . 6
⊢ ◡◡(log ↾ 𝐷) = ◡(exp ↾ (log “ 𝐷)) |
48 | | relres 5426 |
. . . . . . 7
⊢ Rel (log
↾ 𝐷) |
49 | | dfrel2 5583 |
. . . . . . 7
⊢ (Rel (log
↾ 𝐷) ↔ ◡◡(log ↾ 𝐷) = (log ↾ 𝐷)) |
50 | 48, 49 | mpbi 220 |
. . . . . 6
⊢ ◡◡(log ↾ 𝐷) = (log ↾ 𝐷) |
51 | 47, 50 | eqtr3i 2646 |
. . . . 5
⊢ ◡(exp ↾ (log “ 𝐷)) = (log ↾ 𝐷) |
52 | | f1of 6137 |
. . . . . . 7
⊢ ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) → (log
↾ 𝐷):𝐷⟶(log “ 𝐷)) |
53 | 18, 52 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (log ↾ 𝐷):𝐷⟶(log “ 𝐷)) |
54 | | imassrn 5477 |
. . . . . . . 8
⊢ (log
“ 𝐷) ⊆ ran
log |
55 | | logrncn 24309 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran log → 𝑥 ∈
ℂ) |
56 | 55 | ssriv 3607 |
. . . . . . . 8
⊢ ran log
⊆ ℂ |
57 | 54, 56 | sstri 3612 |
. . . . . . 7
⊢ (log
“ 𝐷) ⊆
ℂ |
58 | 10 | logcn 24393 |
. . . . . . 7
⊢ (log
↾ 𝐷) ∈ (𝐷–cn→ℂ) |
59 | | cncffvrn 22701 |
. . . . . . 7
⊢ (((log
“ 𝐷) ⊆ ℂ
∧ (log ↾ 𝐷)
∈ (𝐷–cn→ℂ)) → ((log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷))) |
60 | 57, 58, 59 | mp2an 708 |
. . . . . 6
⊢ ((log
↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷)) |
61 | 53, 60 | sylibr 224 |
. . . . 5
⊢ (⊤
→ (log ↾ 𝐷)
∈ (𝐷–cn→(log “ 𝐷))) |
62 | 51, 61 | syl5eqel 2705 |
. . . 4
⊢ (⊤
→ ◡(exp ↾ (log “ 𝐷)) ∈ (𝐷–cn→(log “ 𝐷))) |
63 | | ssid 3624 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
64 | 1, 7 | dvres 23675 |
. . . . . . . . 9
⊢
(((ℂ ⊆ ℂ ∧ exp:ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ (log “ 𝐷) ⊆ ℂ)) → (ℂ D (exp
↾ (log “ 𝐷))) =
((ℂ D exp) ↾
((int‘(TopOpen‘ℂfld))‘(log “ 𝐷)))) |
65 | 63, 24, 63, 57, 64 | mp4an 709 |
. . . . . . . 8
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) = ((ℂ D exp) ↾
((int‘(TopOpen‘ℂfld))‘(log “ 𝐷))) |
66 | | dvef 23743 |
. . . . . . . . 9
⊢ (ℂ
D exp) = exp |
67 | 10 | dvloglem 24394 |
. . . . . . . . . 10
⊢ (log
“ 𝐷) ∈
(TopOpen‘ℂfld) |
68 | | isopn3i 20886 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (log “
𝐷) ∈
(TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘(log “ 𝐷)) = (log “ 𝐷)) |
69 | 2, 67, 68 | mp2an 708 |
. . . . . . . . 9
⊢
((int‘(TopOpen‘ℂfld))‘(log “
𝐷)) = (log “ 𝐷) |
70 | 66, 69 | reseq12i 5394 |
. . . . . . . 8
⊢ ((ℂ
D exp) ↾ ((int‘(TopOpen‘ℂfld))‘(log
“ 𝐷))) = (exp ↾
(log “ 𝐷)) |
71 | 65, 70 | eqtri 2644 |
. . . . . . 7
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) = (exp ↾ (log “ 𝐷)) |
72 | 71 | dmeqi 5325 |
. . . . . 6
⊢ dom
(ℂ D (exp ↾ (log “ 𝐷))) = dom (exp ↾ (log “ 𝐷)) |
73 | | dmres 5419 |
. . . . . 6
⊢ dom (exp
↾ (log “ 𝐷)) =
((log “ 𝐷) ∩ dom
exp) |
74 | 24 | fdmi 6052 |
. . . . . . . 8
⊢ dom exp =
ℂ |
75 | 57, 74 | sseqtr4i 3638 |
. . . . . . 7
⊢ (log
“ 𝐷) ⊆ dom
exp |
76 | | df-ss 3588 |
. . . . . . 7
⊢ ((log
“ 𝐷) ⊆ dom exp
↔ ((log “ 𝐷)
∩ dom exp) = (log “ 𝐷)) |
77 | 75, 76 | mpbi 220 |
. . . . . 6
⊢ ((log
“ 𝐷) ∩ dom exp) =
(log “ 𝐷) |
78 | 72, 73, 77 | 3eqtri 2648 |
. . . . 5
⊢ dom
(ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷) |
79 | 78 | a1i 11 |
. . . 4
⊢ (⊤
→ dom (ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷)) |
80 | | neirr 2803 |
. . . . . 6
⊢ ¬ 0
≠ 0 |
81 | | resss 5422 |
. . . . . . . . . . . . 13
⊢ ((ℂ
D exp) ↾ ((int‘(TopOpen‘ℂfld))‘(log
“ 𝐷))) ⊆
(ℂ D exp) |
82 | 65, 81 | eqsstri 3635 |
. . . . . . . . . . . 12
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) ⊆ (ℂ D exp) |
83 | 82, 66 | sseqtri 3637 |
. . . . . . . . . . 11
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) ⊆ exp |
84 | | rnss 5354 |
. . . . . . . . . . 11
⊢ ((ℂ
D (exp ↾ (log “ 𝐷))) ⊆ exp → ran (ℂ D (exp
↾ (log “ 𝐷)))
⊆ ran exp) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran
(ℂ D (exp ↾ (log “ 𝐷))) ⊆ ran exp |
86 | | eff2 14829 |
. . . . . . . . . . 11
⊢
exp:ℂ⟶(ℂ ∖ {0}) |
87 | | frn 6053 |
. . . . . . . . . . 11
⊢
(exp:ℂ⟶(ℂ ∖ {0}) → ran exp ⊆
(ℂ ∖ {0})) |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran exp
⊆ (ℂ ∖ {0}) |
89 | 85, 88 | sstri 3612 |
. . . . . . . . 9
⊢ ran
(ℂ D (exp ↾ (log “ 𝐷))) ⊆ (ℂ ∖
{0}) |
90 | 89 | sseli 3599 |
. . . . . . . 8
⊢ (0 ∈
ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ∈ (ℂ ∖
{0})) |
91 | | eldifsn 4317 |
. . . . . . . 8
⊢ (0 ∈
(ℂ ∖ {0}) ↔ (0 ∈ ℂ ∧ 0 ≠
0)) |
92 | 90, 91 | sylib 208 |
. . . . . . 7
⊢ (0 ∈
ran (ℂ D (exp ↾ (log “ 𝐷))) → (0 ∈ ℂ ∧ 0 ≠
0)) |
93 | 92 | simprd 479 |
. . . . . 6
⊢ (0 ∈
ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ≠ 0) |
94 | 80, 93 | mto 188 |
. . . . 5
⊢ ¬ 0
∈ ran (ℂ D (exp ↾ (log “ 𝐷))) |
95 | 94 | a1i 11 |
. . . 4
⊢ (⊤
→ ¬ 0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷)))) |
96 | 1, 7, 9, 12, 46, 62, 79, 95 | dvcnv 23740 |
. . 3
⊢ (⊤
→ (ℂ D ◡(exp ↾ (log
“ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥))))) |
97 | 96 | trud 1493 |
. 2
⊢ (ℂ
D ◡(exp ↾ (log “ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)))) |
98 | 51 | oveq2i 6661 |
. 2
⊢ (ℂ
D ◡(exp ↾ (log “ 𝐷))) = (ℂ D (log ↾
𝐷)) |
99 | 71 | fveq1i 6192 |
. . . . 5
⊢ ((ℂ
D (exp ↾ (log “ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = ((exp ↾ (log “ 𝐷))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) |
100 | | f1ocnvfv2 6533 |
. . . . . 6
⊢ (((exp
↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷 ∧ 𝑥 ∈ 𝐷) → ((exp ↾ (log “ 𝐷))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥) |
101 | 45, 100 | mpan 706 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((exp ↾ (log “ 𝐷))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥) |
102 | 99, 101 | syl5eq 2668 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥) |
103 | 102 | oveq2d 6666 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥))) = (1 / 𝑥)) |
104 | 103 | mpteq2ia 4740 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
105 | 97, 98, 104 | 3eqtr3i 2652 |
1
⊢ (ℂ
D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |