Step | Hyp | Ref
| Expression |
1 | | recl 15001 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | | gt0ne0 11625 |
. . . . . 6
โข
(((โโ๐ด)
โ โ โง 0 < (โโ๐ด)) โ (โโ๐ด) โ 0) |
3 | 1, 2 | sylan 581 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ๐ด) โ
0) |
4 | | fveq2 6843 |
. . . . . . 7
โข (๐ด = 0 โ (โโ๐ด) =
(โโ0)) |
5 | | re0 15043 |
. . . . . . 7
โข
(โโ0) = 0 |
6 | 4, 5 | eqtrdi 2789 |
. . . . . 6
โข (๐ด = 0 โ (โโ๐ด) = 0) |
7 | 6 | necon3i 2973 |
. . . . 5
โข
((โโ๐ด)
โ 0 โ ๐ด โ
0) |
8 | 3, 7 | syl 17 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
๐ด โ 0) |
9 | | logcl 25940 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
10 | 8, 9 | syldan 592 |
. . 3
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(logโ๐ด) โ
โ) |
11 | 10 | imcld 15086 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
12 | | coshalfpi 25842 |
. . . . . 6
โข
(cosโ(ฯ / 2)) = 0 |
13 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ๐ด)) |
14 | | abscl 15169 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
โ) |
16 | 15 | recnd 11188 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
โ) |
17 | 16 | mul01d 11359 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท 0)
= 0) |
18 | | simpl 484 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
๐ด โ
โ) |
19 | | absrpcl 15179 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ
โ+) |
20 | 8, 19 | syldan 592 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
โ+) |
21 | 20 | rpne0d 12967 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
0) |
22 | 18, 16, 21 | divcld 11936 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(๐ด / (absโ๐ด)) โ
โ) |
23 | 15, 22 | remul2d 15118 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((absโ๐ด) ยท (๐ด / (absโ๐ด)))) = ((absโ๐ด) ยท (โโ(๐ด / (absโ๐ด))))) |
24 | 18, 16, 21 | divcan2d 11938 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท
(๐ด / (absโ๐ด))) = ๐ด) |
25 | 24 | fveq2d 6847 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((absโ๐ด) ยท (๐ด / (absโ๐ด)))) = (โโ๐ด)) |
26 | 23, 25 | eqtr3d 2775 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท
(โโ(๐ด /
(absโ๐ด)))) =
(โโ๐ด)) |
27 | 13, 17, 26 | 3brtr4d 5138 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท 0)
< ((absโ๐ด)
ยท (โโ(๐ด /
(absโ๐ด))))) |
28 | | 0re 11162 |
. . . . . . . . . . . 12
โข 0 โ
โ |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
โ โ) |
30 | 22 | recld 15085 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(๐ด /
(absโ๐ด))) โ
โ) |
31 | 29, 30, 20 | ltmul2d 13004 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ (0
< (โโ(๐ด /
(absโ๐ด))) โ
((absโ๐ด) ยท 0)
< ((absโ๐ด)
ยท (โโ(๐ด /
(absโ๐ด)))))) |
32 | 27, 31 | mpbird 257 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ(๐ด /
(absโ๐ด)))) |
33 | | efiarg 25978 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ (expโ(i
ยท (โโ(logโ๐ด)))) = (๐ด / (absโ๐ด))) |
34 | 8, 33 | syldan 592 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(expโ(i ยท (โโ(logโ๐ด)))) = (๐ด / (absโ๐ด))) |
35 | 34 | fveq2d 6847 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(expโ(i ยท (โโ(logโ๐ด))))) = (โโ(๐ด / (absโ๐ด)))) |
36 | 32, 35 | breqtrrd 5134 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ(expโ(i ยท (โโ(logโ๐ด)))))) |
37 | | recosval 16023 |
. . . . . . . . 9
โข
((โโ(logโ๐ด)) โ โ โ
(cosโ(โโ(logโ๐ด))) = (โโ(expโ(i ยท
(โโ(logโ๐ด)))))) |
38 | 11, 37 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ(โโ(logโ๐ด))) = (โโ(expโ(i ยท
(โโ(logโ๐ด)))))) |
39 | 36, 38 | breqtrrd 5134 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (cosโ(โโ(logโ๐ด)))) |
40 | | fveq2 6843 |
. . . . . . . . 9
โข
((absโ(โโ(logโ๐ด))) = (โโ(logโ๐ด)) โ
(cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด)))) |
41 | 40 | a1i 11 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) = (โโ(logโ๐ด)) โ
(cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด))))) |
42 | 11 | recnd 11188 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
43 | | cosneg 16034 |
. . . . . . . . . 10
โข
((โโ(logโ๐ด)) โ โ โ
(cosโ-(โโ(logโ๐ด))) =
(cosโ(โโ(logโ๐ด)))) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ-(โโ(logโ๐ด))) =
(cosโ(โโ(logโ๐ด)))) |
45 | | fveqeq2 6852 |
. . . . . . . . 9
โข
((absโ(โโ(logโ๐ด))) = -(โโ(logโ๐ด)) โ
((cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด))) โ
(cosโ-(โโ(logโ๐ด))) =
(cosโ(โโ(logโ๐ด))))) |
46 | 44, 45 | syl5ibrcom 247 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) = -(โโ(logโ๐ด)) โ
(cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด))))) |
47 | 11 | absord 15306 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) = (โโ(logโ๐ด)) โจ
(absโ(โโ(logโ๐ด))) = -(โโ(logโ๐ด)))) |
48 | 41, 46, 47 | mpjaod 859 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด)))) |
49 | 39, 48 | breqtrrd 5134 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (cosโ(absโ(โโ(logโ๐ด))))) |
50 | 12, 49 | eqbrtrid 5141 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ(ฯ / 2)) <
(cosโ(absโ(โโ(logโ๐ด))))) |
51 | 42 | abscld 15327 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) โ โ) |
52 | 42 | absge0d 15335 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
โค (absโ(โโ(logโ๐ด)))) |
53 | | logimcl 25941 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ (-ฯ <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
54 | 8, 53 | syldan 592 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-ฯ < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
55 | 54 | simpld 496 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ < (โโ(logโ๐ด))) |
56 | | pire 25831 |
. . . . . . . . . . 11
โข ฯ
โ โ |
57 | 56 | renegcli 11467 |
. . . . . . . . . 10
โข -ฯ
โ โ |
58 | | ltle 11248 |
. . . . . . . . . 10
โข ((-ฯ
โ โ โง (โโ(logโ๐ด)) โ โ) โ (-ฯ <
(โโ(logโ๐ด)) โ -ฯ โค
(โโ(logโ๐ด)))) |
59 | 57, 11, 58 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-ฯ < (โโ(logโ๐ด)) โ -ฯ โค
(โโ(logโ๐ด)))) |
60 | 55, 59 | mpd 15 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ โค (โโ(logโ๐ด))) |
61 | 54 | simprd 497 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โค ฯ) |
62 | | absle 15206 |
. . . . . . . . 9
โข
(((โโ(logโ๐ด)) โ โ โง ฯ โ โ)
โ ((absโ(โโ(logโ๐ด))) โค ฯ โ (-ฯ โค
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ))) |
63 | 11, 56, 62 | sylancl 587 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) โค ฯ โ (-ฯ โค
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ))) |
64 | 60, 61, 63 | mpbir2and 712 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) โค ฯ) |
65 | 28, 56 | elicc2i 13336 |
. . . . . . 7
โข
((absโ(โโ(logโ๐ด))) โ (0[,]ฯ) โ
((absโ(โโ(logโ๐ด))) โ โ โง 0 โค
(absโ(โโ(logโ๐ด))) โง
(absโ(โโ(logโ๐ด))) โค ฯ)) |
66 | 51, 52, 64, 65 | syl3anbrc 1344 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) โ (0[,]ฯ)) |
67 | | halfpire 25837 |
. . . . . . 7
โข (ฯ /
2) โ โ |
68 | | pirp 25834 |
. . . . . . . 8
โข ฯ
โ โ+ |
69 | | rphalfcl 12947 |
. . . . . . . 8
โข (ฯ
โ โ+ โ (ฯ / 2) โ
โ+) |
70 | | rpge0 12933 |
. . . . . . . 8
โข ((ฯ /
2) โ โ+ โ 0 โค (ฯ / 2)) |
71 | 68, 69, 70 | mp2b 10 |
. . . . . . 7
โข 0 โค
(ฯ / 2) |
72 | | rphalflt 12949 |
. . . . . . . . 9
โข (ฯ
โ โ+ โ (ฯ / 2) < ฯ) |
73 | 68, 72 | ax-mp 5 |
. . . . . . . 8
โข (ฯ /
2) < ฯ |
74 | 67, 56, 73 | ltleii 11283 |
. . . . . . 7
โข (ฯ /
2) โค ฯ |
75 | 28, 56 | elicc2i 13336 |
. . . . . . 7
โข ((ฯ /
2) โ (0[,]ฯ) โ ((ฯ / 2) โ โ โง 0 โค (ฯ / 2)
โง (ฯ / 2) โค ฯ)) |
76 | 67, 71, 74, 75 | mpbir3an 1342 |
. . . . . 6
โข (ฯ /
2) โ (0[,]ฯ) |
77 | | cosord 25903 |
. . . . . 6
โข
(((absโ(โโ(logโ๐ด))) โ (0[,]ฯ) โง (ฯ / 2)
โ (0[,]ฯ)) โ ((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ
(cosโ(ฯ / 2)) <
(cosโ(absโ(โโ(logโ๐ด)))))) |
78 | 66, 76, 77 | sylancl 587 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ (cosโ(ฯ
/ 2)) < (cosโ(absโ(โโ(logโ๐ด)))))) |
79 | 50, 78 | mpbird 257 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) < (ฯ / 2)) |
80 | | abslt 15205 |
. . . . 5
โข
(((โโ(logโ๐ด)) โ โ โง (ฯ / 2) โ
โ) โ ((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ (-(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2)))) |
81 | 11, 67, 80 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ (-(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2)))) |
82 | 79, 81 | mpbid 231 |
. . 3
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-(ฯ / 2) < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2))) |
83 | 82 | simpld 496 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-(ฯ / 2) < (โโ(logโ๐ด))) |
84 | 82 | simprd 497 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) < (ฯ / 2)) |
85 | 67 | renegcli 11467 |
. . . 4
โข -(ฯ /
2) โ โ |
86 | 85 | rexri 11218 |
. . 3
โข -(ฯ /
2) โ โ* |
87 | 67 | rexri 11218 |
. . 3
โข (ฯ /
2) โ โ* |
88 | | elioo2 13311 |
. . 3
โข ((-(ฯ
/ 2) โ โ* โง (ฯ / 2) โ โ*)
โ ((โโ(logโ๐ด)) โ (-(ฯ / 2)(,)(ฯ / 2)) โ
((โโ(logโ๐ด)) โ โ โง -(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2)))) |
89 | 86, 87, 88 | mp2an 691 |
. 2
โข
((โโ(logโ๐ด)) โ (-(ฯ / 2)(,)(ฯ / 2)) โ
((โโ(logโ๐ด)) โ โ โง -(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2))) |
90 | 11, 83, 84, 89 | syl3anbrc 1344 |
1
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ (-(ฯ / 2)(,)(ฯ /
2))) |