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