This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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