Step |
Hyp |
Ref |
Expression |
1 |
|
elioore |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. RR ) |
2 |
1
|
adantr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> A e. RR ) |
3 |
2
|
renegcld |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u A e. RR ) |
4 |
1
|
lt0neg1d |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( A < 0 <-> 0 < -u A ) ) |
5 |
4
|
biimpa |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> 0 < -u A ) |
6 |
|
eliooord |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( -u ( _pi / 2 ) < A /\ A < ( _pi / 2 ) ) ) |
7 |
6
|
simpld |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> -u ( _pi / 2 ) < A ) |
8 |
7
|
adantr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u ( _pi / 2 ) < A ) |
9 |
|
halfpire |
|- ( _pi / 2 ) e. RR |
10 |
|
ltnegcon1 |
|- ( ( ( _pi / 2 ) e. RR /\ A e. RR ) -> ( -u ( _pi / 2 ) < A <-> -u A < ( _pi / 2 ) ) ) |
11 |
9 2 10
|
sylancr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( -u ( _pi / 2 ) < A <-> -u A < ( _pi / 2 ) ) ) |
12 |
8 11
|
mpbid |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u A < ( _pi / 2 ) ) |
13 |
|
0xr |
|- 0 e. RR* |
14 |
9
|
rexri |
|- ( _pi / 2 ) e. RR* |
15 |
|
elioo2 |
|- ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( -u A e. ( 0 (,) ( _pi / 2 ) ) <-> ( -u A e. RR /\ 0 < -u A /\ -u A < ( _pi / 2 ) ) ) ) |
16 |
13 14 15
|
mp2an |
|- ( -u A e. ( 0 (,) ( _pi / 2 ) ) <-> ( -u A e. RR /\ 0 < -u A /\ -u A < ( _pi / 2 ) ) ) |
17 |
3 5 12 16
|
syl3anbrc |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u A e. ( 0 (,) ( _pi / 2 ) ) ) |
18 |
|
sincosq1sgn |
|- ( -u A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` -u A ) /\ 0 < ( cos ` -u A ) ) ) |
19 |
17 18
|
syl |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( 0 < ( sin ` -u A ) /\ 0 < ( cos ` -u A ) ) ) |
20 |
19
|
simprd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> 0 < ( cos ` -u A ) ) |
21 |
20
|
gt0ne0d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( cos ` -u A ) =/= 0 ) |
22 |
3 21
|
retancld |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( tan ` -u A ) e. RR ) |
23 |
|
tangtx |
|- ( -u A e. ( 0 (,) ( _pi / 2 ) ) -> -u A < ( tan ` -u A ) ) |
24 |
17 23
|
syl |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u A < ( tan ` -u A ) ) |
25 |
3 22 24
|
ltled |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u A <_ ( tan ` -u A ) ) |
26 |
|
0re |
|- 0 e. RR |
27 |
|
ltle |
|- ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 -> A <_ 0 ) ) |
28 |
1 26 27
|
sylancl |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( A < 0 -> A <_ 0 ) ) |
29 |
28
|
imp |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> A <_ 0 ) |
30 |
2 29
|
absnidd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( abs ` A ) = -u A ) |
31 |
1
|
recnd |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. CC ) |
32 |
31
|
adantr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> A e. CC ) |
33 |
32
|
negnegd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u -u A = A ) |
34 |
33
|
fveq2d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( tan ` -u -u A ) = ( tan ` A ) ) |
35 |
32
|
negcld |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> -u A e. CC ) |
36 |
|
tanneg |
|- ( ( -u A e. CC /\ ( cos ` -u A ) =/= 0 ) -> ( tan ` -u -u A ) = -u ( tan ` -u A ) ) |
37 |
35 21 36
|
syl2anc |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( tan ` -u -u A ) = -u ( tan ` -u A ) ) |
38 |
34 37
|
eqtr3d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( tan ` A ) = -u ( tan ` -u A ) ) |
39 |
38
|
fveq2d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( abs ` ( tan ` A ) ) = ( abs ` -u ( tan ` -u A ) ) ) |
40 |
22
|
recnd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( tan ` -u A ) e. CC ) |
41 |
40
|
absnegd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( abs ` -u ( tan ` -u A ) ) = ( abs ` ( tan ` -u A ) ) ) |
42 |
|
0red |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> 0 e. RR ) |
43 |
|
ltle |
|- ( ( 0 e. RR /\ -u A e. RR ) -> ( 0 < -u A -> 0 <_ -u A ) ) |
44 |
26 3 43
|
sylancr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( 0 < -u A -> 0 <_ -u A ) ) |
45 |
5 44
|
mpd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> 0 <_ -u A ) |
46 |
42 3 22 45 25
|
letrd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> 0 <_ ( tan ` -u A ) ) |
47 |
22 46
|
absidd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( abs ` ( tan ` -u A ) ) = ( tan ` -u A ) ) |
48 |
39 41 47
|
3eqtrd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( abs ` ( tan ` A ) ) = ( tan ` -u A ) ) |
49 |
25 30 48
|
3brtr4d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A < 0 ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) ) |
50 |
|
abs0 |
|- ( abs ` 0 ) = 0 |
51 |
50 26
|
eqeltri |
|- ( abs ` 0 ) e. RR |
52 |
51
|
leidi |
|- ( abs ` 0 ) <_ ( abs ` 0 ) |
53 |
52
|
a1i |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> ( abs ` 0 ) <_ ( abs ` 0 ) ) |
54 |
|
simpr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> A = 0 ) |
55 |
54
|
fveq2d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> ( abs ` A ) = ( abs ` 0 ) ) |
56 |
54
|
fveq2d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> ( tan ` A ) = ( tan ` 0 ) ) |
57 |
|
tan0 |
|- ( tan ` 0 ) = 0 |
58 |
56 57
|
eqtrdi |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> ( tan ` A ) = 0 ) |
59 |
58
|
fveq2d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> ( abs ` ( tan ` A ) ) = ( abs ` 0 ) ) |
60 |
53 55 59
|
3brtr4d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ A = 0 ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) ) |
61 |
1
|
adantr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> A e. RR ) |
62 |
|
simpr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> 0 < A ) |
63 |
6
|
simprd |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A < ( _pi / 2 ) ) |
64 |
63
|
adantr |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> A < ( _pi / 2 ) ) |
65 |
|
elioo2 |
|- ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( A e. ( 0 (,) ( _pi / 2 ) ) <-> ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) ) ) |
66 |
13 14 65
|
mp2an |
|- ( A e. ( 0 (,) ( _pi / 2 ) ) <-> ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) ) |
67 |
61 62 64 66
|
syl3anbrc |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> A e. ( 0 (,) ( _pi / 2 ) ) ) |
68 |
|
sincosq1sgn |
|- ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) ) |
69 |
67 68
|
syl |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) ) |
70 |
69
|
simprd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> 0 < ( cos ` A ) ) |
71 |
70
|
gt0ne0d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> ( cos ` A ) =/= 0 ) |
72 |
61 71
|
retancld |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> ( tan ` A ) e. RR ) |
73 |
|
tangtx |
|- ( A e. ( 0 (,) ( _pi / 2 ) ) -> A < ( tan ` A ) ) |
74 |
67 73
|
syl |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> A < ( tan ` A ) ) |
75 |
61 72 74
|
ltled |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> A <_ ( tan ` A ) ) |
76 |
|
ltle |
|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) ) |
77 |
26 1 76
|
sylancr |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( 0 < A -> 0 <_ A ) ) |
78 |
77
|
imp |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> 0 <_ A ) |
79 |
61 78
|
absidd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> ( abs ` A ) = A ) |
80 |
|
0red |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> 0 e. RR ) |
81 |
80 61 72 78 75
|
letrd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> 0 <_ ( tan ` A ) ) |
82 |
72 81
|
absidd |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> ( abs ` ( tan ` A ) ) = ( tan ` A ) ) |
83 |
75 79 82
|
3brtr4d |
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ 0 < A ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) ) |
84 |
|
lttri4 |
|- ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 \/ A = 0 \/ 0 < A ) ) |
85 |
1 26 84
|
sylancl |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( A < 0 \/ A = 0 \/ 0 < A ) ) |
86 |
49 60 83 85
|
mpjao3dan |
|- ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) ) |