Metamath Proof Explorer


Theorem tanord

Description: The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion tanord ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( tan ‘ 𝐴 ) < ( tan ‘ 𝐵 ) ) )

Proof

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