Step | Hyp | Ref
| Expression |
1 | | logf1o 26072 |
. . . . . . 7
β’
log:(β β {0})β1-1-ontoβran
log |
2 | | f1of 6833 |
. . . . . . 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 26149 |
. . . . . 6
β’ π· β (β β
{0}) |
6 | | fssres 6757 |
. . . . . 6
β’
((log:(β β {0})βΆran log β§ π· β (β β {0})) β (log
βΎ π·):π·βΆran
log) |
7 | 3, 5, 6 | mp2an 690 |
. . . . 5
β’ (log
βΎ π·):π·βΆran log |
8 | | ffn 6717 |
. . . . 5
β’ ((log
βΎ π·):π·βΆran log β (log
βΎ π·) Fn π·) |
9 | 7, 8 | ax-mp 5 |
. . . 4
β’ (log
βΎ π·) Fn π· |
10 | | dffn5 6950 |
. . . 4
β’ ((log
βΎ π·) Fn π· β (log βΎ π·) = (π₯ β π· β¦ ((log βΎ π·)βπ₯))) |
11 | 9, 10 | mpbi 229 |
. . 3
β’ (log
βΎ π·) = (π₯ β π· β¦ ((log βΎ π·)βπ₯)) |
12 | | fvres 6910 |
. . . . 5
β’ (π₯ β π· β ((log βΎ π·)βπ₯) = (logβπ₯)) |
13 | 4 | ellogdm 26146 |
. . . . . . . 8
β’ (π₯ β π· β (π₯ β β β§ (π₯ β β β π₯ β
β+))) |
14 | 13 | simplbi 498 |
. . . . . . 7
β’ (π₯ β π· β π₯ β β) |
15 | 4 | logdmn0 26147 |
. . . . . . 7
β’ (π₯ β π· β π₯ β 0) |
16 | 14, 15 | logcld 26078 |
. . . . . 6
β’ (π₯ β π· β (logβπ₯) β β) |
17 | 16 | replimd 15143 |
. . . . 5
β’ (π₯ β π· β (logβπ₯) = ((ββ(logβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
18 | | relog 26104 |
. . . . . . . 8
β’ ((π₯ β β β§ π₯ β 0) β
(ββ(logβπ₯)) = (logβ(absβπ₯))) |
19 | 14, 15, 18 | syl2anc 584 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) = (logβ(absβπ₯))) |
20 | 14, 15 | absrpcld 15394 |
. . . . . . . 8
β’ (π₯ β π· β (absβπ₯) β
β+) |
21 | 20 | fvresd 6911 |
. . . . . . 7
β’ (π₯ β π· β ((log βΎ
β+)β(absβπ₯)) = (logβ(absβπ₯))) |
22 | 19, 21 | eqtr4d 2775 |
. . . . . 6
β’ (π₯ β π· β (ββ(logβπ₯)) = ((log βΎ
β+)β(absβπ₯))) |
23 | 22 | oveq1d 7423 |
. . . . 5
β’ (π₯ β π· β ((ββ(logβπ₯)) + (i Β·
(ββ(logβπ₯)))) = (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
24 | 12, 17, 23 | 3eqtrd 2776 |
. . . 4
β’ (π₯ β π· β ((log βΎ π·)βπ₯) = (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
25 | 24 | mpteq2ia 5251 |
. . 3
β’ (π₯ β π· β¦ ((log βΎ π·)βπ₯)) = (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
26 | 11, 25 | eqtri 2760 |
. 2
β’ (log
βΎ π·) = (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) |
27 | | eqid 2732 |
. . . 4
β’
(TopOpenββfld) =
(TopOpenββfld) |
28 | 27 | addcn 24380 |
. . . . 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 24298 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
31 | 14 | ssriv 3986 |
. . . . . . . 8
β’ π· β
β |
32 | | resttopon 22664 |
. . . . . . . 8
β’
(((TopOpenββfld) β (TopOnββ)
β§ π· β β)
β ((TopOpenββfld) βΎt π·) β (TopOnβπ·)) |
33 | 30, 31, 32 | mp2an 690 |
. . . . . . 7
β’
((TopOpenββfld) βΎt π·) β (TopOnβπ·) |
34 | 33 | a1i 11 |
. . . . . 6
β’ (β€
β ((TopOpenββfld) βΎt π·) β (TopOnβπ·)) |
35 | | absf 15283 |
. . . . . . . . . . . 12
β’
abs:ββΆβ |
36 | | fssres 6757 |
. . . . . . . . . . . 12
β’
((abs:ββΆβ β§ π· β β) β (abs βΎ π·):π·βΆβ) |
37 | 35, 31, 36 | mp2an 690 |
. . . . . . . . . . 11
β’ (abs
βΎ π·):π·βΆβ |
38 | 37 | a1i 11 |
. . . . . . . . . 10
β’ (β€
β (abs βΎ π·):π·βΆβ) |
39 | 38 | feqmptd 6960 |
. . . . . . . . 9
β’ (β€
β (abs βΎ π·) =
(π₯ β π· β¦ ((abs βΎ π·)βπ₯))) |
40 | | fvres 6910 |
. . . . . . . . . 10
β’ (π₯ β π· β ((abs βΎ π·)βπ₯) = (absβπ₯)) |
41 | 40 | mpteq2ia 5251 |
. . . . . . . . 9
β’ (π₯ β π· β¦ ((abs βΎ π·)βπ₯)) = (π₯ β π· β¦ (absβπ₯)) |
42 | 39, 41 | eqtrdi 2788 |
. . . . . . . 8
β’ (β€
β (abs βΎ π·) =
(π₯ β π· β¦ (absβπ₯))) |
43 | | ffn 6717 |
. . . . . . . . . . 11
β’ ((abs
βΎ π·):π·βΆβ β (abs
βΎ π·) Fn π·) |
44 | 37, 43 | ax-mp 5 |
. . . . . . . . . 10
β’ (abs
βΎ π·) Fn π· |
45 | 40, 20 | eqeltrd 2833 |
. . . . . . . . . . 11
β’ (π₯ β π· β ((abs βΎ π·)βπ₯) β
β+) |
46 | 45 | rgen 3063 |
. . . . . . . . . 10
β’
βπ₯ β
π· ((abs βΎ π·)βπ₯) β β+ |
47 | | ffnfv 7117 |
. . . . . . . . . 10
β’ ((abs
βΎ π·):π·βΆβ+
β ((abs βΎ π·) Fn
π· β§ βπ₯ β π· ((abs βΎ π·)βπ₯) β
β+)) |
48 | 44, 46, 47 | mpbir2an 709 |
. . . . . . . . 9
β’ (abs
βΎ π·):π·βΆβ+ |
49 | | rpssre 12980 |
. . . . . . . . . . 11
β’
β+ β β |
50 | | ax-resscn 11166 |
. . . . . . . . . . 11
β’ β
β β |
51 | 49, 50 | sstri 3991 |
. . . . . . . . . 10
β’
β+ β β |
52 | | abscncf 24416 |
. . . . . . . . . . 11
β’ abs
β (ββcnββ) |
53 | | rescncf 24412 |
. . . . . . . . . . 11
β’ (π· β β β (abs
β (ββcnββ)
β (abs βΎ π·)
β (π·βcnββ))) |
54 | 31, 52, 53 | mp2 9 |
. . . . . . . . . 10
β’ (abs
βΎ π·) β (π·βcnββ) |
55 | | cncfcdm 24413 |
. . . . . . . . . 10
β’
((β+ β β β§ (abs βΎ π·) β (π·βcnββ)) β ((abs βΎ π·) β (π·βcnββ+) β (abs βΎ π·):π·βΆβ+)) |
56 | 51, 54, 55 | mp2an 690 |
. . . . . . . . 9
β’ ((abs
βΎ π·) β (π·βcnββ+) β (abs βΎ π·):π·βΆβ+) |
57 | 48, 56 | mpbir 230 |
. . . . . . . 8
β’ (abs
βΎ π·) β (π·βcnββ+) |
58 | 42, 57 | eqeltrrdi 2842 |
. . . . . . 7
β’ (β€
β (π₯ β π· β¦ (absβπ₯)) β (π·βcnββ+)) |
59 | | eqid 2732 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt π·) =
((TopOpenββfld) βΎt π·) |
60 | | eqid 2732 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt
β+) = ((TopOpenββfld)
βΎt β+) |
61 | 27, 59, 60 | cncfcn 24425 |
. . . . . . . 8
β’ ((π· β β β§
β+ β β) β (π·βcnββ+) =
(((TopOpenββfld) βΎt π·) Cn ((TopOpenββfld)
βΎt β+))) |
62 | 31, 51, 61 | mp2an 690 |
. . . . . . 7
β’ (π·βcnββ+) =
(((TopOpenββfld) βΎt π·) Cn ((TopOpenββfld)
βΎt β+)) |
63 | 58, 62 | eleqtrdi 2843 |
. . . . . 6
β’ (β€
β (π₯ β π· β¦ (absβπ₯)) β
(((TopOpenββfld) βΎt π·) Cn ((TopOpenββfld)
βΎt β+))) |
64 | | ssid 4004 |
. . . . . . . . . 10
β’ β
β β |
65 | | cncfss 24414 |
. . . . . . . . . 10
β’ ((β
β β β§ β β β) β
(β+βcnββ) β
(β+βcnββ)) |
66 | 50, 64, 65 | mp2an 690 |
. . . . . . . . 9
β’
(β+βcnββ) β
(β+βcnββ) |
67 | | relogcn 26145 |
. . . . . . . . 9
β’ (log
βΎ β+) β (β+βcnββ) |
68 | 66, 67 | sselii 3979 |
. . . . . . . 8
β’ (log
βΎ β+) β (β+βcnββ) |
69 | 68 | a1i 11 |
. . . . . . 7
β’ (β€
β (log βΎ β+) β
(β+βcnββ)) |
70 | 30 | toponrestid 22422 |
. . . . . . . . 9
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
71 | 27, 60, 70 | cncfcn 24425 |
. . . . . . . 8
β’
((β+ β β β§ β β β)
β (β+βcnββ) =
(((TopOpenββfld) βΎt
β+) Cn
(TopOpenββfld))) |
72 | 51, 64, 71 | mp2an 690 |
. . . . . . 7
β’
(β+βcnββ) =
(((TopOpenββfld) βΎt
β+) Cn (TopOpenββfld)) |
73 | 69, 72 | eleqtrdi 2843 |
. . . . . 6
β’ (β€
β (log βΎ β+) β
(((TopOpenββfld) βΎt
β+) Cn
(TopOpenββfld))) |
74 | 34, 63, 73 | cnmpt11f 23167 |
. . . . 5
β’ (β€
β (π₯ β π· β¦ ((log βΎ
β+)β(absβπ₯))) β
(((TopOpenββfld) βΎt π·) Cn
(TopOpenββfld))) |
75 | 27, 59, 70 | cncfcn 24425 |
. . . . . 6
β’ ((π· β β β§ β
β β) β (π·βcnββ) =
(((TopOpenββfld) βΎt π·) Cn
(TopOpenββfld))) |
76 | 31, 64, 75 | mp2an 690 |
. . . . 5
β’ (π·βcnββ) =
(((TopOpenββfld) βΎt π·) Cn
(TopOpenββfld)) |
77 | 74, 76 | eleqtrrdi 2844 |
. . . 4
β’ (β€
β (π₯ β π· β¦ ((log βΎ
β+)β(absβπ₯))) β (π·βcnββ)) |
78 | 16 | imcld 15141 |
. . . . . . . 8
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
79 | 78 | recnd 11241 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
80 | 79 | adantl 482 |
. . . . . 6
β’
((β€ β§ π₯
β π·) β
(ββ(logβπ₯)) β β) |
81 | | eqidd 2733 |
. . . . . 6
β’ (β€
β (π₯ β π· β¦
(ββ(logβπ₯))) = (π₯ β π· β¦ (ββ(logβπ₯)))) |
82 | | eqidd 2733 |
. . . . . 6
β’ (β€
β (π¦ β β
β¦ (i Β· π¦)) =
(π¦ β β β¦
(i Β· π¦))) |
83 | | oveq2 7416 |
. . . . . 6
β’ (π¦ =
(ββ(logβπ₯)) β (i Β· π¦) = (i Β·
(ββ(logβπ₯)))) |
84 | 80, 81, 82, 83 | fmptco 7126 |
. . . . 5
β’ (β€
β ((π¦ β β
β¦ (i Β· π¦))
β (π₯ β π· β¦
(ββ(logβπ₯)))) = (π₯ β π· β¦ (i Β·
(ββ(logβπ₯))))) |
85 | | cncfss 24414 |
. . . . . . . . 9
β’ ((β
β β β§ β β β) β (π·βcnββ) β (π·βcnββ)) |
86 | 50, 64, 85 | mp2an 690 |
. . . . . . . 8
β’ (π·βcnββ) β (π·βcnββ) |
87 | 4 | logcnlem5 26153 |
. . . . . . . 8
β’ (π₯ β π· β¦ (ββ(logβπ₯))) β (π·βcnββ) |
88 | 86, 87 | sselii 3979 |
. . . . . . 7
β’ (π₯ β π· β¦ (ββ(logβπ₯))) β (π·βcnββ) |
89 | 88 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β π· β¦
(ββ(logβπ₯))) β (π·βcnββ)) |
90 | | ax-icn 11168 |
. . . . . . 7
β’ i β
β |
91 | | eqid 2732 |
. . . . . . . 8
β’ (π¦ β β β¦ (i
Β· π¦)) = (π¦ β β β¦ (i
Β· π¦)) |
92 | 91 | mulc1cncf 24420 |
. . . . . . 7
β’ (i β
β β (π¦ β
β β¦ (i Β· π¦)) β (ββcnββ)) |
93 | 90, 92 | mp1i 13 |
. . . . . 6
β’ (β€
β (π¦ β β
β¦ (i Β· π¦))
β (ββcnββ)) |
94 | 89, 93 | cncfco 24422 |
. . . . 5
β’ (β€
β ((π¦ β β
β¦ (i Β· π¦))
β (π₯ β π· β¦
(ββ(logβπ₯)))) β (π·βcnββ)) |
95 | 84, 94 | eqeltrrd 2834 |
. . . 4
β’ (β€
β (π₯ β π· β¦ (i Β·
(ββ(logβπ₯)))) β (π·βcnββ)) |
96 | 27, 29, 77, 95 | cncfmpt2f 24430 |
. . 3
β’ (β€
β (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) β (π·βcnββ)) |
97 | 96 | mptru 1548 |
. 2
β’ (π₯ β π· β¦ (((log βΎ
β+)β(absβπ₯)) + (i Β·
(ββ(logβπ₯))))) β (π·βcnββ) |
98 | 26, 97 | eqeltri 2829 |
1
β’ (log
βΎ π·) β (π·βcnββ) |