Proof of Theorem dvlog
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 2 | 1 | cnfldtopon 24803 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 3 | 2 | toponrestid 22927 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 4 | | cnelprrecn 11248 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
| 5 | 4 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 6 | | logcn.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
| 7 | 6 | logdmopn 26691 |
. . . . 5
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
| 8 | 7 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
| 9 | | logf1o 26606 |
. . . . . . . . 9
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
| 10 | | f1of1 6847 |
. . . . . . . . 9
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})–1-1→ran log) |
| 11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
⊢
log:(ℂ ∖ {0})–1-1→ran log |
| 12 | 6 | logdmss 26684 |
. . . . . . . 8
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
| 13 | | f1ores 6862 |
. . . . . . . 8
⊢
((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷)) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . . . . 7
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) |
| 15 | | f1ocnv 6860 |
. . . . . . 7
⊢ ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) → ◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . 6
⊢ ◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 |
| 17 | | df-log 26598 |
. . . . . . . . . . 11
⊢ log =
◡(exp ↾ (◡ℑ “
(-π(,]π))) |
| 18 | 17 | reseq1i 5993 |
. . . . . . . . . 10
⊢ (log
↾ 𝐷) = (◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) |
| 19 | 18 | cnveqi 5885 |
. . . . . . . . 9
⊢ ◡(log ↾ 𝐷) = ◡(◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) |
| 20 | | eff 16117 |
. . . . . . . . . . 11
⊢
exp:ℂ⟶ℂ |
| 21 | | cnvimass 6100 |
. . . . . . . . . . . 12
⊢ (◡ℑ “ (-π(,]π)) ⊆ dom
ℑ |
| 22 | | imf 15152 |
. . . . . . . . . . . . 13
⊢
ℑ:ℂ⟶ℝ |
| 23 | 22 | fdmi 6747 |
. . . . . . . . . . . 12
⊢ dom
ℑ = ℂ |
| 24 | 21, 23 | sseqtri 4032 |
. . . . . . . . . . 11
⊢ (◡ℑ “ (-π(,]π)) ⊆
ℂ |
| 25 | | fssres 6774 |
. . . . . . . . . . 11
⊢
((exp:ℂ⟶ℂ ∧ (◡ℑ “ (-π(,]π)) ⊆
ℂ) → (exp ↾ (◡ℑ
“ (-π(,]π))):(◡ℑ
“ (-π(,]π))⟶ℂ) |
| 26 | 20, 24, 25 | mp2an 692 |
. . . . . . . . . 10
⊢ (exp
↾ (◡ℑ “
(-π(,]π))):(◡ℑ “
(-π(,]π))⟶ℂ |
| 27 | | ffun 6739 |
. . . . . . . . . 10
⊢ ((exp
↾ (◡ℑ “
(-π(,]π))):(◡ℑ “
(-π(,]π))⟶ℂ → Fun (exp ↾ (◡ℑ “
(-π(,]π)))) |
| 28 | | funcnvres2 6646 |
. . . . . . . . . 10
⊢ (Fun (exp
↾ (◡ℑ “
(-π(,]π))) → ◡(◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) = ((exp ↾ (◡ℑ “ (-π(,]π))) ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷))) |
| 29 | 26, 27, 28 | mp2b 10 |
. . . . . . . . 9
⊢ ◡(◡(exp ↾ (◡ℑ “ (-π(,]π))) ↾
𝐷) = ((exp ↾ (◡ℑ “ (-π(,]π))) ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
| 30 | | cnvimass 6100 |
. . . . . . . . . . 11
⊢ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) ⊆ dom (exp ↾
(◡ℑ “
(-π(,]π))) |
| 31 | 26 | fdmi 6747 |
. . . . . . . . . . 11
⊢ dom (exp
↾ (◡ℑ “
(-π(,]π))) = (◡ℑ “
(-π(,]π)) |
| 32 | 30, 31 | sseqtri 4032 |
. . . . . . . . . 10
⊢ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) ⊆ (◡ℑ “
(-π(,]π)) |
| 33 | | resabs1 6024 |
. . . . . . . . . 10
⊢ ((◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) ⊆ (◡ℑ “ (-π(,]π)) → ((exp
↾ (◡ℑ “
(-π(,]π))) ↾ (◡(exp ↾
(◡ℑ “ (-π(,]π)))
“ 𝐷)) = (exp ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷))) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . . 9
⊢ ((exp
↾ (◡ℑ “
(-π(,]π))) ↾ (◡(exp ↾
(◡ℑ “ (-π(,]π)))
“ 𝐷)) = (exp ↾
(◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
| 35 | 19, 29, 34 | 3eqtri 2769 |
. . . . . . . 8
⊢ ◡(log ↾ 𝐷) = (exp ↾ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
| 36 | 17 | imaeq1i 6075 |
. . . . . . . . 9
⊢ (log
“ 𝐷) = (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷) |
| 37 | 36 | reseq2i 5994 |
. . . . . . . 8
⊢ (exp
↾ (log “ 𝐷)) =
(exp ↾ (◡(exp ↾ (◡ℑ “ (-π(,]π))) “
𝐷)) |
| 38 | 35, 37 | eqtr4i 2768 |
. . . . . . 7
⊢ ◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷)) |
| 39 | | f1oeq1 6836 |
. . . . . . 7
⊢ (◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷)) → (◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 ↔ (exp ↾ (log
“ 𝐷)):(log “
𝐷)–1-1-onto→𝐷)) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . 6
⊢ (◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 ↔ (exp ↾ (log
“ 𝐷)):(log “
𝐷)–1-1-onto→𝐷) |
| 41 | 16, 40 | mpbi 230 |
. . . . 5
⊢ (exp
↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷 |
| 42 | 41 | a1i 11 |
. . . 4
⊢ (⊤
→ (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷) |
| 43 | 38 | cnveqi 5885 |
. . . . . 6
⊢ ◡◡(log ↾ 𝐷) = ◡(exp ↾ (log “ 𝐷)) |
| 44 | | relres 6023 |
. . . . . . 7
⊢ Rel (log
↾ 𝐷) |
| 45 | | dfrel2 6209 |
. . . . . . 7
⊢ (Rel (log
↾ 𝐷) ↔ ◡◡(log ↾ 𝐷) = (log ↾ 𝐷)) |
| 46 | 44, 45 | mpbi 230 |
. . . . . 6
⊢ ◡◡(log ↾ 𝐷) = (log ↾ 𝐷) |
| 47 | 43, 46 | eqtr3i 2767 |
. . . . 5
⊢ ◡(exp ↾ (log “ 𝐷)) = (log ↾ 𝐷) |
| 48 | | f1of 6848 |
. . . . . . 7
⊢ ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) → (log
↾ 𝐷):𝐷⟶(log “ 𝐷)) |
| 49 | 14, 48 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (log ↾ 𝐷):𝐷⟶(log “ 𝐷)) |
| 50 | | imassrn 6089 |
. . . . . . . 8
⊢ (log
“ 𝐷) ⊆ ran
log |
| 51 | | logrncn 26604 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran log → 𝑥 ∈
ℂ) |
| 52 | 51 | ssriv 3987 |
. . . . . . . 8
⊢ ran log
⊆ ℂ |
| 53 | 50, 52 | sstri 3993 |
. . . . . . 7
⊢ (log
“ 𝐷) ⊆
ℂ |
| 54 | 6 | logcn 26689 |
. . . . . . 7
⊢ (log
↾ 𝐷) ∈ (𝐷–cn→ℂ) |
| 55 | | cncfcdm 24924 |
. . . . . . 7
⊢ (((log
“ 𝐷) ⊆ ℂ
∧ (log ↾ 𝐷)
∈ (𝐷–cn→ℂ)) → ((log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷))) |
| 56 | 53, 54, 55 | mp2an 692 |
. . . . . 6
⊢ ((log
↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷)) |
| 57 | 49, 56 | sylibr 234 |
. . . . 5
⊢ (⊤
→ (log ↾ 𝐷)
∈ (𝐷–cn→(log “ 𝐷))) |
| 58 | 47, 57 | eqeltrid 2845 |
. . . 4
⊢ (⊤
→ ◡(exp ↾ (log “ 𝐷)) ∈ (𝐷–cn→(log “ 𝐷))) |
| 59 | | ssid 4006 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
| 60 | 1, 3 | dvres 25946 |
. . . . . . . . 9
⊢
(((ℂ ⊆ ℂ ∧ exp:ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ (log “ 𝐷) ⊆ ℂ)) → (ℂ D (exp
↾ (log “ 𝐷))) =
((ℂ D exp) ↾
((int‘(TopOpen‘ℂfld))‘(log “ 𝐷)))) |
| 61 | 59, 20, 59, 53, 60 | mp4an 693 |
. . . . . . . 8
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) = ((ℂ D exp) ↾
((int‘(TopOpen‘ℂfld))‘(log “ 𝐷))) |
| 62 | | dvef 26018 |
. . . . . . . . 9
⊢ (ℂ
D exp) = exp |
| 63 | 1 | cnfldtop 24804 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Top |
| 64 | 6 | dvloglem 26690 |
. . . . . . . . . 10
⊢ (log
“ 𝐷) ∈
(TopOpen‘ℂfld) |
| 65 | | isopn3i 23090 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (log “
𝐷) ∈
(TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘(log “ 𝐷)) = (log “ 𝐷)) |
| 66 | 63, 64, 65 | mp2an 692 |
. . . . . . . . 9
⊢
((int‘(TopOpen‘ℂfld))‘(log “
𝐷)) = (log “ 𝐷) |
| 67 | 62, 66 | reseq12i 5995 |
. . . . . . . 8
⊢ ((ℂ
D exp) ↾ ((int‘(TopOpen‘ℂfld))‘(log
“ 𝐷))) = (exp ↾
(log “ 𝐷)) |
| 68 | 61, 67 | eqtri 2765 |
. . . . . . 7
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) = (exp ↾ (log “ 𝐷)) |
| 69 | 68 | dmeqi 5915 |
. . . . . 6
⊢ dom
(ℂ D (exp ↾ (log “ 𝐷))) = dom (exp ↾ (log “ 𝐷)) |
| 70 | | dmres 6030 |
. . . . . 6
⊢ dom (exp
↾ (log “ 𝐷)) =
((log “ 𝐷) ∩ dom
exp) |
| 71 | 20 | fdmi 6747 |
. . . . . . . 8
⊢ dom exp =
ℂ |
| 72 | 53, 71 | sseqtrri 4033 |
. . . . . . 7
⊢ (log
“ 𝐷) ⊆ dom
exp |
| 73 | | dfss2 3969 |
. . . . . . 7
⊢ ((log
“ 𝐷) ⊆ dom exp
↔ ((log “ 𝐷)
∩ dom exp) = (log “ 𝐷)) |
| 74 | 72, 73 | mpbi 230 |
. . . . . 6
⊢ ((log
“ 𝐷) ∩ dom exp) =
(log “ 𝐷) |
| 75 | 69, 70, 74 | 3eqtri 2769 |
. . . . 5
⊢ dom
(ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷) |
| 76 | 75 | a1i 11 |
. . . 4
⊢ (⊤
→ dom (ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷)) |
| 77 | | neirr 2949 |
. . . . . 6
⊢ ¬ 0
≠ 0 |
| 78 | | resss 6019 |
. . . . . . . . . . . . 13
⊢ ((ℂ
D exp) ↾ ((int‘(TopOpen‘ℂfld))‘(log
“ 𝐷))) ⊆
(ℂ D exp) |
| 79 | 61, 78 | eqsstri 4030 |
. . . . . . . . . . . 12
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) ⊆ (ℂ D exp) |
| 80 | 79, 62 | sseqtri 4032 |
. . . . . . . . . . 11
⊢ (ℂ
D (exp ↾ (log “ 𝐷))) ⊆ exp |
| 81 | 80 | rnssi 5951 |
. . . . . . . . . 10
⊢ ran
(ℂ D (exp ↾ (log “ 𝐷))) ⊆ ran exp |
| 82 | | eff2 16135 |
. . . . . . . . . . 11
⊢
exp:ℂ⟶(ℂ ∖ {0}) |
| 83 | | frn 6743 |
. . . . . . . . . . 11
⊢
(exp:ℂ⟶(ℂ ∖ {0}) → ran exp ⊆
(ℂ ∖ {0})) |
| 84 | 82, 83 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran exp
⊆ (ℂ ∖ {0}) |
| 85 | 81, 84 | sstri 3993 |
. . . . . . . . 9
⊢ ran
(ℂ D (exp ↾ (log “ 𝐷))) ⊆ (ℂ ∖
{0}) |
| 86 | 85 | sseli 3979 |
. . . . . . . 8
⊢ (0 ∈
ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ∈ (ℂ ∖
{0})) |
| 87 | | eldifsn 4786 |
. . . . . . . 8
⊢ (0 ∈
(ℂ ∖ {0}) ↔ (0 ∈ ℂ ∧ 0 ≠
0)) |
| 88 | 86, 87 | sylib 218 |
. . . . . . 7
⊢ (0 ∈
ran (ℂ D (exp ↾ (log “ 𝐷))) → (0 ∈ ℂ ∧ 0 ≠
0)) |
| 89 | 88 | simprd 495 |
. . . . . 6
⊢ (0 ∈
ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ≠ 0) |
| 90 | 77, 89 | mto 197 |
. . . . 5
⊢ ¬ 0
∈ ran (ℂ D (exp ↾ (log “ 𝐷))) |
| 91 | 90 | a1i 11 |
. . . 4
⊢ (⊤
→ ¬ 0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷)))) |
| 92 | 1, 3, 5, 8, 42, 58, 76, 91 | dvcnv 26015 |
. . 3
⊢ (⊤
→ (ℂ D ◡(exp ↾ (log
“ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥))))) |
| 93 | 92 | mptru 1547 |
. 2
⊢ (ℂ
D ◡(exp ↾ (log “ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)))) |
| 94 | 47 | oveq2i 7442 |
. 2
⊢ (ℂ
D ◡(exp ↾ (log “ 𝐷))) = (ℂ D (log ↾
𝐷)) |
| 95 | 68 | fveq1i 6907 |
. . . . 5
⊢ ((ℂ
D (exp ↾ (log “ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = ((exp ↾ (log “ 𝐷))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) |
| 96 | | f1ocnvfv2 7297 |
. . . . . 6
⊢ (((exp
↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷 ∧ 𝑥 ∈ 𝐷) → ((exp ↾ (log “ 𝐷))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥) |
| 97 | 41, 96 | mpan 690 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((exp ↾ (log “ 𝐷))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥) |
| 98 | 95, 97 | eqtrid 2789 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥) |
| 99 | 98 | oveq2d 7447 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥))) = (1 / 𝑥)) |
| 100 | 99 | mpteq2ia 5245 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log
“ 𝐷)))‘(◡(exp ↾ (log “ 𝐷))‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
| 101 | 93, 94, 100 | 3eqtr3i 2773 |
1
⊢ (ℂ
D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |