Step | Hyp | Ref
| Expression |
1 | | imcl 15002 |
. . . . . 6
β’ (π΄ β β β
(ββπ΄) β
β) |
2 | | gt0ne0 11625 |
. . . . . 6
β’
(((ββπ΄)
β β β§ 0 < (ββπ΄)) β (ββπ΄) β 0) |
3 | 1, 2 | sylan 581 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββπ΄) β
0) |
4 | | fveq2 6843 |
. . . . . . 7
β’ (π΄ = 0 β (ββπ΄) =
(ββ0)) |
5 | | im0 15044 |
. . . . . . 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 | | simpr 486 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
< (ββπ΄)) |
13 | | abscl 15169 |
. . . . . . . . . . 11
β’ (π΄ β β β
(absβπ΄) β
β) |
14 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(absβπ΄) β
β) |
15 | 14 | recnd 11188 |
. . . . . . . . 9
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(absβπ΄) β
β) |
16 | 15 | mul01d 11359 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((absβπ΄) Β· 0)
= 0) |
17 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
π΄ β
β) |
18 | | absrpcl 15179 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0) β (absβπ΄) β
β+) |
19 | 8, 18 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(absβπ΄) β
β+) |
20 | 19 | rpne0d 12967 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(absβπ΄) β
0) |
21 | 17, 15, 20 | divcld 11936 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(π΄ / (absβπ΄)) β
β) |
22 | 14, 21 | immul2d 15119 |
. . . . . . . . 9
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ((absβπ΄) Β· (π΄ / (absβπ΄)))) = ((absβπ΄) Β· (ββ(π΄ / (absβπ΄))))) |
23 | 17, 15, 20 | divcan2d 11938 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((absβπ΄) Β·
(π΄ / (absβπ΄))) = π΄) |
24 | 23 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ((absβπ΄) Β· (π΄ / (absβπ΄)))) = (ββπ΄)) |
25 | 22, 24 | eqtr3d 2775 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((absβπ΄) Β·
(ββ(π΄ /
(absβπ΄)))) =
(ββπ΄)) |
26 | 12, 16, 25 | 3brtr4d 5138 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((absβπ΄) Β· 0)
< ((absβπ΄)
Β· (ββ(π΄
/ (absβπ΄))))) |
27 | | 0re 11162 |
. . . . . . . . 9
β’ 0 β
β |
28 | 27 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
β β) |
29 | 21 | imcld 15086 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(π΄ /
(absβπ΄))) β
β) |
30 | 28, 29, 19 | ltmul2d 13004 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(0 < (ββ(π΄ /
(absβπ΄))) β
((absβπ΄) Β· 0)
< ((absβπ΄)
Β· (ββ(π΄
/ (absβπ΄)))))) |
31 | 26, 30 | mpbird 257 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
< (ββ(π΄ /
(absβπ΄)))) |
32 | | efiarg 25978 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β 0) β (expβ(i
Β· (ββ(logβπ΄)))) = (π΄ / (absβπ΄))) |
33 | 8, 32 | syldan 592 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(expβ(i Β· (ββ(logβπ΄)))) = (π΄ / (absβπ΄))) |
34 | 33 | fveq2d 6847 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(expβ(i Β· (ββ(logβπ΄))))) = (ββ(π΄ / (absβπ΄)))) |
35 | 31, 34 | breqtrrd 5134 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
< (ββ(expβ(i Β· (ββ(logβπ΄)))))) |
36 | | resinval 16022 |
. . . . . 6
β’
((ββ(logβπ΄)) β β β
(sinβ(ββ(logβπ΄))) = (ββ(expβ(i Β·
(ββ(logβπ΄)))))) |
37 | 11, 36 | syl 17 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(sinβ(ββ(logβπ΄))) = (ββ(expβ(i Β·
(ββ(logβπ΄)))))) |
38 | 35, 37 | breqtrrd 5134 |
. . . 4
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
< (sinβ(ββ(logβπ΄)))) |
39 | 11 | resincld 16030 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(sinβ(ββ(logβπ΄))) β β) |
40 | 39 | lt0neg2d 11730 |
. . . 4
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(0 < (sinβ(ββ(logβπ΄))) β
-(sinβ(ββ(logβπ΄))) < 0)) |
41 | 38, 40 | mpbid 231 |
. . 3
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
-(sinβ(ββ(logβπ΄))) < 0) |
42 | | pire 25831 |
. . . . . . . . . . 11
β’ Ο
β β |
43 | | readdcl 11139 |
. . . . . . . . . . 11
β’
(((ββ(logβπ΄)) β β β§ Ο β β)
β ((ββ(logβπ΄)) + Ο) β β) |
44 | 11, 42, 43 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((ββ(logβπ΄)) + Ο) β β) |
45 | 44 | adantr 482 |
. . . . . . . . 9
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β
((ββ(logβπ΄)) + Ο) β β) |
46 | | df-neg 11393 |
. . . . . . . . . . . 12
β’ -Ο =
(0 β Ο) |
47 | | logimcl 25941 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0) β (-Ο <
(ββ(logβπ΄)) β§ (ββ(logβπ΄)) β€ Ο)) |
48 | 8, 47 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(-Ο < (ββ(logβπ΄)) β§ (ββ(logβπ΄)) β€ Ο)) |
49 | 48 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
-Ο < (ββ(logβπ΄))) |
50 | 42 | renegcli 11467 |
. . . . . . . . . . . . . 14
β’ -Ο
β β |
51 | | ltle 11248 |
. . . . . . . . . . . . . 14
β’ ((-Ο
β β β§ (ββ(logβπ΄)) β β) β (-Ο <
(ββ(logβπ΄)) β -Ο β€
(ββ(logβπ΄)))) |
52 | 50, 11, 51 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(-Ο < (ββ(logβπ΄)) β -Ο β€
(ββ(logβπ΄)))) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
-Ο β€ (ββ(logβπ΄))) |
54 | 46, 53 | eqbrtrrid 5142 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(0 β Ο) β€ (ββ(logβπ΄))) |
55 | 42 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
Ο β β) |
56 | 28, 55, 11 | lesubaddd 11757 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((0 β Ο) β€ (ββ(logβπ΄)) β 0 β€
((ββ(logβπ΄)) + Ο))) |
57 | 54, 56 | mpbid 231 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
β€ ((ββ(logβπ΄)) + Ο)) |
58 | 57 | adantr 482 |
. . . . . . . . 9
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β 0 β€
((ββ(logβπ΄)) + Ο)) |
59 | 11, 28, 55 | leadd1d 11754 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((ββ(logβπ΄)) β€ 0 β
((ββ(logβπ΄)) + Ο) β€ (0 +
Ο))) |
60 | 59 | biimpa 478 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β
((ββ(logβπ΄)) + Ο) β€ (0 + Ο)) |
61 | | picn 25832 |
. . . . . . . . . . 11
β’ Ο
β β |
62 | 61 | addid2i 11348 |
. . . . . . . . . 10
β’ (0 +
Ο) = Ο |
63 | 60, 62 | breqtrdi 5147 |
. . . . . . . . 9
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β
((ββ(logβπ΄)) + Ο) β€ Ο) |
64 | 27, 42 | elicc2i 13336 |
. . . . . . . . 9
β’
(((ββ(logβπ΄)) + Ο) β (0[,]Ο) β
(((ββ(logβπ΄)) + Ο) β β β§ 0 β€
((ββ(logβπ΄)) + Ο) β§
((ββ(logβπ΄)) + Ο) β€ Ο)) |
65 | 45, 58, 63, 64 | syl3anbrc 1344 |
. . . . . . . 8
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β
((ββ(logβπ΄)) + Ο) β
(0[,]Ο)) |
66 | | sinq12ge0 25881 |
. . . . . . . 8
β’
(((ββ(logβπ΄)) + Ο) β (0[,]Ο) β 0 β€
(sinβ((ββ(logβπ΄)) + Ο))) |
67 | 65, 66 | syl 17 |
. . . . . . 7
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β 0 β€
(sinβ((ββ(logβπ΄)) + Ο))) |
68 | 11 | recnd 11188 |
. . . . . . . . 9
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(logβπ΄)) β β) |
69 | | sinppi 25862 |
. . . . . . . . 9
β’
((ββ(logβπ΄)) β β β
(sinβ((ββ(logβπ΄)) + Ο)) =
-(sinβ(ββ(logβπ΄)))) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(sinβ((ββ(logβπ΄)) + Ο)) =
-(sinβ(ββ(logβπ΄)))) |
71 | 70 | adantr 482 |
. . . . . . 7
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β
(sinβ((ββ(logβπ΄)) + Ο)) =
-(sinβ(ββ(logβπ΄)))) |
72 | 67, 71 | breqtrd 5132 |
. . . . . 6
β’ (((π΄ β β β§ 0 <
(ββπ΄)) β§
(ββ(logβπ΄)) β€ 0) β 0 β€
-(sinβ(ββ(logβπ΄)))) |
73 | 72 | ex 414 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((ββ(logβπ΄)) β€ 0 β 0 β€
-(sinβ(ββ(logβπ΄))))) |
74 | 73 | con3d 152 |
. . . 4
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(Β¬ 0 β€ -(sinβ(ββ(logβπ΄))) β Β¬
(ββ(logβπ΄)) β€ 0)) |
75 | 39 | renegcld 11587 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
-(sinβ(ββ(logβπ΄))) β β) |
76 | | ltnle 11239 |
. . . . 5
β’
((-(sinβ(ββ(logβπ΄))) β β β§ 0 β β)
β (-(sinβ(ββ(logβπ΄))) < 0 β Β¬ 0 β€
-(sinβ(ββ(logβπ΄))))) |
77 | 75, 27, 76 | sylancl 587 |
. . . 4
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(-(sinβ(ββ(logβπ΄))) < 0 β Β¬ 0 β€
-(sinβ(ββ(logβπ΄))))) |
78 | | ltnle 11239 |
. . . . 5
β’ ((0
β β β§ (ββ(logβπ΄)) β β) β (0 <
(ββ(logβπ΄)) β Β¬
(ββ(logβπ΄)) β€ 0)) |
79 | 27, 11, 78 | sylancr 588 |
. . . 4
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(0 < (ββ(logβπ΄)) β Β¬
(ββ(logβπ΄)) β€ 0)) |
80 | 74, 77, 79 | 3imtr4d 294 |
. . 3
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(-(sinβ(ββ(logβπ΄))) < 0 β 0 <
(ββ(logβπ΄)))) |
81 | 41, 80 | mpd 15 |
. 2
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β 0
< (ββ(logβπ΄))) |
82 | 48 | simprd 497 |
. . 3
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(logβπ΄)) β€ Ο) |
83 | | rpre 12928 |
. . . . . . . . 9
β’ (-π΄ β β+
β -π΄ β
β) |
84 | 83 | renegcld 11587 |
. . . . . . . 8
β’ (-π΄ β β+
β --π΄ β
β) |
85 | | negneg 11456 |
. . . . . . . . . 10
β’ (π΄ β β β --π΄ = π΄) |
86 | 85 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
--π΄ = π΄) |
87 | 86 | eleq1d 2819 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(--π΄ β β β
π΄ β
β)) |
88 | 84, 87 | imbitrid 243 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(-π΄ β
β+ β π΄ β β)) |
89 | | lognegb 25961 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β 0) β (-π΄ β β+
β (ββ(logβπ΄)) = Ο)) |
90 | 8, 89 | syldan 592 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(-π΄ β
β+ β (ββ(logβπ΄)) = Ο)) |
91 | | reim0b 15010 |
. . . . . . . 8
β’ (π΄ β β β (π΄ β β β
(ββπ΄) =
0)) |
92 | 91 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(π΄ β β β
(ββπ΄) =
0)) |
93 | 88, 90, 92 | 3imtr3d 293 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((ββ(logβπ΄)) = Ο β (ββπ΄) = 0)) |
94 | 93 | necon3d 2961 |
. . . . 5
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
((ββπ΄) β 0
β (ββ(logβπ΄)) β Ο)) |
95 | 3, 94 | mpd 15 |
. . . 4
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(logβπ΄)) β Ο) |
96 | 95 | necomd 2996 |
. . 3
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
Ο β (ββ(logβπ΄))) |
97 | 11, 55, 82, 96 | leneltd 11314 |
. 2
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(logβπ΄)) < Ο) |
98 | | 0xr 11207 |
. . 3
β’ 0 β
β* |
99 | 42 | rexri 11218 |
. . 3
β’ Ο
β β* |
100 | | elioo2 13311 |
. . 3
β’ ((0
β β* β§ Ο β β*) β
((ββ(logβπ΄)) β (0(,)Ο) β
((ββ(logβπ΄)) β β β§ 0 <
(ββ(logβπ΄)) β§ (ββ(logβπ΄)) < Ο))) |
101 | 98, 99, 100 | mp2an 691 |
. 2
β’
((ββ(logβπ΄)) β (0(,)Ο) β
((ββ(logβπ΄)) β β β§ 0 <
(ββ(logβπ΄)) β§ (ββ(logβπ΄)) < Ο)) |
102 | 11, 81, 97, 101 | syl3anbrc 1344 |
1
β’ ((π΄ β β β§ 0 <
(ββπ΄)) β
(ββ(logβπ΄)) β (0(,)Ο)) |