Step |
Hyp |
Ref |
Expression |
1 |
|
tru |
⊢ ⊤ |
2 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( tan ‘ 𝑥 ) = ( tan ‘ 𝑦 ) ) |
3 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( tan ‘ 𝑥 ) = ( tan ‘ 𝐴 ) ) |
4 |
|
fveq2 |
⊢ ( 𝑥 = 𝐵 → ( tan ‘ 𝑥 ) = ( tan ‘ 𝐵 ) ) |
5 |
|
ioossre |
⊢ ( - ( π / 2 ) (,) ( π / 2 ) ) ⊆ ℝ |
6 |
|
elioore |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝑥 ∈ ℝ ) |
7 |
6
|
recnd |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝑥 ∈ ℂ ) |
8 |
6
|
rered |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝑥 ) = 𝑥 ) |
9 |
|
id |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
10 |
8 9
|
eqeltrd |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝑥 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
11 |
|
cosne0 |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℜ ‘ 𝑥 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝑥 ) ≠ 0 ) |
12 |
7 10 11
|
syl2anc |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( cos ‘ 𝑥 ) ≠ 0 ) |
13 |
6 12
|
retancld |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( tan ‘ 𝑥 ) ∈ ℝ ) |
14 |
13
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( tan ‘ 𝑥 ) ∈ ℝ ) |
15 |
6
|
3ad2ant1 |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ℝ ) |
17 |
16
|
recnd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ℂ ) |
18 |
17
|
negnegd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → - - 𝑥 = 𝑥 ) |
19 |
18
|
fveq2d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( tan ‘ - - 𝑥 ) = ( tan ‘ 𝑥 ) ) |
20 |
17
|
negcld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → - 𝑥 ∈ ℂ ) |
21 |
|
cosneg |
⊢ ( 𝑥 ∈ ℂ → ( cos ‘ - 𝑥 ) = ( cos ‘ 𝑥 ) ) |
22 |
17 21
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( cos ‘ - 𝑥 ) = ( cos ‘ 𝑥 ) ) |
23 |
|
simpl1 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
24 |
23 12
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( cos ‘ 𝑥 ) ≠ 0 ) |
25 |
22 24
|
eqnetrd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( cos ‘ - 𝑥 ) ≠ 0 ) |
26 |
|
tanneg |
⊢ ( ( - 𝑥 ∈ ℂ ∧ ( cos ‘ - 𝑥 ) ≠ 0 ) → ( tan ‘ - - 𝑥 ) = - ( tan ‘ - 𝑥 ) ) |
27 |
20 25 26
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( tan ‘ - - 𝑥 ) = - ( tan ‘ - 𝑥 ) ) |
28 |
19 27
|
eqtr3d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( tan ‘ 𝑥 ) = - ( tan ‘ - 𝑥 ) ) |
29 |
15
|
adantr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑥 ∈ ℝ ) |
30 |
29
|
renegcld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - 𝑥 ∈ ℝ ) |
31 |
25
|
adantrr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( cos ‘ - 𝑥 ) ≠ 0 ) |
32 |
30 31
|
retancld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( tan ‘ - 𝑥 ) ∈ ℝ ) |
33 |
32
|
renegcld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - ( tan ‘ - 𝑥 ) ∈ ℝ ) |
34 |
|
0red |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 0 ∈ ℝ ) |
35 |
|
simp2 |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
36 |
5 35
|
sselid |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ ) |
37 |
36
|
adantr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑦 ∈ ℝ ) |
38 |
|
simpl2 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
39 |
|
elioore |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝑦 ∈ ℝ ) |
40 |
39
|
recnd |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝑦 ∈ ℂ ) |
41 |
39
|
rered |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝑦 ) = 𝑦 ) |
42 |
|
id |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
43 |
41 42
|
eqeltrd |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝑦 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
44 |
|
cosne0 |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( ℜ ‘ 𝑦 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝑦 ) ≠ 0 ) |
45 |
40 43 44
|
syl2anc |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( cos ‘ 𝑦 ) ≠ 0 ) |
46 |
38 45
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( cos ‘ 𝑦 ) ≠ 0 ) |
47 |
37 46
|
retancld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( tan ‘ 𝑦 ) ∈ ℝ ) |
48 |
|
simprl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑥 < 0 ) |
49 |
29
|
lt0neg1d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( 𝑥 < 0 ↔ 0 < - 𝑥 ) ) |
50 |
48 49
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 0 < - 𝑥 ) |
51 |
|
simpl1 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
52 |
|
eliooord |
⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) |
53 |
51 52
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( - ( π / 2 ) < 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) |
54 |
53
|
simpld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - ( π / 2 ) < 𝑥 ) |
55 |
|
halfpire |
⊢ ( π / 2 ) ∈ ℝ |
56 |
|
ltnegcon1 |
⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( - ( π / 2 ) < 𝑥 ↔ - 𝑥 < ( π / 2 ) ) ) |
57 |
55 29 56
|
sylancr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( - ( π / 2 ) < 𝑥 ↔ - 𝑥 < ( π / 2 ) ) ) |
58 |
54 57
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - 𝑥 < ( π / 2 ) ) |
59 |
|
0xr |
⊢ 0 ∈ ℝ* |
60 |
55
|
rexri |
⊢ ( π / 2 ) ∈ ℝ* |
61 |
|
elioo2 |
⊢ ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( - 𝑥 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( - 𝑥 ∈ ℝ ∧ 0 < - 𝑥 ∧ - 𝑥 < ( π / 2 ) ) ) ) |
62 |
59 60 61
|
mp2an |
⊢ ( - 𝑥 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( - 𝑥 ∈ ℝ ∧ 0 < - 𝑥 ∧ - 𝑥 < ( π / 2 ) ) ) |
63 |
30 50 58 62
|
syl3anbrc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - 𝑥 ∈ ( 0 (,) ( π / 2 ) ) ) |
64 |
|
tanrpcl |
⊢ ( - 𝑥 ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ - 𝑥 ) ∈ ℝ+ ) |
65 |
63 64
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( tan ‘ - 𝑥 ) ∈ ℝ+ ) |
66 |
65
|
rpgt0d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 0 < ( tan ‘ - 𝑥 ) ) |
67 |
32
|
lt0neg2d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( 0 < ( tan ‘ - 𝑥 ) ↔ - ( tan ‘ - 𝑥 ) < 0 ) ) |
68 |
66 67
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - ( tan ‘ - 𝑥 ) < 0 ) |
69 |
|
simprr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 0 < 𝑦 ) |
70 |
|
eliooord |
⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) |
71 |
38 70
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( - ( π / 2 ) < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) |
72 |
71
|
simprd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑦 < ( π / 2 ) ) |
73 |
|
elioo2 |
⊢ ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝑦 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) ) |
74 |
59 60 73
|
mp2an |
⊢ ( 𝑦 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) |
75 |
37 69 72 74
|
syl3anbrc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 𝑦 ∈ ( 0 (,) ( π / 2 ) ) ) |
76 |
|
tanrpcl |
⊢ ( 𝑦 ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ 𝑦 ) ∈ ℝ+ ) |
77 |
75 76
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → ( tan ‘ 𝑦 ) ∈ ℝ+ ) |
78 |
77
|
rpgt0d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → 0 < ( tan ‘ 𝑦 ) ) |
79 |
33 34 47 68 78
|
lttrd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ ( 𝑥 < 0 ∧ 0 < 𝑦 ) ) → - ( tan ‘ - 𝑥 ) < ( tan ‘ 𝑦 ) ) |
80 |
79
|
anassrs |
⊢ ( ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) ∧ 0 < 𝑦 ) → - ( tan ‘ - 𝑥 ) < ( tan ‘ 𝑦 ) ) |
81 |
|
simpl3 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑥 < 𝑦 ) |
82 |
15
|
adantr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑥 ∈ ℝ ) |
83 |
36
|
adantr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑦 ∈ ℝ ) |
84 |
82 83
|
ltnegd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( 𝑥 < 𝑦 ↔ - 𝑦 < - 𝑥 ) ) |
85 |
81 84
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑦 < - 𝑥 ) |
86 |
83
|
renegcld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑦 ∈ ℝ ) |
87 |
|
simpr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑦 ≤ 0 ) |
88 |
83
|
le0neg1d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( 𝑦 ≤ 0 ↔ 0 ≤ - 𝑦 ) ) |
89 |
87 88
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 0 ≤ - 𝑦 ) |
90 |
|
simpl2 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
91 |
90 70
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( - ( π / 2 ) < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) |
92 |
91
|
simpld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - ( π / 2 ) < 𝑦 ) |
93 |
|
ltnegcon1 |
⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( - ( π / 2 ) < 𝑦 ↔ - 𝑦 < ( π / 2 ) ) ) |
94 |
55 83 93
|
sylancr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( - ( π / 2 ) < 𝑦 ↔ - 𝑦 < ( π / 2 ) ) ) |
95 |
92 94
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑦 < ( π / 2 ) ) |
96 |
|
0re |
⊢ 0 ∈ ℝ |
97 |
|
elico2 |
⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( - 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( - 𝑦 ∈ ℝ ∧ 0 ≤ - 𝑦 ∧ - 𝑦 < ( π / 2 ) ) ) ) |
98 |
96 60 97
|
mp2an |
⊢ ( - 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( - 𝑦 ∈ ℝ ∧ 0 ≤ - 𝑦 ∧ - 𝑦 < ( π / 2 ) ) ) |
99 |
86 89 95 98
|
syl3anbrc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) |
100 |
82
|
renegcld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑥 ∈ ℝ ) |
101 |
|
simp3 |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 ) |
102 |
|
0red |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 ∈ ℝ ) |
103 |
|
ltletr |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑥 < 𝑦 ∧ 𝑦 ≤ 0 ) → 𝑥 < 0 ) ) |
104 |
15 36 102 103
|
syl3anc |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑥 < 𝑦 ∧ 𝑦 ≤ 0 ) → 𝑥 < 0 ) ) |
105 |
101 104
|
mpand |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 ≤ 0 → 𝑥 < 0 ) ) |
106 |
105
|
imp |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑥 < 0 ) |
107 |
|
ltle |
⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑥 < 0 → 𝑥 ≤ 0 ) ) |
108 |
82 96 107
|
sylancl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( 𝑥 < 0 → 𝑥 ≤ 0 ) ) |
109 |
106 108
|
mpd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑥 ≤ 0 ) |
110 |
82
|
le0neg1d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( 𝑥 ≤ 0 ↔ 0 ≤ - 𝑥 ) ) |
111 |
109 110
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 0 ≤ - 𝑥 ) |
112 |
|
simpl1 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
113 |
112 52
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( - ( π / 2 ) < 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) |
114 |
113
|
simpld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - ( π / 2 ) < 𝑥 ) |
115 |
55 82 56
|
sylancr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( - ( π / 2 ) < 𝑥 ↔ - 𝑥 < ( π / 2 ) ) ) |
116 |
114 115
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑥 < ( π / 2 ) ) |
117 |
|
elico2 |
⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( - 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( - 𝑥 ∈ ℝ ∧ 0 ≤ - 𝑥 ∧ - 𝑥 < ( π / 2 ) ) ) ) |
118 |
96 60 117
|
mp2an |
⊢ ( - 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( - 𝑥 ∈ ℝ ∧ 0 ≤ - 𝑥 ∧ - 𝑥 < ( π / 2 ) ) ) |
119 |
100 111 116 118
|
syl3anbrc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ) |
120 |
|
tanord1 |
⊢ ( ( - 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ - 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ) → ( - 𝑦 < - 𝑥 ↔ ( tan ‘ - 𝑦 ) < ( tan ‘ - 𝑥 ) ) ) |
121 |
99 119 120
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( - 𝑦 < - 𝑥 ↔ ( tan ‘ - 𝑦 ) < ( tan ‘ - 𝑥 ) ) ) |
122 |
85 121
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( tan ‘ - 𝑦 ) < ( tan ‘ - 𝑥 ) ) |
123 |
83
|
recnd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → 𝑦 ∈ ℂ ) |
124 |
|
cosneg |
⊢ ( 𝑦 ∈ ℂ → ( cos ‘ - 𝑦 ) = ( cos ‘ 𝑦 ) ) |
125 |
123 124
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( cos ‘ - 𝑦 ) = ( cos ‘ 𝑦 ) ) |
126 |
90 45
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( cos ‘ 𝑦 ) ≠ 0 ) |
127 |
125 126
|
eqnetrd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( cos ‘ - 𝑦 ) ≠ 0 ) |
128 |
86 127
|
retancld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( tan ‘ - 𝑦 ) ∈ ℝ ) |
129 |
106 25
|
syldan |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( cos ‘ - 𝑥 ) ≠ 0 ) |
130 |
100 129
|
retancld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( tan ‘ - 𝑥 ) ∈ ℝ ) |
131 |
128 130
|
ltnegd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( ( tan ‘ - 𝑦 ) < ( tan ‘ - 𝑥 ) ↔ - ( tan ‘ - 𝑥 ) < - ( tan ‘ - 𝑦 ) ) ) |
132 |
122 131
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - ( tan ‘ - 𝑥 ) < - ( tan ‘ - 𝑦 ) ) |
133 |
123
|
negnegd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - - 𝑦 = 𝑦 ) |
134 |
133
|
fveq2d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( tan ‘ - - 𝑦 ) = ( tan ‘ 𝑦 ) ) |
135 |
123
|
negcld |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - 𝑦 ∈ ℂ ) |
136 |
|
tanneg |
⊢ ( ( - 𝑦 ∈ ℂ ∧ ( cos ‘ - 𝑦 ) ≠ 0 ) → ( tan ‘ - - 𝑦 ) = - ( tan ‘ - 𝑦 ) ) |
137 |
135 127 136
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( tan ‘ - - 𝑦 ) = - ( tan ‘ - 𝑦 ) ) |
138 |
134 137
|
eqtr3d |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → ( tan ‘ 𝑦 ) = - ( tan ‘ - 𝑦 ) ) |
139 |
132 138
|
breqtrrd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑦 ≤ 0 ) → - ( tan ‘ - 𝑥 ) < ( tan ‘ 𝑦 ) ) |
140 |
139
|
adantlr |
⊢ ( ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) ∧ 𝑦 ≤ 0 ) → - ( tan ‘ - 𝑥 ) < ( tan ‘ 𝑦 ) ) |
141 |
|
0red |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → 0 ∈ ℝ ) |
142 |
|
simpl2 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
143 |
5 142
|
sselid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → 𝑦 ∈ ℝ ) |
144 |
80 140 141 143
|
ltlecasei |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → - ( tan ‘ - 𝑥 ) < ( tan ‘ 𝑦 ) ) |
145 |
28 144
|
eqbrtrd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑥 < 0 ) → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) |
146 |
|
simpl3 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑥 < 𝑦 ) |
147 |
15
|
adantr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ℝ ) |
148 |
|
simpr |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 0 ≤ 𝑥 ) |
149 |
|
simpl1 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
150 |
149 52
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → ( - ( π / 2 ) < 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) |
151 |
150
|
simprd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑥 < ( π / 2 ) ) |
152 |
|
elico2 |
⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) ) |
153 |
96 60 152
|
mp2an |
⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) |
154 |
147 148 151 153
|
syl3anbrc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ) |
155 |
|
simpl2 |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
156 |
5 155
|
sselid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑦 ∈ ℝ ) |
157 |
|
0red |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 0 ∈ ℝ ) |
158 |
147 156 146
|
ltled |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑥 ≤ 𝑦 ) |
159 |
157 147 156 148 158
|
letrd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 0 ≤ 𝑦 ) |
160 |
155 70
|
syl |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → ( - ( π / 2 ) < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) |
161 |
160
|
simprd |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑦 < ( π / 2 ) ) |
162 |
|
elico2 |
⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) ) |
163 |
96 60 162
|
mp2an |
⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) |
164 |
156 159 161 163
|
syl3anbrc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) |
165 |
|
tanord1 |
⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) → ( 𝑥 < 𝑦 ↔ ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) ) |
166 |
154 164 165
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → ( 𝑥 < 𝑦 ↔ ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) ) |
167 |
146 166
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) ∧ 0 ≤ 𝑥 ) → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) |
168 |
145 167 15 102
|
ltlecasei |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) |
169 |
168
|
3expia |
⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 𝑥 < 𝑦 → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) ) |
170 |
169
|
adantl |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ) → ( 𝑥 < 𝑦 → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) ) |
171 |
2 3 4 5 14 170
|
ltord1 |
⊢ ( ( ⊤ ∧ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ) → ( 𝐴 < 𝐵 ↔ ( tan ‘ 𝐴 ) < ( tan ‘ 𝐵 ) ) ) |
172 |
1 171
|
mpan |
⊢ ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( tan ‘ 𝐴 ) < ( tan ‘ 𝐵 ) ) ) |