| 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 ‘ 𝐵 ) ) ) |