Metamath Proof Explorer

Theorem tanord1

Description: The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord .) (Contributed by Mario Carneiro, 29-Jul-2014) Revised to replace an OLD theorem. (Revised by Wolf Lammen, 20-Sep-2020)

Ref Expression
Assertion tanord1 ( ( 𝐴 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝐵 ∈ ( 0 [,) ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( tan ‘ 𝐴 ) < ( tan ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 tru ⊢ ⊤
2 fveq2 ⊢ ( 𝑥 = 𝑦 → ( tan ‘ 𝑥 ) = ( tan ‘ 𝑦 ) )
3 fveq2 ⊢ ( 𝑥 = 𝐴 → ( tan ‘ 𝑥 ) = ( tan ‘ 𝐴 ) )
4 fveq2 ⊢ ( 𝑥 = 𝐵 → ( tan ‘ 𝑥 ) = ( tan ‘ 𝐵 ) )
5 0re ⊢ 0 ∈ ℝ
6 halfpire ⊢ ( π / 2 ) ∈ ℝ
7 6 rexri ⊢ ( π / 2 ) ∈ ℝ*
8 icossre ⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( 0 [,) ( π / 2 ) ) ⊆ ℝ )
9 5 7 8 mp2an ⊢ ( 0 [,) ( π / 2 ) ) ⊆ ℝ
10 9 sseli ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → 𝑥 ∈ ℝ )
11 neghalfpirx ⊢ - ( π / 2 ) ∈ ℝ*
12 pire ⊢ π ∈ ℝ
13 2re ⊢ 2 ∈ ℝ
14 pipos ⊢ 0 < π
15 2pos ⊢ 0 < 2
16 12 13 14 15 divgt0ii ⊢ 0 < ( π / 2 )
17 lt0neg2 ⊢ ( ( π / 2 ) ∈ ℝ → ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 ) )
18 6 17 ax-mp ⊢ ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 )
19 16 18 mpbi ⊢ - ( π / 2 ) < 0
20 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
21 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
22 xrltletr ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( - ( π / 2 ) < 0 ∧ 0 ≤ 𝑤 ) → - ( π / 2 ) < 𝑤 ) )
23 20 21 22 ixxss1 ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ - ( π / 2 ) < 0 ) → ( 0 [,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) (,) ( π / 2 ) ) )
24 11 19 23 mp2an ⊢ ( 0 [,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) (,) ( π / 2 ) )
25 24 sseli ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
26 cosq14gt0 ⊢ ( 𝑥 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ 𝑥 ) )
27 25 26 syl ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → 0 < ( cos ‘ 𝑥 ) )
28 27 gt0ne0d ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → ( cos ‘ 𝑥 ) ≠ 0 )
29 10 28 retancld ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → ( tan ‘ 𝑥 ) ∈ ℝ )
30 29 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ) → ( tan ‘ 𝑥 ) ∈ ℝ )
31 10 resincld ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → ( sin ‘ 𝑥 ) ∈ ℝ )
32 10 recoscld ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → ( cos ‘ 𝑥 ) ∈ ℝ )
33 31 32 28 redivcld ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ∈ ℝ )
34 33 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ∈ ℝ )
35 9 sseli ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → 𝑦 ∈ ℝ )
36 35 3ad2ant2 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ )
37 36 resincld ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( sin ‘ 𝑦 ) ∈ ℝ )
38 32 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( cos ‘ 𝑥 ) ∈ ℝ )
39 28 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( cos ‘ 𝑥 ) ≠ 0 )
40 37 38 39 redivcld ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) ∈ ℝ )
41 36 recoscld ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( cos ‘ 𝑦 ) ∈ ℝ )
42 24 sseli ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
43 cosq14gt0 ⊢ ( 𝑦 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ 𝑦 ) )
44 42 43 syl ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → 0 < ( cos ‘ 𝑦 ) )
45 44 gt0ne0d ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → ( cos ‘ 𝑦 ) ≠ 0 )
46 45 3ad2ant2 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( cos ‘ 𝑦 ) ≠ 0 )
47 37 41 46 redivcld ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) ∈ ℝ )
48 ioossicc ⊢ ( - ( π / 2 ) (,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) [,] ( π / 2 ) )
49 24 48 sstri ⊢ ( 0 [,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) [,] ( π / 2 ) )
50 49 sseli ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
51 49 sseli ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → 𝑦 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
52 sinord ⊢ ( ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ∧ 𝑦 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( 𝑥 < 𝑦 ↔ ( sin ‘ 𝑥 ) < ( sin ‘ 𝑦 ) ) )
53 50 51 52 syl2an ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) → ( 𝑥 < 𝑦 ↔ ( sin ‘ 𝑥 ) < ( sin ‘ 𝑦 ) ) )
54 53 biimp3a ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( sin ‘ 𝑥 ) < ( sin ‘ 𝑦 ) )
55 10 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ )
56 55 resincld ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( sin ‘ 𝑥 ) ∈ ℝ )
57 27 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 < ( cos ‘ 𝑥 ) )
58 ltdiv1 ⊢ ( ( ( sin ‘ 𝑥 ) ∈ ℝ ∧ ( sin ‘ 𝑦 ) ∈ ℝ ∧ ( ( cos ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( cos ‘ 𝑥 ) ) ) → ( ( sin ‘ 𝑥 ) < ( sin ‘ 𝑦 ) ↔ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) ) )
59 56 37 38 57 58 syl112anc ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑥 ) < ( sin ‘ 𝑦 ) ↔ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) ) )
60 54 59 mpbid ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) )
61 12 rexri ⊢ π ∈ ℝ*
62 pirp ⊢ π ∈ ℝ+
63 rphalflt ⊢ ( π ∈ ℝ+ → ( π / 2 ) < π )
64 62 63 ax-mp ⊢ ( π / 2 ) < π
65 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
66 xrlttr ⊢ ( ( 𝑤 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( 𝑤 < ( π / 2 ) ∧ ( π / 2 ) < π ) → 𝑤 < π ) )
67 xrltle ⊢ ( ( 𝑤 ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝑤 < π → 𝑤 ≤ π ) )
68 67 3adant2 ⊢ ( ( 𝑤 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝑤 < π → 𝑤 ≤ π ) )
69 66 68 syld ⊢ ( ( 𝑤 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( 𝑤 < ( π / 2 ) ∧ ( π / 2 ) < π ) → 𝑤 ≤ π ) )
70 65 21 69 ixxss2 ⊢ ( ( π ∈ ℝ* ∧ ( π / 2 ) < π ) → ( 0 [,) ( π / 2 ) ) ⊆ ( 0 [,] π ) )
71 61 64 70 mp2an ⊢ ( 0 [,) ( π / 2 ) ) ⊆ ( 0 [,] π )
72 71 sseli ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → 𝑥 ∈ ( 0 [,] π ) )
73 71 sseli ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → 𝑦 ∈ ( 0 [,] π ) )
74 cosord ⊢ ( ( 𝑥 ∈ ( 0 [,] π ) ∧ 𝑦 ∈ ( 0 [,] π ) ) → ( 𝑥 < 𝑦 ↔ ( cos ‘ 𝑦 ) < ( cos ‘ 𝑥 ) ) )
75 72 73 74 syl2an ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) → ( 𝑥 < 𝑦 ↔ ( cos ‘ 𝑦 ) < ( cos ‘ 𝑥 ) ) )
76 75 biimp3a ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( cos ‘ 𝑦 ) < ( cos ‘ 𝑥 ) )
77 0red ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 ∈ ℝ )
78 simp1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 0 [,) ( π / 2 ) ) )
79 elico2 ⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < ( π / 2 ) ) ) )
80 5 7 79 mp2an ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < ( π / 2 ) ) )
81 78 80 sylib ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < ( π / 2 ) ) )
82 81 simp2d ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 ≤ 𝑥 )
83 simp3 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
84 77 55 36 82 83 lelttrd ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 < 𝑦 )
85 simp2 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 0 [,) ( π / 2 ) ) )
86 elico2 ⊢ ( ( 0 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) )
87 5 7 86 mp2an ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( π / 2 ) ) )
88 85 87 sylib ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( π / 2 ) ) )
89 88 simp3d ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 < ( π / 2 ) )
90 0xr ⊢ 0 ∈ ℝ*
91 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝑦 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ∧ 𝑦 < ( π / 2 ) ) ) )
92 90 7 91 mp2an ⊢ ( 𝑦 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ∧ 𝑦 < ( π / 2 ) ) )
93 36 84 89 92 syl3anbrc ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 0 (,) ( π / 2 ) ) )
94 sincosq1sgn ⊢ ( 𝑦 ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ 𝑦 ) ∧ 0 < ( cos ‘ 𝑦 ) ) )
95 93 94 syl ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( 0 < ( sin ‘ 𝑦 ) ∧ 0 < ( cos ‘ 𝑦 ) ) )
96 95 simprd ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 < ( cos ‘ 𝑦 ) )
97 95 simpld ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 0 < ( sin ‘ 𝑦 ) )
98 ltdiv2 ⊢ ( ( ( ( cos ‘ 𝑦 ) ∈ ℝ ∧ 0 < ( cos ‘ 𝑦 ) ) ∧ ( ( cos ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( cos ‘ 𝑥 ) ) ∧ ( ( sin ‘ 𝑦 ) ∈ ℝ ∧ 0 < ( sin ‘ 𝑦 ) ) ) → ( ( cos ‘ 𝑦 ) < ( cos ‘ 𝑥 ) ↔ ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) ) )
99 41 96 38 57 37 97 98 syl222anc ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( cos ‘ 𝑦 ) < ( cos ‘ 𝑥 ) ↔ ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) ) )
100 76 99 mpbid ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) )
101 34 40 47 60 100 lttrd ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) < ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) )
102 10 recnd ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → 𝑥 ∈ ℂ )
103 tanval ⊢ ( ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ≠ 0 ) → ( tan ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
104 102 28 103 syl2anc ⊢ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) → ( tan ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
105 104 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( tan ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
106 35 recnd ⊢ ( 𝑦 ∈ ( 0 [,) ( π / 2 ) ) → 𝑦 ∈ ℂ )
107 106 3ad2ant2 ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℂ )
108 tanval ⊢ ( ( 𝑦 ∈ ℂ ∧ ( cos ‘ 𝑦 ) ≠ 0 ) → ( tan ‘ 𝑦 ) = ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) )
109 107 46 108 syl2anc ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( tan ‘ 𝑦 ) = ( ( sin ‘ 𝑦 ) / ( cos ‘ 𝑦 ) ) )
110 101 105 109 3brtr4d ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑥 < 𝑦 ) → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) )
111 110 3expia ⊢ ( ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) → ( 𝑥 < 𝑦 → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) )
112 111 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝑦 ∈ ( 0 [,) ( π / 2 ) ) ) ) → ( 𝑥 < 𝑦 → ( tan ‘ 𝑥 ) < ( tan ‘ 𝑦 ) ) )
113 2 3 4 9 30 112 ltord1 ⊢ ( ( ⊤ ∧ ( 𝐴 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝐵 ∈ ( 0 [,) ( π / 2 ) ) ) ) → ( 𝐴 < 𝐵 ↔ ( tan ‘ 𝐴 ) < ( tan ‘ 𝐵 ) ) )
114 1 113 mpan ⊢ ( ( 𝐴 ∈ ( 0 [,) ( π / 2 ) ) ∧ 𝐵 ∈ ( 0 [,) ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( tan ‘ 𝐴 ) < ( tan ‘ 𝐵 ) ) )