Step | Hyp | Ref
| Expression |
1 | | logf1o 26073 |
. . . . . . 7
β’
log:(β β {0})β1-1-ontoβran
log |
2 | | f1of 6834 |
. . . . . . 7
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})βΆran log) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’
log:(β β {0})βΆran log |
4 | | logcn.d |
. . . . . . 7
β’ π· = (β β
(-β(,]0)) |
5 | 4 | logdmss 26150 |
. . . . . 6
β’ π· β (β β
{0}) |
6 | | fssres 6758 |
. . . . . 6
β’
((log:(β β {0})βΆran log β§ π· β (β β {0})) β (log
βΎ π·):π·βΆran
log) |
7 | 3, 5, 6 | mp2an 691 |
. . . . 5
β’ (log
βΎ π·):π·βΆran log |
8 | | ffn 6718 |
. . . . 5
β’ ((log
βΎ π·):π·βΆran log β (log
βΎ π·) Fn π·) |
9 | 7, 8 | ax-mp 5 |
. . . 4
β’ (log
βΎ π·) Fn π· |
10 | | dffn5 6951 |
. . . 4
β’ ((log
βΎ π·) Fn π· β (log βΎ π·) = (π₯ β π· β¦ ((log βΎ π·)βπ₯))) |
11 | 9, 10 | mpbi 229 |
. . 3
β’ (log
βΎ π·) = (π₯ β π· β¦ ((log βΎ π·)βπ₯)) |
12 | | fvres 6911 |
. . . . 5
β’ (π₯ β π· β ((log βΎ π·)βπ₯) = (logβπ₯)) |
13 | 4 | ellogdm 26147 |
. . . . . . . 8
β’ (π₯ β π· β (π₯ β β β§ (π₯ β β β π₯ β
β+))) |
14 | 13 | simplbi 499 |
. . . . . . 7
β’ (π₯ β π· β π₯ β β) |
15 | 4 | logdmn0 26148 |
. . . . . . 7
β’ (π₯ β π· β π₯ β 0) |
16 | 14, 15 | logcld 26079 |
. . . . . 6
β’ (π₯ β π· β (logβπ₯) β β) |
17 | 16 | replimd 15144 |
. . . . 5
β’ (π₯ β π· β (logβπ₯) = ((ββ(logβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
18 | | relog 26105 |
. . . . . . . 8
β’ ((π₯ β β β§ π₯ β 0) β
(ββ(logβπ₯)) = (logβ(absβπ₯))) |
19 | 14, 15, 18 | syl2anc 585 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) = (logβ(absβπ₯))) |
20 | 14, 15 | absrpcld 15395 |
. . . . . . . 8
β’ (π₯ β π· β (absβπ₯) β
β+) |
21 | 20 | fvresd 6912 |
. . . . . . 7
β’ (π₯ β π· β ((log βΎ
β+)β(absβπ₯)) = (logβ(absβπ₯))) |
22 | 19, 21 | eqtr4d 2776 |
. . . . . 6
β’ (π₯ β π· β (ββ(logβπ₯)) = ((log βΎ
β+)β(absβπ₯))) |
23 | 22 | oveq1d 7424 |
. . . . 5
β’ (π₯ β π· β ((ββ(logβπ₯)) + (i Β·
(ββ(logβπ₯)))) = (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
24 | 12, 17, 23 | 3eqtrd 2777 |
. . . 4
β’ (π₯ β π· β ((log βΎ π·)βπ₯) = (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
25 | 24 | mpteq2ia 5252 |
. . 3
β’ (π₯ β π· β¦ ((log βΎ π·)βπ₯)) = (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
26 | 11, 25 | eqtri 2761 |
. 2
β’ (log
βΎ π·) = (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
27 | | eqid 2733 |
. . . 4
β’
(TopOpenββfld) =
(TopOpenββfld) |
28 | 27 | addcn 24381 |
. . . . 5
β’ + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
29 | 28 | a1i 11 |
. . . 4
β’ (β€
β + β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
30 | 27 | cnfldtopon 24299 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
31 | 14 | ssriv 3987 |
. . . . . . . 8
β’ π· β
β |
32 | | resttopon 22665 |
. . . . . . . 8
β’
(((TopOpenββfld) β (TopOnββ)
β§ π· β β)
β ((TopOpenββfld) βΎt π·) β (TopOnβπ·)) |
33 | 30, 31, 32 | mp2an 691 |
. . . . . . 7
β’
((TopOpenββfld) βΎt π·) β (TopOnβπ·) |
34 | 33 | a1i 11 |
. . . . . 6
β’ (β€
β ((TopOpenββfld) βΎt π·) β (TopOnβπ·)) |
35 | | absf 15284 |
. . . . . . . . . . . 12
β’
abs:ββΆβ |
36 | | fssres 6758 |
. . . . . . . . . . . 12
β’
((abs:ββΆβ β§ π· β β) β (abs βΎ π·):π·βΆβ) |
37 | 35, 31, 36 | mp2an 691 |
. . . . . . . . . . 11
β’ (abs
βΎ π·):π·βΆβ |
38 | 37 | a1i 11 |
. . . . . . . . . 10
β’ (β€
β (abs βΎ π·):π·βΆβ) |
39 | 38 | feqmptd 6961 |
. . . . . . . . 9
β’ (β€
β (abs βΎ π·) =
(π₯ β π· β¦ ((abs βΎ π·)βπ₯))) |
40 | | fvres 6911 |
. . . . . . . . . 10
β’ (π₯ β π· β ((abs βΎ π·)βπ₯) = (absβπ₯)) |
41 | 40 | mpteq2ia 5252 |
. . . . . . . . 9
β’ (π₯ β π· β¦ ((abs βΎ π·)βπ₯)) = (π₯ β π· β¦ (absβπ₯)) |
42 | 39, 41 | eqtrdi 2789 |
. . . . . . . 8
β’ (β€
β (abs βΎ π·) =
(π₯ β π· β¦ (absβπ₯))) |
43 | | ffn 6718 |
. . . . . . . . . . 11
β’ ((abs
βΎ π·):π·βΆβ β (abs
βΎ π·) Fn π·) |
44 | 37, 43 | ax-mp 5 |
. . . . . . . . . 10
β’ (abs
βΎ π·) Fn π· |
45 | 40, 20 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π₯ β π· β ((abs βΎ π·)βπ₯) β
β+) |
46 | 45 | rgen 3064 |
. . . . . . . . . 10
β’
βπ₯ β
π· ((abs βΎ π·)βπ₯) β β+ |
47 | | ffnfv 7118 |
. . . . . . . . . 10
β’ ((abs
βΎ π·):π·βΆβ+
β ((abs βΎ π·) Fn
π· β§ βπ₯ β π· ((abs βΎ π·)βπ₯) β
β+)) |
48 | 44, 46, 47 | mpbir2an 710 |
. . . . . . . . 9
β’ (abs
βΎ π·):π·βΆβ+ |
49 | | rpssre 12981 |
. . . . . . . . . . 11
β’
β+ β β |
50 | | ax-resscn 11167 |
. . . . . . . . . . 11
β’ β
β β |
51 | 49, 50 | sstri 3992 |
. . . . . . . . . 10
β’
β+ β β |
52 | | abscncf 24417 |
. . . . . . . . . . 11
β’ abs
β (ββcnββ) |
53 | | rescncf 24413 |
. . . . . . . . . . 11
β’ (π· β β β (abs
β (ββcnββ)
β (abs βΎ π·)
β (π·βcnββ))) |
54 | 31, 52, 53 | mp2 9 |
. . . . . . . . . 10
β’ (abs
βΎ π·) β (π·βcnββ) |
55 | | cncfcdm 24414 |
. . . . . . . . . 10
β’
((β+ β β β§ (abs βΎ π·) β (π·βcnββ)) β ((abs βΎ π·) β (π·βcnββ+) β (abs βΎ π·):π·βΆβ+)) |
56 | 51, 54, 55 | mp2an 691 |
. . . . . . . . 9
β’ ((abs
βΎ π·) β (π·βcnββ+) β (abs βΎ π·):π·βΆβ+) |
57 | 48, 56 | mpbir 230 |
. . . . . . . 8
β’ (abs
βΎ π·) β (π·βcnββ+) |
58 | 42, 57 | eqeltrrdi 2843 |
. . . . . . 7
β’ (β€
β (π₯ β π· β¦ (absβπ₯)) β (π·βcnββ+)) |
59 | | eqid 2733 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt π·) =
((TopOpenββfld) βΎt π·) |
60 | | eqid 2733 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt
β+) = ((TopOpenββfld)
βΎt β+) |
61 | 27, 59, 60 | cncfcn 24426 |
. . . . . . . 8
β’ ((π· β β β§
β+ β β) β (π·βcnββ+) =
(((TopOpenββfld) βΎt π·) Cn ((TopOpenββfld)
βΎt β+))) |
62 | 31, 51, 61 | mp2an 691 |
. . . . . . 7
β’ (π·βcnββ+) =
(((TopOpenββfld) βΎt π·) Cn ((TopOpenββfld)
βΎt β+)) |
63 | 58, 62 | eleqtrdi 2844 |
. . . . . 6
β’ (β€
β (π₯ β π· β¦ (absβπ₯)) β
(((TopOpenββfld) βΎt π·) Cn ((TopOpenββfld)
βΎt β+))) |
64 | | ssid 4005 |
. . . . . . . . . 10
β’ β
β β |
65 | | cncfss 24415 |
. . . . . . . . . 10
β’ ((β
β β β§ β β β) β
(β+βcnββ) β
(β+βcnββ)) |
66 | 50, 64, 65 | mp2an 691 |
. . . . . . . . 9
β’
(β+βcnββ) β
(β+βcnββ) |
67 | | relogcn 26146 |
. . . . . . . . 9
β’ (log
βΎ β+) β (β+βcnββ) |
68 | 66, 67 | sselii 3980 |
. . . . . . . 8
β’ (log
βΎ β+) β (β+βcnββ) |
69 | 68 | a1i 11 |
. . . . . . 7
β’ (β€
β (log βΎ β+) β
(β+βcnββ)) |
70 | 30 | toponrestid 22423 |
. . . . . . . . 9
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
71 | 27, 60, 70 | cncfcn 24426 |
. . . . . . . 8
β’
((β+ β β β§ β β β)
β (β+βcnββ) =
(((TopOpenββfld) βΎt
β+) Cn
(TopOpenββfld))) |
72 | 51, 64, 71 | mp2an 691 |
. . . . . . 7
β’
(β+βcnββ) =
(((TopOpenββfld) βΎt
β+) Cn (TopOpenββfld)) |
73 | 69, 72 | eleqtrdi 2844 |
. . . . . 6
β’ (β€
β (log βΎ β+) β
(((TopOpenββfld) βΎt
β+) Cn
(TopOpenββfld))) |
74 | 34, 63, 73 | cnmpt11f 23168 |
. . . . 5
β’ (β€
β (π₯ β π· β¦ ((log βΎ
β+)β(absβπ₯))) β
(((TopOpenββfld) βΎt π·) Cn
(TopOpenββfld))) |
75 | 27, 59, 70 | cncfcn 24426 |
. . . . . 6
β’ ((π· β β β§ β
β β) β (π·βcnββ) =
(((TopOpenββfld) βΎt π·) Cn
(TopOpenββfld))) |
76 | 31, 64, 75 | mp2an 691 |
. . . . 5
β’ (π·βcnββ) =
(((TopOpenββfld) βΎt π·) Cn
(TopOpenββfld)) |
77 | 74, 76 | eleqtrrdi 2845 |
. . . 4
β’ (β€
β (π₯ β π· β¦ ((log βΎ
β+)β(absβπ₯))) β (π·βcnββ)) |
78 | 16 | imcld 15142 |
. . . . . . . 8
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
79 | 78 | recnd 11242 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
80 | 79 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β π·) β
(ββ(logβπ₯)) β β) |
81 | | eqidd 2734 |
. . . . . 6
β’ (β€
β (π₯ β π· β¦
(ββ(logβπ₯))) = (π₯ β π· β¦ (ββ(logβπ₯)))) |
82 | | eqidd 2734 |
. . . . . 6
β’ (β€
β (π¦ β β
β¦ (i Β· π¦)) =
(π¦ β β β¦
(i Β· π¦))) |
83 | | oveq2 7417 |
. . . . . 6
β’ (π¦ =
(ββ(logβπ₯)) β (i Β· π¦) = (i Β·
(ββ(logβπ₯)))) |
84 | 80, 81, 82, 83 | fmptco 7127 |
. . . . 5
β’ (β€
β ((π¦ β β
β¦ (i Β· π¦))
β (π₯ β π· β¦
(ββ(logβπ₯)))) = (π₯ β π· β¦ (i Β·
(ββ(logβπ₯))))) |
85 | | cncfss 24415 |
. . . . . . . . 9
β’ ((β
β β β§ β β β) β (π·βcnββ) β (π·βcnββ)) |
86 | 50, 64, 85 | mp2an 691 |
. . . . . . . 8
β’ (π·βcnββ) β (π·βcnββ) |
87 | 4 | logcnlem5 26154 |
. . . . . . . 8
β’ (π₯ β π· β¦ (ββ(logβπ₯))) β (π·βcnββ) |
88 | 86, 87 | sselii 3980 |
. . . . . . 7
β’ (π₯ β π· β¦ (ββ(logβπ₯))) β (π·βcnββ) |
89 | 88 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β π· β¦
(ββ(logβπ₯))) β (π·βcnββ)) |
90 | | ax-icn 11169 |
. . . . . . 7
β’ i β
β |
91 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β β β¦ (i
Β· π¦)) = (π¦ β β β¦ (i
Β· π¦)) |
92 | 91 | mulc1cncf 24421 |
. . . . . . 7
β’ (i β
β β (π¦ β
β β¦ (i Β· π¦)) β (ββcnββ)) |
93 | 90, 92 | mp1i 13 |
. . . . . 6
β’ (β€
β (π¦ β β
β¦ (i Β· π¦))
β (ββcnββ)) |
94 | 89, 93 | cncfco 24423 |
. . . . 5
β’ (β€
β ((π¦ β β
β¦ (i Β· π¦))
β (π₯ β π· β¦
(ββ(logβπ₯)))) β (π·βcnββ)) |
95 | 84, 94 | eqeltrrd 2835 |
. . . 4
β’ (β€
β (π₯ β π· β¦ (i Β·
(ββ(logβπ₯)))) β (π·βcnββ)) |
96 | 27, 29, 77, 95 | cncfmpt2f 24431 |
. . 3
β’ (β€
β (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) β (π·βcnββ)) |
97 | 96 | mptru 1549 |
. 2
β’ (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) β (π·βcnββ) |
98 | 26, 97 | eqeltri 2830 |
1
β’ (log
βΎ π·) β (π·βcnββ) |