Step | Hyp | Ref
| Expression |
1 | | recl 15063 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | | gt0ne0 11683 |
. . . . . 6
โข
(((โโ๐ด)
โ โ โง 0 < (โโ๐ด)) โ (โโ๐ด) โ 0) |
3 | 1, 2 | sylan 579 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ๐ด) โ
0) |
4 | | fveq2 6885 |
. . . . . . 7
โข (๐ด = 0 โ (โโ๐ด) =
(โโ0)) |
5 | | re0 15105 |
. . . . . . 7
โข
(โโ0) = 0 |
6 | 4, 5 | eqtrdi 2782 |
. . . . . 6
โข (๐ด = 0 โ (โโ๐ด) = 0) |
7 | 6 | necon3i 2967 |
. . . . 5
โข
((โโ๐ด)
โ 0 โ ๐ด โ
0) |
8 | 3, 7 | syl 17 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
๐ด โ 0) |
9 | | logcl 26457 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
10 | 8, 9 | syldan 590 |
. . 3
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(logโ๐ด) โ
โ) |
11 | 10 | imcld 15148 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
12 | | coshalfpi 26359 |
. . . . . 6
โข
(cosโ(ฯ / 2)) = 0 |
13 | | simpr 484 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ๐ด)) |
14 | | abscl 15231 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
โ) |
16 | 15 | recnd 11246 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
โ) |
17 | 16 | mul01d 11417 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท 0)
= 0) |
18 | | simpl 482 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
๐ด โ
โ) |
19 | | absrpcl 15241 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ
โ+) |
20 | 8, 19 | syldan 590 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
โ+) |
21 | 20 | rpne0d 13027 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ๐ด) โ
0) |
22 | 18, 16, 21 | divcld 11994 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(๐ด / (absโ๐ด)) โ
โ) |
23 | 15, 22 | remul2d 15180 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((absโ๐ด) ยท (๐ด / (absโ๐ด)))) = ((absโ๐ด) ยท (โโ(๐ด / (absโ๐ด))))) |
24 | 18, 16, 21 | divcan2d 11996 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท
(๐ด / (absโ๐ด))) = ๐ด) |
25 | 24 | fveq2d 6889 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ((absโ๐ด) ยท (๐ด / (absโ๐ด)))) = (โโ๐ด)) |
26 | 23, 25 | eqtr3d 2768 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท
(โโ(๐ด /
(absโ๐ด)))) =
(โโ๐ด)) |
27 | 13, 17, 26 | 3brtr4d 5173 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ๐ด) ยท 0)
< ((absโ๐ด)
ยท (โโ(๐ด /
(absโ๐ด))))) |
28 | | 0re 11220 |
. . . . . . . . . . . 12
โข 0 โ
โ |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
โ โ) |
30 | 22 | recld 15147 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(๐ด /
(absโ๐ด))) โ
โ) |
31 | 29, 30, 20 | ltmul2d 13064 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ (0
< (โโ(๐ด /
(absโ๐ด))) โ
((absโ๐ด) ยท 0)
< ((absโ๐ด)
ยท (โโ(๐ด /
(absโ๐ด)))))) |
32 | 27, 31 | mpbird 257 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ(๐ด /
(absโ๐ด)))) |
33 | | efiarg 26496 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ (expโ(i
ยท (โโ(logโ๐ด)))) = (๐ด / (absโ๐ด))) |
34 | 8, 33 | syldan 590 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(expโ(i ยท (โโ(logโ๐ด)))) = (๐ด / (absโ๐ด))) |
35 | 34 | fveq2d 6889 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(expโ(i ยท (โโ(logโ๐ด))))) = (โโ(๐ด / (absโ๐ด)))) |
36 | 32, 35 | breqtrrd 5169 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (โโ(expโ(i ยท (โโ(logโ๐ด)))))) |
37 | | recosval 16086 |
. . . . . . . . 9
โข
((โโ(logโ๐ด)) โ โ โ
(cosโ(โโ(logโ๐ด))) = (โโ(expโ(i ยท
(โโ(logโ๐ด)))))) |
38 | 11, 37 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ(โโ(logโ๐ด))) = (โโ(expโ(i ยท
(โโ(logโ๐ด)))))) |
39 | 36, 38 | breqtrrd 5169 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (cosโ(โโ(logโ๐ด)))) |
40 | | fveq2 6885 |
. . . . . . . . 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 11246 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ โ) |
43 | | cosneg 16097 |
. . . . . . . . . 10
โข
((โโ(logโ๐ด)) โ โ โ
(cosโ-(โโ(logโ๐ด))) =
(cosโ(โโ(logโ๐ด)))) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ-(โโ(logโ๐ด))) =
(cosโ(โโ(logโ๐ด)))) |
45 | | fveqeq2 6894 |
. . . . . . . . 9
โข
((absโ(โโ(logโ๐ด))) = -(โโ(logโ๐ด)) โ
((cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด))) โ
(cosโ-(โโ(logโ๐ด))) =
(cosโ(โโ(logโ๐ด))))) |
46 | 44, 45 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) = -(โโ(logโ๐ด)) โ
(cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด))))) |
47 | 11 | absord 15368 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) = (โโ(logโ๐ด)) โจ
(absโ(โโ(logโ๐ด))) = -(โโ(logโ๐ด)))) |
48 | 41, 46, 47 | mpjaod 857 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ(absโ(โโ(logโ๐ด)))) =
(cosโ(โโ(logโ๐ด)))) |
49 | 39, 48 | breqtrrd 5169 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
< (cosโ(absโ(โโ(logโ๐ด))))) |
50 | 12, 49 | eqbrtrid 5176 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(cosโ(ฯ / 2)) <
(cosโ(absโ(โโ(logโ๐ด))))) |
51 | 42 | abscld 15389 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) โ โ) |
52 | 42 | absge0d 15397 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ 0
โค (absโ(โโ(logโ๐ด)))) |
53 | | logimcl 26458 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ (-ฯ <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
54 | 8, 53 | syldan 590 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-ฯ < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ)) |
55 | 54 | simpld 494 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ < (โโ(logโ๐ด))) |
56 | | pire 26348 |
. . . . . . . . . . 11
โข ฯ
โ โ |
57 | 56 | renegcli 11525 |
. . . . . . . . . 10
โข -ฯ
โ โ |
58 | | ltle 11306 |
. . . . . . . . . 10
โข ((-ฯ
โ โ โง (โโ(logโ๐ด)) โ โ) โ (-ฯ <
(โโ(logโ๐ด)) โ -ฯ โค
(โโ(logโ๐ด)))) |
59 | 57, 11, 58 | sylancr 586 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-ฯ < (โโ(logโ๐ด)) โ -ฯ โค
(โโ(logโ๐ด)))) |
60 | 55, 59 | mpd 15 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-ฯ โค (โโ(logโ๐ด))) |
61 | 54 | simprd 495 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โค ฯ) |
62 | | absle 15268 |
. . . . . . . . 9
โข
(((โโ(logโ๐ด)) โ โ โง ฯ โ โ)
โ ((absโ(โโ(logโ๐ด))) โค ฯ โ (-ฯ โค
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ))) |
63 | 11, 56, 62 | sylancl 585 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) โค ฯ โ (-ฯ โค
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) โค ฯ))) |
64 | 60, 61, 63 | mpbir2and 710 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) โค ฯ) |
65 | 28, 56 | elicc2i 13396 |
. . . . . . 7
โข
((absโ(โโ(logโ๐ด))) โ (0[,]ฯ) โ
((absโ(โโ(logโ๐ด))) โ โ โง 0 โค
(absโ(โโ(logโ๐ด))) โง
(absโ(โโ(logโ๐ด))) โค ฯ)) |
66 | 51, 52, 64, 65 | syl3anbrc 1340 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) โ (0[,]ฯ)) |
67 | | halfpire 26354 |
. . . . . . 7
โข (ฯ /
2) โ โ |
68 | | pirp 26351 |
. . . . . . . 8
โข ฯ
โ โ+ |
69 | | rphalfcl 13007 |
. . . . . . . 8
โข (ฯ
โ โ+ โ (ฯ / 2) โ
โ+) |
70 | | rpge0 12993 |
. . . . . . . 8
โข ((ฯ /
2) โ โ+ โ 0 โค (ฯ / 2)) |
71 | 68, 69, 70 | mp2b 10 |
. . . . . . 7
โข 0 โค
(ฯ / 2) |
72 | | rphalflt 13009 |
. . . . . . . . 9
โข (ฯ
โ โ+ โ (ฯ / 2) < ฯ) |
73 | 68, 72 | ax-mp 5 |
. . . . . . . 8
โข (ฯ /
2) < ฯ |
74 | 67, 56, 73 | ltleii 11341 |
. . . . . . 7
โข (ฯ /
2) โค ฯ |
75 | 28, 56 | elicc2i 13396 |
. . . . . . 7
โข ((ฯ /
2) โ (0[,]ฯ) โ ((ฯ / 2) โ โ โง 0 โค (ฯ / 2)
โง (ฯ / 2) โค ฯ)) |
76 | 67, 71, 74, 75 | mpbir3an 1338 |
. . . . . 6
โข (ฯ /
2) โ (0[,]ฯ) |
77 | | cosord 26420 |
. . . . . 6
โข
(((absโ(โโ(logโ๐ด))) โ (0[,]ฯ) โง (ฯ / 2)
โ (0[,]ฯ)) โ ((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ
(cosโ(ฯ / 2)) <
(cosโ(absโ(โโ(logโ๐ด)))))) |
78 | 66, 76, 77 | sylancl 585 |
. . . . 5
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ (cosโ(ฯ
/ 2)) < (cosโ(absโ(โโ(logโ๐ด)))))) |
79 | 50, 78 | mpbird 257 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(absโ(โโ(logโ๐ด))) < (ฯ / 2)) |
80 | | abslt 15267 |
. . . . 5
โข
(((โโ(logโ๐ด)) โ โ โง (ฯ / 2) โ
โ) โ ((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ (-(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2)))) |
81 | 11, 67, 80 | sylancl 585 |
. . . 4
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
((absโ(โโ(logโ๐ด))) < (ฯ / 2) โ (-(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2)))) |
82 | 79, 81 | mpbid 231 |
. . 3
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(-(ฯ / 2) < (โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2))) |
83 | 82 | simpld 494 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
-(ฯ / 2) < (โโ(logโ๐ด))) |
84 | 82 | simprd 495 |
. 2
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) < (ฯ / 2)) |
85 | 67 | renegcli 11525 |
. . . 4
โข -(ฯ /
2) โ โ |
86 | 85 | rexri 11276 |
. . 3
โข -(ฯ /
2) โ โ* |
87 | 67 | rexri 11276 |
. . 3
โข (ฯ /
2) โ โ* |
88 | | elioo2 13371 |
. . 3
โข ((-(ฯ
/ 2) โ โ* โง (ฯ / 2) โ โ*)
โ ((โโ(logโ๐ด)) โ (-(ฯ / 2)(,)(ฯ / 2)) โ
((โโ(logโ๐ด)) โ โ โง -(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2)))) |
89 | 86, 87, 88 | mp2an 689 |
. 2
โข
((โโ(logโ๐ด)) โ (-(ฯ / 2)(,)(ฯ / 2)) โ
((โโ(logโ๐ด)) โ โ โง -(ฯ / 2) <
(โโ(logโ๐ด)) โง (โโ(logโ๐ด)) < (ฯ /
2))) |
90 | 11, 83, 84, 89 | syl3anbrc 1340 |
1
โข ((๐ด โ โ โง 0 <
(โโ๐ด)) โ
(โโ(logโ๐ด)) โ (-(ฯ / 2)(,)(ฯ /
2))) |