Step | Hyp | Ref
| Expression |
1 | | tru 1546 |
. 2
⊢
⊤ |
2 | | fveq2 6674 |
. . 3
⊢ (𝑥 = 𝑦 → (tan‘𝑥) = (tan‘𝑦)) |
3 | | fveq2 6674 |
. . 3
⊢ (𝑥 = 𝐴 → (tan‘𝑥) = (tan‘𝐴)) |
4 | | fveq2 6674 |
. . 3
⊢ (𝑥 = 𝐵 → (tan‘𝑥) = (tan‘𝐵)) |
5 | | ioossre 12882 |
. . 3
⊢ (-(π /
2)(,)(π / 2)) ⊆ ℝ |
6 | | elioore 12851 |
. . . . 5
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → 𝑥 ∈
ℝ) |
7 | 6 | recnd 10747 |
. . . . . 6
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → 𝑥 ∈
ℂ) |
8 | 6 | rered 14673 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → (ℜ‘𝑥)
= 𝑥) |
9 | | id 22 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → 𝑥 ∈ (-(π
/ 2)(,)(π / 2))) |
10 | 8, 9 | eqeltrd 2833 |
. . . . . 6
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → (ℜ‘𝑥)
∈ (-(π / 2)(,)(π / 2))) |
11 | | cosne0 25273 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧
(ℜ‘𝑥) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝑥) ≠ 0) |
12 | 7, 10, 11 | syl2anc 587 |
. . . . 5
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → (cos‘𝑥)
≠ 0) |
13 | 6, 12 | retancld 15590 |
. . . 4
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → (tan‘𝑥)
∈ ℝ) |
14 | 13 | adantl 485 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (-(π / 2)(,)(π / 2))) → (tan‘𝑥) ∈ ℝ) |
15 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → 𝑥 ∈
ℝ) |
16 | 15 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → 𝑥 ∈
ℝ) |
17 | 16 | recnd 10747 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → 𝑥 ∈
ℂ) |
18 | 17 | negnegd 11066 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → --𝑥 = 𝑥) |
19 | 18 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) →
(tan‘--𝑥) =
(tan‘𝑥)) |
20 | 17 | negcld 11062 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → -𝑥 ∈
ℂ) |
21 | | cosneg 15592 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ →
(cos‘-𝑥) =
(cos‘𝑥)) |
22 | 17, 21 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) →
(cos‘-𝑥) =
(cos‘𝑥)) |
23 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → 𝑥 ∈ (-(π / 2)(,)(π /
2))) |
24 | 23, 12 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → (cos‘𝑥) ≠ 0) |
25 | 22, 24 | eqnetrd 3001 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) →
(cos‘-𝑥) ≠
0) |
26 | | tanneg 15593 |
. . . . . . . . 9
⊢ ((-𝑥 ∈ ℂ ∧
(cos‘-𝑥) ≠ 0)
→ (tan‘--𝑥) =
-(tan‘-𝑥)) |
27 | 20, 25, 26 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) →
(tan‘--𝑥) =
-(tan‘-𝑥)) |
28 | 19, 27 | eqtr3d 2775 |
. . . . . . 7
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → (tan‘𝑥) = -(tan‘-𝑥)) |
29 | 15 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑥 ∈ ℝ) |
30 | 29 | renegcld 11145 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -𝑥 ∈ ℝ) |
31 | 25 | adantrr 717 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (cos‘-𝑥) ≠ 0) |
32 | 30, 31 | retancld 15590 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (tan‘-𝑥) ∈
ℝ) |
33 | 32 | renegcld 11145 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -(tan‘-𝑥) ∈
ℝ) |
34 | | 0red 10722 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 0 ∈
ℝ) |
35 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → 𝑦 ∈ (-(π / 2)(,)(π /
2))) |
36 | 5, 35 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → 𝑦 ∈
ℝ) |
37 | 36 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑦 ∈ ℝ) |
38 | | simpl2 1193 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑦 ∈ (-(π / 2)(,)(π /
2))) |
39 | | elioore 12851 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → 𝑦 ∈
ℝ) |
40 | 39 | recnd 10747 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → 𝑦 ∈
ℂ) |
41 | 39 | rered 14673 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → (ℜ‘𝑦)
= 𝑦) |
42 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → 𝑦 ∈ (-(π
/ 2)(,)(π / 2))) |
43 | 41, 42 | eqeltrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → (ℜ‘𝑦)
∈ (-(π / 2)(,)(π / 2))) |
44 | | cosne0 25273 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧
(ℜ‘𝑦) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝑦) ≠ 0) |
45 | 40, 43, 44 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → (cos‘𝑦)
≠ 0) |
46 | 38, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (cos‘𝑦) ≠ 0) |
47 | 37, 46 | retancld 15590 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (tan‘𝑦) ∈
ℝ) |
48 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑥 < 0) |
49 | 29 | lt0neg1d 11287 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (𝑥 < 0 ↔ 0 < -𝑥)) |
50 | 48, 49 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 0 < -𝑥) |
51 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑥 ∈ (-(π / 2)(,)(π /
2))) |
52 | | eliooord 12880 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-(π / 2)(,)(π /
2)) → (-(π / 2) < 𝑥 ∧ 𝑥 < (π / 2))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (-(π / 2) <
𝑥 ∧ 𝑥 < (π / 2))) |
54 | 53 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -(π / 2) < 𝑥) |
55 | | halfpire 25209 |
. . . . . . . . . . . . . . . 16
⊢ (π /
2) ∈ ℝ |
56 | | ltnegcon1 11219 |
. . . . . . . . . . . . . . . 16
⊢ (((π /
2) ∈ ℝ ∧ 𝑥
∈ ℝ) → (-(π / 2) < 𝑥 ↔ -𝑥 < (π / 2))) |
57 | 55, 29, 56 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (-(π / 2) <
𝑥 ↔ -𝑥 < (π /
2))) |
58 | 54, 57 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -𝑥 < (π / 2)) |
59 | | 0xr 10766 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ* |
60 | 55 | rexri 10777 |
. . . . . . . . . . . . . . 15
⊢ (π /
2) ∈ ℝ* |
61 | | elioo2 12862 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
(-𝑥 ∈ (0(,)(π / 2))
↔ (-𝑥 ∈ ℝ
∧ 0 < -𝑥 ∧
-𝑥 < (π /
2)))) |
62 | 59, 60, 61 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (-𝑥 ∈ (0(,)(π / 2)) ↔
(-𝑥 ∈ ℝ ∧ 0
< -𝑥 ∧ -𝑥 < (π /
2))) |
63 | 30, 50, 58, 62 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -𝑥 ∈ (0(,)(π / 2))) |
64 | | tanrpcl 25249 |
. . . . . . . . . . . . 13
⊢ (-𝑥 ∈ (0(,)(π / 2)) →
(tan‘-𝑥) ∈
ℝ+) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (tan‘-𝑥) ∈
ℝ+) |
66 | 65 | rpgt0d 12517 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 0 <
(tan‘-𝑥)) |
67 | 32 | lt0neg2d 11288 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (0 <
(tan‘-𝑥) ↔
-(tan‘-𝑥) <
0)) |
68 | 66, 67 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -(tan‘-𝑥) < 0) |
69 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 0 < 𝑦) |
70 | | eliooord 12880 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (-(π / 2)(,)(π /
2)) → (-(π / 2) < 𝑦 ∧ 𝑦 < (π / 2))) |
71 | 38, 70 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (-(π / 2) <
𝑦 ∧ 𝑦 < (π / 2))) |
72 | 71 | simprd 499 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑦 < (π / 2)) |
73 | | elioo2 12862 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
(𝑦 ∈ (0(,)(π / 2))
↔ (𝑦 ∈ ℝ
∧ 0 < 𝑦 ∧ 𝑦 < (π /
2)))) |
74 | 59, 60, 73 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(,)(π / 2)) ↔
(𝑦 ∈ ℝ ∧ 0
< 𝑦 ∧ 𝑦 < (π /
2))) |
75 | 37, 69, 72, 74 | syl3anbrc 1344 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 𝑦 ∈ (0(,)(π / 2))) |
76 | | tanrpcl 25249 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(,)(π / 2)) →
(tan‘𝑦) ∈
ℝ+) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → (tan‘𝑦) ∈
ℝ+) |
78 | 77 | rpgt0d 12517 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → 0 <
(tan‘𝑦)) |
79 | 33, 34, 47, 68, 78 | lttrd 10879 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ (𝑥 < 0 ∧ 0 < 𝑦)) → -(tan‘-𝑥) < (tan‘𝑦)) |
80 | 79 | anassrs 471 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) ∧ 0 < 𝑦) → -(tan‘-𝑥) < (tan‘𝑦)) |
81 | | simpl3 1194 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑥 < 𝑦) |
82 | 15 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑥 ∈
ℝ) |
83 | 36 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑦 ∈
ℝ) |
84 | 82, 83 | ltnegd 11296 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (𝑥 < 𝑦 ↔ -𝑦 < -𝑥)) |
85 | 81, 84 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑦 < -𝑥) |
86 | 83 | renegcld 11145 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑦 ∈
ℝ) |
87 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑦 ≤ 0) |
88 | 83 | le0neg1d 11289 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦)) |
89 | 87, 88 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 0 ≤ -𝑦) |
90 | | simpl2 1193 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑦 ∈ (-(π / 2)(,)(π /
2))) |
91 | 90, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (-(π / 2)
< 𝑦 ∧ 𝑦 < (π /
2))) |
92 | 91 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -(π / 2) <
𝑦) |
93 | | ltnegcon1 11219 |
. . . . . . . . . . . . . . . 16
⊢ (((π /
2) ∈ ℝ ∧ 𝑦
∈ ℝ) → (-(π / 2) < 𝑦 ↔ -𝑦 < (π / 2))) |
94 | 55, 83, 93 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (-(π / 2)
< 𝑦 ↔ -𝑦 < (π /
2))) |
95 | 92, 94 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑦 < (π /
2)) |
96 | | 0re 10721 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
97 | | elico2 12885 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (π / 2) ∈ ℝ*) → (-𝑦 ∈ (0[,)(π / 2)) ↔
(-𝑦 ∈ ℝ ∧ 0
≤ -𝑦 ∧ -𝑦 < (π /
2)))) |
98 | 96, 60, 97 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (-𝑦 ∈ (0[,)(π / 2)) ↔
(-𝑦 ∈ ℝ ∧ 0
≤ -𝑦 ∧ -𝑦 < (π /
2))) |
99 | 86, 89, 95, 98 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑦 ∈ (0[,)(π /
2))) |
100 | 82 | renegcld 11145 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑥 ∈
ℝ) |
101 | | simp3 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → 𝑥 < 𝑦) |
102 | | 0red 10722 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → 0 ∈
ℝ) |
103 | | ltletr 10810 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → ((𝑥 <
𝑦 ∧ 𝑦 ≤ 0) → 𝑥 < 0)) |
104 | 15, 36, 102, 103 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → ((𝑥 < 𝑦 ∧ 𝑦 ≤ 0) → 𝑥 < 0)) |
105 | 101, 104 | mpand 695 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) → (𝑦 ≤ 0 → 𝑥 < 0)) |
106 | 105 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑥 < 0) |
107 | | ltle 10807 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑥 < 0
→ 𝑥 ≤
0)) |
108 | 82, 96, 107 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (𝑥 < 0 → 𝑥 ≤ 0)) |
109 | 106, 108 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑥 ≤ 0) |
110 | 82 | le0neg1d 11289 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (𝑥 ≤ 0 ↔ 0 ≤ -𝑥)) |
111 | 109, 110 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 0 ≤ -𝑥) |
112 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑥 ∈ (-(π / 2)(,)(π /
2))) |
113 | 112, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (-(π / 2)
< 𝑥 ∧ 𝑥 < (π /
2))) |
114 | 113 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -(π / 2) <
𝑥) |
115 | 55, 82, 56 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (-(π / 2)
< 𝑥 ↔ -𝑥 < (π /
2))) |
116 | 114, 115 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑥 < (π /
2)) |
117 | | elico2 12885 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (π / 2) ∈ ℝ*) → (-𝑥 ∈ (0[,)(π / 2)) ↔
(-𝑥 ∈ ℝ ∧ 0
≤ -𝑥 ∧ -𝑥 < (π /
2)))) |
118 | 96, 60, 117 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (-𝑥 ∈ (0[,)(π / 2)) ↔
(-𝑥 ∈ ℝ ∧ 0
≤ -𝑥 ∧ -𝑥 < (π /
2))) |
119 | 100, 111,
116, 118 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑥 ∈ (0[,)(π /
2))) |
120 | | tanord1 25281 |
. . . . . . . . . . . . 13
⊢ ((-𝑦 ∈ (0[,)(π / 2)) ∧
-𝑥 ∈ (0[,)(π / 2)))
→ (-𝑦 < -𝑥 ↔ (tan‘-𝑦) < (tan‘-𝑥))) |
121 | 99, 119, 120 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (-𝑦 < -𝑥 ↔ (tan‘-𝑦) < (tan‘-𝑥))) |
122 | 85, 121 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(tan‘-𝑦) <
(tan‘-𝑥)) |
123 | 83 | recnd 10747 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → 𝑦 ∈
ℂ) |
124 | | cosneg 15592 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ →
(cos‘-𝑦) =
(cos‘𝑦)) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(cos‘-𝑦) =
(cos‘𝑦)) |
126 | 90, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (cos‘𝑦) ≠ 0) |
127 | 125, 126 | eqnetrd 3001 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(cos‘-𝑦) ≠
0) |
128 | 86, 127 | retancld 15590 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(tan‘-𝑦) ∈
ℝ) |
129 | 106, 25 | syldan 594 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(cos‘-𝑥) ≠
0) |
130 | 100, 129 | retancld 15590 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(tan‘-𝑥) ∈
ℝ) |
131 | 128, 130 | ltnegd 11296 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
((tan‘-𝑦) <
(tan‘-𝑥) ↔
-(tan‘-𝑥) <
-(tan‘-𝑦))) |
132 | 122, 131 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
-(tan‘-𝑥) <
-(tan‘-𝑦)) |
133 | 123 | negnegd 11066 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → --𝑦 = 𝑦) |
134 | 133 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(tan‘--𝑦) =
(tan‘𝑦)) |
135 | 123 | negcld 11062 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → -𝑦 ∈
ℂ) |
136 | | tanneg 15593 |
. . . . . . . . . . . 12
⊢ ((-𝑦 ∈ ℂ ∧
(cos‘-𝑦) ≠ 0)
→ (tan‘--𝑦) =
-(tan‘-𝑦)) |
137 | 135, 127,
136 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
(tan‘--𝑦) =
-(tan‘-𝑦)) |
138 | 134, 137 | eqtr3d 2775 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) → (tan‘𝑦) = -(tan‘-𝑦)) |
139 | 132, 138 | breqtrrd 5058 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑦 ≤ 0) →
-(tan‘-𝑥) <
(tan‘𝑦)) |
140 | 139 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) ∧ 𝑦 ≤ 0) →
-(tan‘-𝑥) <
(tan‘𝑦)) |
141 | | 0red 10722 |
. . . . . . . 8
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → 0 ∈
ℝ) |
142 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → 𝑦 ∈ (-(π / 2)(,)(π /
2))) |
143 | 5, 142 | sseldi 3875 |
. . . . . . . 8
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → 𝑦 ∈
ℝ) |
144 | 80, 140, 141, 143 | ltlecasei 10826 |
. . . . . . 7
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) →
-(tan‘-𝑥) <
(tan‘𝑦)) |
145 | 28, 144 | eqbrtrd 5052 |
. . . . . 6
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 𝑥 < 0) → (tan‘𝑥) < (tan‘𝑦)) |
146 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑥 < 𝑦) |
147 | 15 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ) |
148 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 0 ≤ 𝑥) |
149 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑥 ∈ (-(π / 2)(,)(π /
2))) |
150 | 149, 52 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → (-(π / 2) < 𝑥 ∧ 𝑥 < (π / 2))) |
151 | 150 | simprd 499 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑥 < (π / 2)) |
152 | | elico2 12885 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (π / 2) ∈ ℝ*) → (𝑥 ∈ (0[,)(π / 2)) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 < (π /
2)))) |
153 | 96, 60, 152 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,)(π / 2)) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 < (π /
2))) |
154 | 147, 148,
151, 153 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑥 ∈ (0[,)(π / 2))) |
155 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑦 ∈ (-(π / 2)(,)(π /
2))) |
156 | 5, 155 | sseldi 3875 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑦 ∈ ℝ) |
157 | | 0red 10722 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 0 ∈
ℝ) |
158 | 147, 156,
146 | ltled 10866 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑥 ≤ 𝑦) |
159 | 157, 147,
156, 148, 158 | letrd 10875 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 0 ≤ 𝑦) |
160 | 155, 70 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → (-(π / 2) < 𝑦 ∧ 𝑦 < (π / 2))) |
161 | 160 | simprd 499 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑦 < (π / 2)) |
162 | | elico2 12885 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (π / 2) ∈ ℝ*) → (𝑦 ∈ (0[,)(π / 2)) ↔
(𝑦 ∈ ℝ ∧ 0
≤ 𝑦 ∧ 𝑦 < (π /
2)))) |
163 | 96, 60, 162 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,)(π / 2)) ↔
(𝑦 ∈ ℝ ∧ 0
≤ 𝑦 ∧ 𝑦 < (π /
2))) |
164 | 156, 159,
161, 163 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → 𝑦 ∈ (0[,)(π / 2))) |
165 | | tanord1 25281 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,)(π / 2)) ∧
𝑦 ∈ (0[,)(π / 2)))
→ (𝑥 < 𝑦 ↔ (tan‘𝑥) < (tan‘𝑦))) |
166 | 154, 164,
165 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → (𝑥 < 𝑦 ↔ (tan‘𝑥) < (tan‘𝑦))) |
167 | 146, 166 | mpbid 235 |
. . . . . 6
⊢ (((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) ∧ 0 ≤ 𝑥) → (tan‘𝑥) < (tan‘𝑦)) |
168 | 145, 167,
15, 102 | ltlecasei 10826 |
. . . . 5
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2)) ∧ 𝑥
< 𝑦) →
(tan‘𝑥) <
(tan‘𝑦)) |
169 | 168 | 3expia 1122 |
. . . 4
⊢ ((𝑥 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝑦 ∈ (-(π
/ 2)(,)(π / 2))) → (𝑥 < 𝑦 → (tan‘𝑥) < (tan‘𝑦))) |
170 | 169 | adantl 485 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ (-(π / 2)(,)(π / 2)) ∧ 𝑦 ∈ (-(π / 2)(,)(π / 2)))) →
(𝑥 < 𝑦 → (tan‘𝑥) < (tan‘𝑦))) |
171 | 2, 3, 4, 5, 14, 170 | ltord1 11244 |
. 2
⊢
((⊤ ∧ (𝐴
∈ (-(π / 2)(,)(π / 2)) ∧ 𝐵 ∈ (-(π / 2)(,)(π / 2)))) →
(𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵))) |
172 | 1, 171 | mpan 690 |
1
⊢ ((𝐴 ∈ (-(π / 2)(,)(π /
2)) ∧ 𝐵 ∈ (-(π
/ 2)(,)(π / 2))) → (𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵))) |