Step | Hyp | Ref
| Expression |
1 | | logcl 25940 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
2 | 1 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(logโ๐ด) โ
โ) |
3 | | ax-icn 11115 |
. . . . . 6
โข i โ
โ |
4 | | halfpire 25837 |
. . . . . . 7
โข (ฯ /
2) โ โ |
5 | 4 | recni 11174 |
. . . . . 6
โข (ฯ /
2) โ โ |
6 | 3, 5 | mulcli 11167 |
. . . . 5
โข (i
ยท (ฯ / 2)) โ โ |
7 | | efadd 15981 |
. . . . 5
โข
(((logโ๐ด)
โ โ โง (i ยท (ฯ / 2)) โ โ) โ
(expโ((logโ๐ด) +
(i ยท (ฯ / 2)))) = ((expโ(logโ๐ด)) ยท (expโ(i ยท (ฯ /
2))))) |
8 | 2, 6, 7 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(expโ((logโ๐ด) +
(i ยท (ฯ / 2)))) = ((expโ(logโ๐ด)) ยท (expโ(i ยท (ฯ /
2))))) |
9 | | eflog 25948 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ
(expโ(logโ๐ด)) =
๐ด) |
10 | 9 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(expโ(logโ๐ด)) =
๐ด) |
11 | | efhalfpi 25844 |
. . . . . 6
โข
(expโ(i ยท (ฯ / 2))) = i |
12 | 11 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(expโ(i ยท (ฯ / 2))) = i) |
13 | 10, 12 | oveq12d 7376 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
((expโ(logโ๐ด))
ยท (expโ(i ยท (ฯ / 2)))) = (๐ด ยท i)) |
14 | | simp1 1137 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
๐ด โ
โ) |
15 | | mulcom 11142 |
. . . . 5
โข ((๐ด โ โ โง i โ
โ) โ (๐ด ยท
i) = (i ยท ๐ด)) |
16 | 14, 3, 15 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(๐ด ยท i) = (i
ยท ๐ด)) |
17 | 8, 13, 16 | 3eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(expโ((logโ๐ด) +
(i ยท (ฯ / 2)))) = (i ยท ๐ด)) |
18 | 17 | fveq2d 6847 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(logโ(expโ((logโ๐ด) + (i ยท (ฯ / 2))))) =
(logโ(i ยท ๐ด))) |
19 | | addcl 11138 |
. . . . 5
โข
(((logโ๐ด)
โ โ โง (i ยท (ฯ / 2)) โ โ) โ
((logโ๐ด) + (i
ยท (ฯ / 2))) โ โ) |
20 | 2, 6, 19 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
((logโ๐ด) + (i
ยท (ฯ / 2))) โ โ) |
21 | | pire 25831 |
. . . . . . . 8
โข ฯ
โ โ |
22 | 21 | renegcli 11467 |
. . . . . . 7
โข -ฯ
โ โ |
23 | 22 | a1i 11 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
-ฯ โ โ) |
24 | 2 | imcld 15086 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
25 | | readdcl 11139 |
. . . . . . 7
โข
(((โโ(logโ๐ด)) โ โ โง (ฯ / 2) โ
โ) โ ((โโ(logโ๐ด)) + (ฯ / 2)) โ
โ) |
26 | 24, 4, 25 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
((โโ(logโ๐ด)) + (ฯ / 2)) โ
โ) |
27 | | logimcl 25941 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ (-ฯ <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
28 | 27 | 3adant3 1133 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(-ฯ < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
29 | 28 | simpld 496 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
-ฯ < (โโ(logโ๐ด))) |
30 | | pirp 25834 |
. . . . . . . 8
โข ฯ
โ โ+ |
31 | | rphalfcl 12947 |
. . . . . . . 8
โข (ฯ
โ โ+ โ (ฯ / 2) โ
โ+) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
โข (ฯ /
2) โ โ+ |
33 | | ltaddrp 12957 |
. . . . . . 7
โข
(((โโ(logโ๐ด)) โ โ โง (ฯ / 2) โ
โ+) โ (โโ(logโ๐ด)) < ((โโ(logโ๐ด)) + (ฯ /
2))) |
34 | 24, 32, 33 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ(logโ๐ด)) < ((โโ(logโ๐ด)) + (ฯ /
2))) |
35 | 23, 24, 26, 29, 34 | lttrd 11321 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
-ฯ < ((โโ(logโ๐ด)) + (ฯ / 2))) |
36 | | imadd 15025 |
. . . . . . 7
โข
(((logโ๐ด)
โ โ โง (i ยท (ฯ / 2)) โ โ) โ
(โโ((logโ๐ด) + (i ยท (ฯ / 2)))) =
((โโ(logโ๐ด)) + (โโ(i ยท (ฯ /
2))))) |
37 | 2, 6, 36 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ((logโ๐ด) + (i ยท (ฯ / 2)))) =
((โโ(logโ๐ด)) + (โโ(i ยท (ฯ /
2))))) |
38 | | reim 15000 |
. . . . . . . . 9
โข ((ฯ /
2) โ โ โ (โโ(ฯ / 2)) = (โโ(i ยท
(ฯ / 2)))) |
39 | 5, 38 | ax-mp 5 |
. . . . . . . 8
โข
(โโ(ฯ / 2)) = (โโ(i ยท (ฯ /
2))) |
40 | | rere 15013 |
. . . . . . . . 9
โข ((ฯ /
2) โ โ โ (โโ(ฯ / 2)) = (ฯ /
2)) |
41 | 4, 40 | ax-mp 5 |
. . . . . . . 8
โข
(โโ(ฯ / 2)) = (ฯ / 2) |
42 | 39, 41 | eqtr3i 2763 |
. . . . . . 7
โข
(โโ(i ยท (ฯ / 2))) = (ฯ / 2) |
43 | 42 | oveq2i 7369 |
. . . . . 6
โข
((โโ(logโ๐ด)) + (โโ(i ยท (ฯ /
2)))) = ((โโ(logโ๐ด)) + (ฯ / 2)) |
44 | 37, 43 | eqtrdi 2789 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ((logโ๐ด) + (i ยท (ฯ / 2)))) =
((โโ(logโ๐ด)) + (ฯ / 2))) |
45 | 35, 44 | breqtrrd 5134 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
-ฯ < (โโ((logโ๐ด) + (i ยท (ฯ /
2))))) |
46 | | argrege0 25982 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ (-(ฯ / 2)[,](ฯ /
2))) |
47 | 4 | renegcli 11467 |
. . . . . . . . . 10
โข -(ฯ /
2) โ โ |
48 | 47, 4 | elicc2i 13336 |
. . . . . . . . 9
โข
((โโ(logโ๐ด)) โ (-(ฯ / 2)[,](ฯ / 2)) โ
((โโ(logโ๐ด)) โ โ โง -(ฯ / 2) โค
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค (ฯ /
2))) |
49 | 48 | simp3bi 1148 |
. . . . . . . 8
โข
((โโ(logโ๐ด)) โ (-(ฯ / 2)[,](ฯ / 2)) โ
(โโ(logโ๐ด)) โค (ฯ / 2)) |
50 | 46, 49 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ(logโ๐ด)) โค (ฯ / 2)) |
51 | 21 | recni 11174 |
. . . . . . . 8
โข ฯ
โ โ |
52 | | pidiv2halves 25840 |
. . . . . . . 8
โข ((ฯ /
2) + (ฯ / 2)) = ฯ |
53 | 51, 5, 5, 52 | subaddrii 11495 |
. . . . . . 7
โข (ฯ
โ (ฯ / 2)) = (ฯ / 2) |
54 | 50, 53 | breqtrrdi 5148 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ(logโ๐ด)) โค (ฯ โ (ฯ /
2))) |
55 | 4 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(ฯ / 2) โ โ) |
56 | 21 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
ฯ โ โ) |
57 | | leaddsub 11636 |
. . . . . . 7
โข
(((โโ(logโ๐ด)) โ โ โง (ฯ / 2) โ
โ โง ฯ โ โ) โ (((โโ(logโ๐ด)) + (ฯ / 2)) โค ฯ
โ (โโ(logโ๐ด)) โค (ฯ โ (ฯ /
2)))) |
58 | 24, 55, 56, 57 | syl3anc 1372 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(((โโ(logโ๐ด)) + (ฯ / 2)) โค ฯ โ
(โโ(logโ๐ด)) โค (ฯ โ (ฯ /
2)))) |
59 | 54, 58 | mpbird 257 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
((โโ(logโ๐ด)) + (ฯ / 2)) โค ฯ) |
60 | 44, 59 | eqbrtrd 5128 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(โโ((logโ๐ด) + (i ยท (ฯ / 2)))) โค
ฯ) |
61 | | ellogrn 25931 |
. . . 4
โข
(((logโ๐ด) + (i
ยท (ฯ / 2))) โ ran log โ (((logโ๐ด) + (i ยท (ฯ / 2))) โ โ
โง -ฯ < (โโ((logโ๐ด) + (i ยท (ฯ / 2)))) โง
(โโ((logโ๐ด) + (i ยท (ฯ / 2)))) โค
ฯ)) |
62 | 20, 45, 60, 61 | syl3anbrc 1344 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
((logโ๐ด) + (i
ยท (ฯ / 2))) โ ran log) |
63 | | logef 25953 |
. . 3
โข
(((logโ๐ด) + (i
ยท (ฯ / 2))) โ ran log โ
(logโ(expโ((logโ๐ด) + (i ยท (ฯ / 2))))) =
((logโ๐ด) + (i
ยท (ฯ / 2)))) |
64 | 62, 63 | syl 17 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(logโ(expโ((logโ๐ด) + (i ยท (ฯ / 2))))) =
((logโ๐ด) + (i
ยท (ฯ / 2)))) |
65 | 18, 64 | eqtr3d 2775 |
1
โข ((๐ด โ โ โง ๐ด โ 0 โง 0 โค
(โโ๐ด)) โ
(logโ(i ยท ๐ด))
= ((logโ๐ด) + (i
ยท (ฯ / 2)))) |