Step | Hyp | Ref
| Expression |
1 | | logf1o 25943 |
. . . 4
β’
log:(β β {0})β1-1-ontoβran
log |
2 | | f1of1 6787 |
. . . 4
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})β1-1βran log) |
3 | 1, 2 | ax-mp 5 |
. . 3
β’
log:(β β {0})β1-1βran log |
4 | | logcn.d |
. . . 4
β’ π· = (β β
(-β(,]0)) |
5 | 4 | logdmss 26020 |
. . 3
β’ π· β (β β
{0}) |
6 | | f1ores 6802 |
. . 3
β’
((log:(β β {0})β1-1βran log β§ π· β (β β {0})) β (log
βΎ π·):π·β1-1-ontoβ(log
β π·)) |
7 | 3, 5, 6 | mp2an 691 |
. 2
β’ (log
βΎ π·):π·β1-1-ontoβ(log
β π·) |
8 | | f1ofun 6790 |
. . . . . . 7
β’
(log:(β β {0})β1-1-ontoβran
log β Fun log) |
9 | 1, 8 | ax-mp 5 |
. . . . . 6
β’ Fun
log |
10 | | f1of 6788 |
. . . . . . . . 9
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})βΆran log) |
11 | 1, 10 | ax-mp 5 |
. . . . . . . 8
β’
log:(β β {0})βΆran log |
12 | 11 | fdmi 6684 |
. . . . . . 7
β’ dom log =
(β β {0}) |
13 | 5, 12 | sseqtrri 3985 |
. . . . . 6
β’ π· β dom
log |
14 | | funimass4 6911 |
. . . . . 6
β’ ((Fun log
β§ π· β dom log)
β ((log β π·)
β (β‘β β
(-Ο(,)Ο)) β βπ₯ β π· (logβπ₯) β (β‘β β
(-Ο(,)Ο)))) |
15 | 9, 13, 14 | mp2an 691 |
. . . . 5
β’ ((log
β π·) β (β‘β β (-Ο(,)Ο)) β
βπ₯ β π· (logβπ₯) β (β‘β β
(-Ο(,)Ο))) |
16 | 4 | ellogdm 26017 |
. . . . . . . 8
β’ (π₯ β π· β (π₯ β β β§ (π₯ β β β π₯ β
β+))) |
17 | 16 | simplbi 499 |
. . . . . . 7
β’ (π₯ β π· β π₯ β β) |
18 | 4 | logdmn0 26018 |
. . . . . . 7
β’ (π₯ β π· β π₯ β 0) |
19 | 17, 18 | logcld 25949 |
. . . . . 6
β’ (π₯ β π· β (logβπ₯) β β) |
20 | 19 | imcld 15089 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
21 | 17, 18 | logimcld 25950 |
. . . . . . . 8
β’ (π₯ β π· β (-Ο <
(ββ(logβπ₯)) β§ (ββ(logβπ₯)) β€ Ο)) |
22 | 21 | simpld 496 |
. . . . . . 7
β’ (π₯ β π· β -Ο <
(ββ(logβπ₯))) |
23 | | pire 25838 |
. . . . . . . . 9
β’ Ο
β β |
24 | 23 | a1i 11 |
. . . . . . . 8
β’ (π₯ β π· β Ο β
β) |
25 | 21 | simprd 497 |
. . . . . . . 8
β’ (π₯ β π· β (ββ(logβπ₯)) β€ Ο) |
26 | 4 | logdmnrp 26019 |
. . . . . . . . . 10
β’ (π₯ β π· β Β¬ -π₯ β β+) |
27 | | lognegb 25968 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π₯ β 0) β (-π₯ β β+
β (ββ(logβπ₯)) = Ο)) |
28 | 17, 18, 27 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π₯ β π· β (-π₯ β β+ β
(ββ(logβπ₯)) = Ο)) |
29 | 28 | necon3bbid 2978 |
. . . . . . . . . 10
β’ (π₯ β π· β (Β¬ -π₯ β β+ β
(ββ(logβπ₯)) β Ο)) |
30 | 26, 29 | mpbid 231 |
. . . . . . . . 9
β’ (π₯ β π· β (ββ(logβπ₯)) β Ο) |
31 | 30 | necomd 2996 |
. . . . . . . 8
β’ (π₯ β π· β Ο β
(ββ(logβπ₯))) |
32 | 20, 24, 25, 31 | leneltd 11317 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) < Ο) |
33 | 23 | renegcli 11470 |
. . . . . . . . 9
β’ -Ο
β β |
34 | 33 | rexri 11221 |
. . . . . . . 8
β’ -Ο
β β* |
35 | 23 | rexri 11221 |
. . . . . . . 8
β’ Ο
β β* |
36 | | elioo2 13314 |
. . . . . . . 8
β’ ((-Ο
β β* β§ Ο β β*) β
((ββ(logβπ₯)) β (-Ο(,)Ο) β
((ββ(logβπ₯)) β β β§ -Ο <
(ββ(logβπ₯)) β§ (ββ(logβπ₯)) < Ο))) |
37 | 34, 35, 36 | mp2an 691 |
. . . . . . 7
β’
((ββ(logβπ₯)) β (-Ο(,)Ο) β
((ββ(logβπ₯)) β β β§ -Ο <
(ββ(logβπ₯)) β§ (ββ(logβπ₯)) < Ο)) |
38 | 20, 22, 32, 37 | syl3anbrc 1344 |
. . . . . 6
β’ (π₯ β π· β (ββ(logβπ₯)) β
(-Ο(,)Ο)) |
39 | | imf 15007 |
. . . . . . 7
β’
β:ββΆβ |
40 | | ffn 6672 |
. . . . . . 7
β’
(β:ββΆβ β β Fn
β) |
41 | | elpreima 7012 |
. . . . . . 7
β’ (β
Fn β β ((logβπ₯) β (β‘β β (-Ο(,)Ο)) β
((logβπ₯) β
β β§ (ββ(logβπ₯)) β (-Ο(,)Ο)))) |
42 | 39, 40, 41 | mp2b 10 |
. . . . . 6
β’
((logβπ₯)
β (β‘β β
(-Ο(,)Ο)) β ((logβπ₯) β β β§
(ββ(logβπ₯)) β (-Ο(,)Ο))) |
43 | 19, 38, 42 | sylanbrc 584 |
. . . . 5
β’ (π₯ β π· β (logβπ₯) β (β‘β β
(-Ο(,)Ο))) |
44 | 15, 43 | mprgbir 3068 |
. . . 4
β’ (log
β π·) β (β‘β β
(-Ο(,)Ο)) |
45 | | elpreima 7012 |
. . . . . . 7
β’ (β
Fn β β (π₯ β
(β‘β β (-Ο(,)Ο))
β (π₯ β β
β§ (ββπ₯)
β (-Ο(,)Ο)))) |
46 | 39, 40, 45 | mp2b 10 |
. . . . . 6
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο))) |
47 | | simpl 484 |
. . . . . . . . 9
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β π₯
β β) |
48 | | eliooord 13332 |
. . . . . . . . . . 11
β’
((ββπ₯)
β (-Ο(,)Ο) β (-Ο < (ββπ₯) β§ (ββπ₯) < Ο)) |
49 | 48 | adantl 483 |
. . . . . . . . . 10
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (-Ο < (ββπ₯) β§ (ββπ₯) < Ο)) |
50 | 49 | simpld 496 |
. . . . . . . . 9
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β -Ο < (ββπ₯)) |
51 | 49 | simprd 497 |
. . . . . . . . . 10
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (ββπ₯) < Ο) |
52 | | imcl 15005 |
. . . . . . . . . . . 12
β’ (π₯ β β β
(ββπ₯) β
β) |
53 | 52 | adantr 482 |
. . . . . . . . . . 11
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (ββπ₯) β β) |
54 | | ltle 11251 |
. . . . . . . . . . 11
β’
(((ββπ₯)
β β β§ Ο β β) β ((ββπ₯) < Ο β
(ββπ₯) β€
Ο)) |
55 | 53, 23, 54 | sylancl 587 |
. . . . . . . . . 10
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β ((ββπ₯) < Ο β (ββπ₯) β€ Ο)) |
56 | 51, 55 | mpd 15 |
. . . . . . . . 9
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (ββπ₯) β€ Ο) |
57 | | ellogrn 25938 |
. . . . . . . . 9
β’ (π₯ β ran log β (π₯ β β β§ -Ο <
(ββπ₯) β§
(ββπ₯) β€
Ο)) |
58 | 47, 50, 56, 57 | syl3anbrc 1344 |
. . . . . . . 8
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β π₯
β ran log) |
59 | | logef 25960 |
. . . . . . . 8
β’ (π₯ β ran log β
(logβ(expβπ₯)) =
π₯) |
60 | 58, 59 | syl 17 |
. . . . . . 7
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (logβ(expβπ₯)) = π₯) |
61 | | efcl 15973 |
. . . . . . . . . 10
β’ (π₯ β β β
(expβπ₯) β
β) |
62 | 61 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (expβπ₯) β β) |
63 | 53 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) β
β) |
64 | 63 | recnd 11191 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) β
β) |
65 | | picn 25839 |
. . . . . . . . . . . . . 14
β’ Ο
β β |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β Ο β
β) |
67 | | pipos 25840 |
. . . . . . . . . . . . . . 15
β’ 0 <
Ο |
68 | 23, 67 | gt0ne0ii 11699 |
. . . . . . . . . . . . . 14
β’ Ο β
0 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β Ο β
0) |
70 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) < Ο) |
71 | 65 | mulid1i 11167 |
. . . . . . . . . . . . . . . . . 18
β’ (Ο
Β· 1) = Ο |
72 | 70, 71 | breqtrrdi 5151 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) < (Ο Β·
1)) |
73 | | 1re 11163 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β 1 β
β) |
75 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β Ο β
β) |
76 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β 0 <
Ο) |
77 | | ltdivmul 12038 |
. . . . . . . . . . . . . . . . . 18
β’
(((ββπ₯)
β β β§ 1 β β β§ (Ο β β β§ 0 <
Ο)) β (((ββπ₯) / Ο) < 1 β (ββπ₯) < (Ο Β·
1))) |
78 | 63, 74, 75, 76, 77 | syl112anc 1375 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(((ββπ₯) / Ο)
< 1 β (ββπ₯) < (Ο Β· 1))) |
79 | 72, 78 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((ββπ₯) / Ο)
< 1) |
80 | | 1e0p1 12668 |
. . . . . . . . . . . . . . . 16
β’ 1 = (0 +
1) |
81 | 79, 80 | breqtrdi 5150 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((ββπ₯) / Ο)
< (0 + 1)) |
82 | 63 | recoscld 16034 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(cosβ(ββπ₯)) β β) |
83 | 63 | resincld 16033 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(sinβ(ββπ₯)) β β) |
84 | 82, 83 | crimd 15126 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(ββ((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯))))) = (sinβ(ββπ₯))) |
85 | | efeul 16052 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β β β
(expβπ₯) =
((expβ(ββπ₯)) Β· ((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯)))))) |
86 | 85 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (expβπ₯) =
((expβ(ββπ₯)) Β· ((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯)))))) |
87 | 86 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β ((expβπ₯) /
(expβ(ββπ₯))) = (((expβ(ββπ₯)) Β·
((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯))))) / (expβ(ββπ₯)))) |
88 | 82 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(cosβ(ββπ₯)) β β) |
89 | | ax-icn 11118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ i β
β |
90 | 83 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(sinβ(ββπ₯)) β β) |
91 | | mulcl 11143 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((i
β β β§ (sinβ(ββπ₯)) β β) β (i Β·
(sinβ(ββπ₯))) β β) |
92 | 89, 90, 91 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (i Β·
(sinβ(ββπ₯))) β β) |
93 | 88, 92 | addcld 11182 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯)))) β β) |
94 | | recl 15004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β β β
(ββπ₯) β
β) |
95 | 94 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) β
β) |
96 | 95 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) β
β) |
97 | | efcl 15973 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((ββπ₯)
β β β (expβ(ββπ₯)) β β) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(expβ(ββπ₯)) β β) |
99 | | efne0 15987 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((ββπ₯)
β β β (expβ(ββπ₯)) β 0) |
100 | 96, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(expβ(ββπ₯)) β 0) |
101 | 93, 98, 100 | divcan3d 11944 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(((expβ(ββπ₯)) Β· ((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯))))) / (expβ(ββπ₯))) =
((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯))))) |
102 | 87, 101 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β ((expβπ₯) /
(expβ(ββπ₯))) = ((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯))))) |
103 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (expβπ₯) β
β) |
104 | 95 | reefcld 15978 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(expβ(ββπ₯)) β β) |
105 | 103, 104,
100 | redivcld 11991 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β ((expβπ₯) /
(expβ(ββπ₯))) β β) |
106 | 102, 105 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯)))) β β) |
107 | 106 | reim0d 15119 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(ββ((cosβ(ββπ₯)) + (i Β·
(sinβ(ββπ₯))))) = 0) |
108 | 84, 107 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(sinβ(ββπ₯)) = 0) |
109 | | sineq0 25903 |
. . . . . . . . . . . . . . . . . 18
β’
((ββπ₯)
β β β ((sinβ(ββπ₯)) = 0 β ((ββπ₯) / Ο) β
β€)) |
110 | 64, 109 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((sinβ(ββπ₯)) = 0 β ((ββπ₯) / Ο) β
β€)) |
111 | 108, 110 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((ββπ₯) / Ο)
β β€) |
112 | | 0z 12518 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β€ |
113 | | zleltp1 12562 |
. . . . . . . . . . . . . . . 16
β’
((((ββπ₯)
/ Ο) β β€ β§ 0 β β€) β (((ββπ₯) / Ο) β€ 0 β
((ββπ₯) / Ο)
< (0 + 1))) |
114 | 111, 112,
113 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(((ββπ₯) / Ο)
β€ 0 β ((ββπ₯) / Ο) < (0 + 1))) |
115 | 81, 114 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((ββπ₯) / Ο)
β€ 0) |
116 | | df-neg 11396 |
. . . . . . . . . . . . . . . 16
β’ -1 = (0
β 1) |
117 | 65 | mulm1i 11608 |
. . . . . . . . . . . . . . . . . 18
β’ (-1
Β· Ο) = -Ο |
118 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β -Ο <
(ββπ₯)) |
119 | 117, 118 | eqbrtrid 5144 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (-1 Β· Ο)
< (ββπ₯)) |
120 | 73 | renegcli 11470 |
. . . . . . . . . . . . . . . . . . 19
β’ -1 β
β |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β -1 β
β) |
122 | | ltmuldiv 12036 |
. . . . . . . . . . . . . . . . . 18
β’ ((-1
β β β§ (ββπ₯) β β β§ (Ο β β
β§ 0 < Ο)) β ((-1 Β· Ο) < (ββπ₯) β -1 <
((ββπ₯) /
Ο))) |
123 | 121, 63, 75, 76, 122 | syl112anc 1375 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β ((-1 Β· Ο)
< (ββπ₯)
β -1 < ((ββπ₯) / Ο))) |
124 | 119, 123 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β -1 <
((ββπ₯) /
Ο)) |
125 | 116, 124 | eqbrtrrid 5145 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (0 β 1) <
((ββπ₯) /
Ο)) |
126 | | zlem1lt 12563 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β€ β§ ((ββπ₯) / Ο) β β€) β (0 β€
((ββπ₯) / Ο)
β (0 β 1) < ((ββπ₯) / Ο))) |
127 | 112, 111,
126 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (0 β€
((ββπ₯) / Ο)
β (0 β 1) < ((ββπ₯) / Ο))) |
128 | 125, 127 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β 0 β€
((ββπ₯) /
Ο)) |
129 | 63, 75, 69 | redivcld 11991 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((ββπ₯) / Ο)
β β) |
130 | | 0re 11165 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
131 | | letri3 11248 |
. . . . . . . . . . . . . . 15
β’
((((ββπ₯)
/ Ο) β β β§ 0 β β) β (((ββπ₯) / Ο) = 0 β
(((ββπ₯) / Ο)
β€ 0 β§ 0 β€ ((ββπ₯) / Ο)))) |
132 | 129, 130,
131 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
(((ββπ₯) / Ο)
= 0 β (((ββπ₯) / Ο) β€ 0 β§ 0 β€
((ββπ₯) /
Ο)))) |
133 | 115, 128,
132 | mpbir2and 712 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β
((ββπ₯) / Ο)
= 0) |
134 | 64, 66, 69, 133 | diveq0d 11946 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (ββπ₯) = 0) |
135 | | reim0b 15013 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ β β β
(ββπ₯) =
0)) |
136 | 135 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (π₯ β β β (ββπ₯) = 0)) |
137 | 134, 136 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β π₯ β β) |
138 | 137 | rpefcld 15995 |
. . . . . . . . . 10
β’ (((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β§ (expβπ₯) β β) β (expβπ₯) β
β+) |
139 | 138 | ex 414 |
. . . . . . . . 9
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β ((expβπ₯) β β β (expβπ₯) β
β+)) |
140 | 4 | ellogdm 26017 |
. . . . . . . . 9
β’
((expβπ₯)
β π· β
((expβπ₯) β
β β§ ((expβπ₯) β β β (expβπ₯) β
β+))) |
141 | 62, 139, 140 | sylanbrc 584 |
. . . . . . . 8
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (expβπ₯) β π·) |
142 | | funfvima2 7185 |
. . . . . . . . 9
β’ ((Fun log
β§ π· β dom log)
β ((expβπ₯)
β π· β
(logβ(expβπ₯))
β (log β π·))) |
143 | 9, 13, 142 | mp2an 691 |
. . . . . . . 8
β’
((expβπ₯)
β π· β
(logβ(expβπ₯))
β (log β π·)) |
144 | 141, 143 | syl 17 |
. . . . . . 7
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (logβ(expβπ₯)) β (log β π·)) |
145 | 60, 144 | eqeltrrd 2835 |
. . . . . 6
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β π₯
β (log β π·)) |
146 | 46, 145 | sylbi 216 |
. . . . 5
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β π₯ β (log β π·)) |
147 | 146 | ssriv 3952 |
. . . 4
β’ (β‘β β (-Ο(,)Ο)) β (log
β π·) |
148 | 44, 147 | eqssi 3964 |
. . 3
β’ (log
β π·) = (β‘β β
(-Ο(,)Ο)) |
149 | | f1oeq3 6778 |
. . 3
β’ ((log
β π·) = (β‘β β (-Ο(,)Ο)) β ((log
βΎ π·):π·β1-1-ontoβ(log
β π·) β (log
βΎ π·):π·β1-1-ontoβ(β‘β β
(-Ο(,)Ο)))) |
150 | 148, 149 | ax-mp 5 |
. 2
β’ ((log
βΎ π·):π·β1-1-ontoβ(log
β π·) β (log
βΎ π·):π·β1-1-ontoβ(β‘β β
(-Ο(,)Ο))) |
151 | 7, 150 | mpbi 229 |
1
β’ (log
βΎ π·):π·β1-1-ontoβ(β‘β β
(-Ο(,)Ο)) |