Step | Hyp | Ref
| Expression |
1 | | imcl 15002 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | | gt0ne0 11625 |
. . . . . . . 8
โข
(((โโ๐ด)
โ โ โง 0 < (โโ๐ด)) โ (โโ๐ด) โ 0) |
3 | 1, 2 | sylan 581 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ๐ด) โ
0) |
4 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ด = 0 โ (โโ๐ด) =
(โโ0)) |
5 | | im0 15044 |
. . . . . . . . 9
โข
(โโ0) = 0 |
6 | 4, 5 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ด = 0 โ (โโ๐ด) = 0) |
7 | 6 | necon3i 2973 |
. . . . . . 7
โข
((โโ๐ด)
โ 0 โ ๐ด โ
0) |
8 | 3, 7 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
๐ด โ 0) |
9 | | logcl 25940 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
10 | 8, 9 | syldan 592 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(logโ๐ด) โ
โ) |
11 | | ax-icn 11115 |
. . . . . 6
โข i โ
โ |
12 | | picn 25832 |
. . . . . 6
โข ฯ
โ โ |
13 | 11, 12 | mulcli 11167 |
. . . . 5
โข (i
ยท ฯ) โ โ |
14 | | efsub 15987 |
. . . . 5
โข
(((logโ๐ด)
โ โ โง (i ยท ฯ) โ โ) โ
(expโ((logโ๐ด)
โ (i ยท ฯ))) = ((expโ(logโ๐ด)) / (expโ(i ยท
ฯ)))) |
15 | 10, 13, 14 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(expโ((logโ๐ด)
โ (i ยท ฯ))) = ((expโ(logโ๐ด)) / (expโ(i ยท
ฯ)))) |
16 | | eflog 25948 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ
(expโ(logโ๐ด)) =
๐ด) |
17 | 8, 16 | syldan 592 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(expโ(logโ๐ด)) =
๐ด) |
18 | | efipi 25846 |
. . . . . 6
โข
(expโ(i ยท ฯ)) = -1 |
19 | 18 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(expโ(i ยท ฯ)) = -1) |
20 | 17, 19 | oveq12d 7376 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((expโ(logโ๐ด))
/ (expโ(i ยท ฯ))) = (๐ด / -1)) |
21 | | ax-1cn 11114 |
. . . . . . 7
โข 1 โ
โ |
22 | | ax-1ne0 11125 |
. . . . . . 7
โข 1 โ
0 |
23 | | divneg2 11884 |
. . . . . . 7
โข ((๐ด โ โ โง 1 โ
โ โง 1 โ 0) โ -(๐ด / 1) = (๐ด / -1)) |
24 | 21, 22, 23 | mp3an23 1454 |
. . . . . 6
โข (๐ด โ โ โ -(๐ด / 1) = (๐ด / -1)) |
25 | | div1 11849 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด / 1) = ๐ด) |
26 | 25 | negeqd 11400 |
. . . . . 6
โข (๐ด โ โ โ -(๐ด / 1) = -๐ด) |
27 | 24, 26 | eqtr3d 2775 |
. . . . 5
โข (๐ด โ โ โ (๐ด / -1) = -๐ด) |
28 | 27 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(๐ด / -1) = -๐ด) |
29 | 15, 20, 28 | 3eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(expโ((logโ๐ด)
โ (i ยท ฯ))) = -๐ด) |
30 | 29 | fveq2d 6847 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(logโ(expโ((logโ๐ด) โ (i ยท ฯ)))) =
(logโ-๐ด)) |
31 | | subcl 11405 |
. . . . 5
โข
(((logโ๐ด)
โ โ โง (i ยท ฯ) โ โ) โ ((logโ๐ด) โ (i ยท ฯ))
โ โ) |
32 | 10, 13, 31 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((logโ๐ด) โ (i
ยท ฯ)) โ โ) |
33 | | argimgt0 25983 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ (0(,)ฯ)) |
34 | | eliooord 13329 |
. . . . . . . . 9
โข
((โโ(logโ๐ด)) โ (0(,)ฯ) โ (0 <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < ฯ)) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(0 < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < ฯ)) |
36 | 35 | simpld 496 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ(logโ๐ด))) |
37 | | imcl 15002 |
. . . . . . . . 9
โข
((logโ๐ด)
โ โ โ (โโ(logโ๐ด)) โ โ) |
38 | 10, 37 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
39 | | pire 25831 |
. . . . . . . . 9
โข ฯ
โ โ |
40 | 39 | renegcli 11467 |
. . . . . . . 8
โข -ฯ
โ โ |
41 | | ltaddpos2 11651 |
. . . . . . . 8
โข
(((โโ(logโ๐ด)) โ โ โง -ฯ โ
โ) โ (0 < (โโ(logโ๐ด)) โ -ฯ <
((โโ(logโ๐ด)) + -ฯ))) |
42 | 38, 40, 41 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(0 < (โโ(logโ๐ด)) โ -ฯ <
((โโ(logโ๐ด)) + -ฯ))) |
43 | 36, 42 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ < ((โโ(logโ๐ด)) + -ฯ)) |
44 | 38 | recnd 11188 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
45 | | negsub 11454 |
. . . . . . 7
โข
(((โโ(logโ๐ด)) โ โ โง ฯ โ โ)
โ ((โโ(logโ๐ด)) + -ฯ) =
((โโ(logโ๐ด)) โ ฯ)) |
46 | 44, 12, 45 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((โโ(logโ๐ด)) + -ฯ) =
((โโ(logโ๐ด)) โ ฯ)) |
47 | 43, 46 | breqtrd 5132 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ < ((โโ(logโ๐ด)) โ ฯ)) |
48 | | imsub 15026 |
. . . . . . 7
โข
(((logโ๐ด)
โ โ โง (i ยท ฯ) โ โ) โ
(โโ((logโ๐ด) โ (i ยท ฯ))) =
((โโ(logโ๐ด)) โ (โโ(i ยท
ฯ)))) |
49 | 10, 13, 48 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((logโ๐ด) โ (i ยท ฯ))) =
((โโ(logโ๐ด)) โ (โโ(i ยท
ฯ)))) |
50 | | reim 15000 |
. . . . . . . . 9
โข (ฯ
โ โ โ (โโฯ) = (โโ(i ยท
ฯ))) |
51 | 12, 50 | ax-mp 5 |
. . . . . . . 8
โข
(โโฯ) = (โโ(i ยท ฯ)) |
52 | | rere 15013 |
. . . . . . . . 9
โข (ฯ
โ โ โ (โโฯ) = ฯ) |
53 | 39, 52 | ax-mp 5 |
. . . . . . . 8
โข
(โโฯ) = ฯ |
54 | 51, 53 | eqtr3i 2763 |
. . . . . . 7
โข
(โโ(i ยท ฯ)) = ฯ |
55 | 54 | oveq2i 7369 |
. . . . . 6
โข
((โโ(logโ๐ด)) โ (โโ(i ยท
ฯ))) = ((โโ(logโ๐ด)) โ ฯ) |
56 | 49, 55 | eqtrdi 2789 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((logโ๐ด) โ (i ยท ฯ))) =
((โโ(logโ๐ด)) โ ฯ)) |
57 | 47, 56 | breqtrrd 5134 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ < (โโ((logโ๐ด) โ (i ยท
ฯ)))) |
58 | | resubcl 11470 |
. . . . . . 7
โข
(((โโ(logโ๐ด)) โ โ โง ฯ โ โ)
โ ((โโ(logโ๐ด)) โ ฯ) โ
โ) |
59 | 38, 39, 58 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((โโ(logโ๐ด)) โ ฯ) โ
โ) |
60 | 39 | a1i 11 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
ฯ โ โ) |
61 | | 0re 11162 |
. . . . . . . 8
โข 0 โ
โ |
62 | | pipos 25833 |
. . . . . . . 8
โข 0 <
ฯ |
63 | 61, 39, 62 | ltleii 11283 |
. . . . . . 7
โข 0 โค
ฯ |
64 | | subge02 11676 |
. . . . . . . 8
โข
(((โโ(logโ๐ด)) โ โ โง ฯ โ โ)
โ (0 โค ฯ โ ((โโ(logโ๐ด)) โ ฯ) โค
(โโ(logโ๐ด)))) |
65 | 38, 39, 64 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(0 โค ฯ โ ((โโ(logโ๐ด)) โ ฯ) โค
(โโ(logโ๐ด)))) |
66 | 63, 65 | mpbii 232 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((โโ(logโ๐ด)) โ ฯ) โค
(โโ(logโ๐ด))) |
67 | | logimcl 25941 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ (-ฯ <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
68 | 8, 67 | syldan 592 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-ฯ < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
69 | 68 | simprd 497 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โค ฯ) |
70 | 59, 38, 60, 66, 69 | letrd 11317 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((โโ(logโ๐ด)) โ ฯ) โค ฯ) |
71 | 56, 70 | eqbrtrd 5128 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((logโ๐ด) โ (i ยท ฯ))) โค
ฯ) |
72 | | ellogrn 25931 |
. . . 4
โข
(((logโ๐ด)
โ (i ยท ฯ)) โ ran log โ (((logโ๐ด) โ (i ยท ฯ)) โ โ
โง -ฯ < (โโ((logโ๐ด) โ (i ยท ฯ))) โง
(โโ((logโ๐ด) โ (i ยท ฯ))) โค
ฯ)) |
73 | 32, 57, 71, 72 | syl3anbrc 1344 |
. . 3
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((logโ๐ด) โ (i
ยท ฯ)) โ ran log) |
74 | | logef 25953 |
. . 3
โข
(((logโ๐ด)
โ (i ยท ฯ)) โ ran log โ
(logโ(expโ((logโ๐ด) โ (i ยท ฯ)))) =
((logโ๐ด) โ (i
ยท ฯ))) |
75 | 73, 74 | syl 17 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(logโ(expโ((logโ๐ด) โ (i ยท ฯ)))) =
((logโ๐ด) โ (i
ยท ฯ))) |
76 | 30, 75 | eqtr3d 2775 |
1
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(logโ-๐ด) =
((logโ๐ด) โ (i
ยท ฯ))) |