MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tanord1 Structured version   Visualization version   GIF version

Theorem tanord1 24403
Description: The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 24404.) (Contributed by Mario Carneiro, 29-Jul-2014.) Revised to replace an OLD theorem. (Revised by Wolf Lammen, 20-Sep-2020.)
Assertion
Ref Expression
tanord1 ((𝐴 ∈ (0[,)(π / 2)) ∧ 𝐵 ∈ (0[,)(π / 2))) → (𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵)))

Proof of Theorem tanord1
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1600 . 2
2 fveq2 6304 . . 3 (𝑥 = 𝑦 → (tan‘𝑥) = (tan‘𝑦))
3 fveq2 6304 . . 3 (𝑥 = 𝐴 → (tan‘𝑥) = (tan‘𝐴))
4 fveq2 6304 . . 3 (𝑥 = 𝐵 → (tan‘𝑥) = (tan‘𝐵))
5 0re 10153 . . . 4 0 ∈ ℝ
6 halfpire 24336 . . . . 5 (π / 2) ∈ ℝ
76rexri 10210 . . . 4 (π / 2) ∈ ℝ*
8 icossre 12368 . . . 4 ((0 ∈ ℝ ∧ (π / 2) ∈ ℝ*) → (0[,)(π / 2)) ⊆ ℝ)
95, 7, 8mp2an 710 . . 3 (0[,)(π / 2)) ⊆ ℝ
109sseli 3705 . . . . 5 (𝑥 ∈ (0[,)(π / 2)) → 𝑥 ∈ ℝ)
11 neghalfpirx 24338 . . . . . . . . 9 -(π / 2) ∈ ℝ*
12 pire 24330 . . . . . . . . . . 11 π ∈ ℝ
13 2re 11203 . . . . . . . . . . 11 2 ∈ ℝ
14 pipos 24332 . . . . . . . . . . 11 0 < π
15 2pos 11225 . . . . . . . . . . 11 0 < 2
1612, 13, 14, 15divgt0ii 11054 . . . . . . . . . 10 0 < (π / 2)
17 lt0neg2 10648 . . . . . . . . . . 11 ((π / 2) ∈ ℝ → (0 < (π / 2) ↔ -(π / 2) < 0))
186, 17ax-mp 5 . . . . . . . . . 10 (0 < (π / 2) ↔ -(π / 2) < 0)
1916, 18mpbi 220 . . . . . . . . 9 -(π / 2) < 0
20 df-ioo 12293 . . . . . . . . . 10 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
21 df-ico 12295 . . . . . . . . . 10 [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
22 xrltletr 12102 . . . . . . . . . 10 ((-(π / 2) ∈ ℝ* ∧ 0 ∈ ℝ*𝑤 ∈ ℝ*) → ((-(π / 2) < 0 ∧ 0 ≤ 𝑤) → -(π / 2) < 𝑤))
2320, 21, 22ixxss1 12307 . . . . . . . . 9 ((-(π / 2) ∈ ℝ* ∧ -(π / 2) < 0) → (0[,)(π / 2)) ⊆ (-(π / 2)(,)(π / 2)))
2411, 19, 23mp2an 710 . . . . . . . 8 (0[,)(π / 2)) ⊆ (-(π / 2)(,)(π / 2))
2524sseli 3705 . . . . . . 7 (𝑥 ∈ (0[,)(π / 2)) → 𝑥 ∈ (-(π / 2)(,)(π / 2)))
26 cosq14gt0 24382 . . . . . . 7 (𝑥 ∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘𝑥))
2725, 26syl 17 . . . . . 6 (𝑥 ∈ (0[,)(π / 2)) → 0 < (cos‘𝑥))
2827gt0ne0d 10705 . . . . 5 (𝑥 ∈ (0[,)(π / 2)) → (cos‘𝑥) ≠ 0)
2910, 28retancld 14995 . . . 4 (𝑥 ∈ (0[,)(π / 2)) → (tan‘𝑥) ∈ ℝ)
3029adantl 473 . . 3 ((⊤ ∧ 𝑥 ∈ (0[,)(π / 2))) → (tan‘𝑥) ∈ ℝ)
3110resincld 14993 . . . . . . . . 9 (𝑥 ∈ (0[,)(π / 2)) → (sin‘𝑥) ∈ ℝ)
3210recoscld 14994 . . . . . . . . 9 (𝑥 ∈ (0[,)(π / 2)) → (cos‘𝑥) ∈ ℝ)
3331, 32, 28redivcld 10966 . . . . . . . 8 (𝑥 ∈ (0[,)(π / 2)) → ((sin‘𝑥) / (cos‘𝑥)) ∈ ℝ)
34333ad2ant1 1125 . . . . . . 7 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑥) / (cos‘𝑥)) ∈ ℝ)
359sseli 3705 . . . . . . . . . 10 (𝑦 ∈ (0[,)(π / 2)) → 𝑦 ∈ ℝ)
36353ad2ant2 1126 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ)
3736resincld 14993 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (sin‘𝑦) ∈ ℝ)
38323ad2ant1 1125 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (cos‘𝑥) ∈ ℝ)
39283ad2ant1 1125 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (cos‘𝑥) ≠ 0)
4037, 38, 39redivcld 10966 . . . . . . 7 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑦) / (cos‘𝑥)) ∈ ℝ)
4136recoscld 14994 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (cos‘𝑦) ∈ ℝ)
4224sseli 3705 . . . . . . . . . . 11 (𝑦 ∈ (0[,)(π / 2)) → 𝑦 ∈ (-(π / 2)(,)(π / 2)))
43 cosq14gt0 24382 . . . . . . . . . . 11 (𝑦 ∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘𝑦))
4442, 43syl 17 . . . . . . . . . 10 (𝑦 ∈ (0[,)(π / 2)) → 0 < (cos‘𝑦))
4544gt0ne0d 10705 . . . . . . . . 9 (𝑦 ∈ (0[,)(π / 2)) → (cos‘𝑦) ≠ 0)
46453ad2ant2 1126 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (cos‘𝑦) ≠ 0)
4737, 41, 46redivcld 10966 . . . . . . 7 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑦) / (cos‘𝑦)) ∈ ℝ)
48 ioossicc 12373 . . . . . . . . . . . 12 (-(π / 2)(,)(π / 2)) ⊆ (-(π / 2)[,](π / 2))
4924, 48sstri 3718 . . . . . . . . . . 11 (0[,)(π / 2)) ⊆ (-(π / 2)[,](π / 2))
5049sseli 3705 . . . . . . . . . 10 (𝑥 ∈ (0[,)(π / 2)) → 𝑥 ∈ (-(π / 2)[,](π / 2)))
5149sseli 3705 . . . . . . . . . 10 (𝑦 ∈ (0[,)(π / 2)) → 𝑦 ∈ (-(π / 2)[,](π / 2)))
52 sinord 24400 . . . . . . . . . 10 ((𝑥 ∈ (-(π / 2)[,](π / 2)) ∧ 𝑦 ∈ (-(π / 2)[,](π / 2))) → (𝑥 < 𝑦 ↔ (sin‘𝑥) < (sin‘𝑦)))
5350, 51, 52syl2an 495 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2))) → (𝑥 < 𝑦 ↔ (sin‘𝑥) < (sin‘𝑦)))
5453biimp3a 1545 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (sin‘𝑥) < (sin‘𝑦))
55103ad2ant1 1125 . . . . . . . . . 10 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ)
5655resincld 14993 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (sin‘𝑥) ∈ ℝ)
57273ad2ant1 1125 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 0 < (cos‘𝑥))
58 ltdiv1 11000 . . . . . . . . 9 (((sin‘𝑥) ∈ ℝ ∧ (sin‘𝑦) ∈ ℝ ∧ ((cos‘𝑥) ∈ ℝ ∧ 0 < (cos‘𝑥))) → ((sin‘𝑥) < (sin‘𝑦) ↔ ((sin‘𝑥) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑥))))
5956, 37, 38, 57, 58syl112anc 1443 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑥) < (sin‘𝑦) ↔ ((sin‘𝑥) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑥))))
6054, 59mpbid 222 . . . . . . 7 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑥) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑥)))
6112rexri 10210 . . . . . . . . . . . 12 π ∈ ℝ*
62 pirp 24333 . . . . . . . . . . . . 13 π ∈ ℝ+
63 rphalflt 11974 . . . . . . . . . . . . 13 (π ∈ ℝ+ → (π / 2) < π)
6462, 63ax-mp 5 . . . . . . . . . . . 12 (π / 2) < π
65 df-icc 12296 . . . . . . . . . . . . 13 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
66 xrlttr 12087 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ* ∧ (π / 2) ∈ ℝ* ∧ π ∈ ℝ*) → ((𝑤 < (π / 2) ∧ (π / 2) < π) → 𝑤 < π))
67 xrltle 12096 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ* ∧ π ∈ ℝ*) → (𝑤 < π → 𝑤 ≤ π))
68673adant2 1123 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ* ∧ (π / 2) ∈ ℝ* ∧ π ∈ ℝ*) → (𝑤 < π → 𝑤 ≤ π))
6966, 68syld 47 . . . . . . . . . . . . 13 ((𝑤 ∈ ℝ* ∧ (π / 2) ∈ ℝ* ∧ π ∈ ℝ*) → ((𝑤 < (π / 2) ∧ (π / 2) < π) → 𝑤 ≤ π))
7065, 21, 69ixxss2 12308 . . . . . . . . . . . 12 ((π ∈ ℝ* ∧ (π / 2) < π) → (0[,)(π / 2)) ⊆ (0[,]π))
7161, 64, 70mp2an 710 . . . . . . . . . . 11 (0[,)(π / 2)) ⊆ (0[,]π)
7271sseli 3705 . . . . . . . . . 10 (𝑥 ∈ (0[,)(π / 2)) → 𝑥 ∈ (0[,]π))
7371sseli 3705 . . . . . . . . . 10 (𝑦 ∈ (0[,)(π / 2)) → 𝑦 ∈ (0[,]π))
74 cosord 24398 . . . . . . . . . 10 ((𝑥 ∈ (0[,]π) ∧ 𝑦 ∈ (0[,]π)) → (𝑥 < 𝑦 ↔ (cos‘𝑦) < (cos‘𝑥)))
7572, 73, 74syl2an 495 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2))) → (𝑥 < 𝑦 ↔ (cos‘𝑦) < (cos‘𝑥)))
7675biimp3a 1545 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (cos‘𝑦) < (cos‘𝑥))
77 0red 10154 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 0 ∈ ℝ)
78 simp1 1128 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (0[,)(π / 2)))
79 elico2 12351 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (π / 2) ∈ ℝ*) → (𝑥 ∈ (0[,)(π / 2)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 < (π / 2))))
805, 7, 79mp2an 710 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,)(π / 2)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 < (π / 2)))
8178, 80sylib 208 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 < (π / 2)))
8281simp2d 1135 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 0 ≤ 𝑥)
83 simp3 1130 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦)
8477, 55, 36, 82, 83lelttrd 10308 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 0 < 𝑦)
85 simp2 1129 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (0[,)(π / 2)))
86 elico2 12351 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ (π / 2) ∈ ℝ*) → (𝑦 ∈ (0[,)(π / 2)) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦𝑦 < (π / 2))))
875, 7, 86mp2an 710 . . . . . . . . . . . . . 14 (𝑦 ∈ (0[,)(π / 2)) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦𝑦 < (π / 2)))
8885, 87sylib 208 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦𝑦 < (π / 2)))
8988simp3d 1136 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑦 < (π / 2))
90 0xr 10199 . . . . . . . . . . . . 13 0 ∈ ℝ*
91 elioo2 12330 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → (𝑦 ∈ (0(,)(π / 2)) ↔ (𝑦 ∈ ℝ ∧ 0 < 𝑦𝑦 < (π / 2))))
9290, 7, 91mp2an 710 . . . . . . . . . . . 12 (𝑦 ∈ (0(,)(π / 2)) ↔ (𝑦 ∈ ℝ ∧ 0 < 𝑦𝑦 < (π / 2)))
9336, 84, 89, 92syl3anbrc 1383 . . . . . . . . . . 11 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (0(,)(π / 2)))
94 sincosq1sgn 24370 . . . . . . . . . . 11 (𝑦 ∈ (0(,)(π / 2)) → (0 < (sin‘𝑦) ∧ 0 < (cos‘𝑦)))
9593, 94syl 17 . . . . . . . . . 10 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (0 < (sin‘𝑦) ∧ 0 < (cos‘𝑦)))
9695simprd 482 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 0 < (cos‘𝑦))
9795simpld 477 . . . . . . . . 9 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 0 < (sin‘𝑦))
98 ltdiv2 11022 . . . . . . . . 9 ((((cos‘𝑦) ∈ ℝ ∧ 0 < (cos‘𝑦)) ∧ ((cos‘𝑥) ∈ ℝ ∧ 0 < (cos‘𝑥)) ∧ ((sin‘𝑦) ∈ ℝ ∧ 0 < (sin‘𝑦))) → ((cos‘𝑦) < (cos‘𝑥) ↔ ((sin‘𝑦) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑦))))
9941, 96, 38, 57, 37, 97, 98syl222anc 1455 . . . . . . . 8 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((cos‘𝑦) < (cos‘𝑥) ↔ ((sin‘𝑦) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑦))))
10076, 99mpbid 222 . . . . . . 7 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑦) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑦)))
10134, 40, 47, 60, 100lttrd 10311 . . . . . 6 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → ((sin‘𝑥) / (cos‘𝑥)) < ((sin‘𝑦) / (cos‘𝑦)))
10210recnd 10181 . . . . . . . 8 (𝑥 ∈ (0[,)(π / 2)) → 𝑥 ∈ ℂ)
103 tanval 14978 . . . . . . . 8 ((𝑥 ∈ ℂ ∧ (cos‘𝑥) ≠ 0) → (tan‘𝑥) = ((sin‘𝑥) / (cos‘𝑥)))
104102, 28, 103syl2anc 696 . . . . . . 7 (𝑥 ∈ (0[,)(π / 2)) → (tan‘𝑥) = ((sin‘𝑥) / (cos‘𝑥)))
1051043ad2ant1 1125 . . . . . 6 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (tan‘𝑥) = ((sin‘𝑥) / (cos‘𝑥)))
10635recnd 10181 . . . . . . . 8 (𝑦 ∈ (0[,)(π / 2)) → 𝑦 ∈ ℂ)
1071063ad2ant2 1126 . . . . . . 7 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℂ)
108 tanval 14978 . . . . . . 7 ((𝑦 ∈ ℂ ∧ (cos‘𝑦) ≠ 0) → (tan‘𝑦) = ((sin‘𝑦) / (cos‘𝑦)))
109107, 46, 108syl2anc 696 . . . . . 6 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (tan‘𝑦) = ((sin‘𝑦) / (cos‘𝑦)))
110101, 105, 1093brtr4d 4792 . . . . 5 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)) ∧ 𝑥 < 𝑦) → (tan‘𝑥) < (tan‘𝑦))
1111103expia 1114 . . . 4 ((𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2))) → (𝑥 < 𝑦 → (tan‘𝑥) < (tan‘𝑦)))
112111adantl 473 . . 3 ((⊤ ∧ (𝑥 ∈ (0[,)(π / 2)) ∧ 𝑦 ∈ (0[,)(π / 2)))) → (𝑥 < 𝑦 → (tan‘𝑥) < (tan‘𝑦)))
1132, 3, 4, 9, 30, 112ltord1 10667 . 2 ((⊤ ∧ (𝐴 ∈ (0[,)(π / 2)) ∧ 𝐵 ∈ (0[,)(π / 2)))) → (𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵)))
1141, 113mpan 708 1 ((𝐴 ∈ (0[,)(π / 2)) ∧ 𝐵 ∈ (0[,)(π / 2))) → (𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wtru 1597  wcel 2103  wne 2896  wss 3680   class class class wbr 4760  cfv 6001  (class class class)co 6765  cc 10047  cr 10048  0cc0 10049  *cxr 10186   < clt 10187  cle 10188  -cneg 10380   / cdiv 10797  2c2 11183  +crp 11946  (,)cioo 12289  [,)cico 12291  [,]cicc 12292  sincsin 14914  cosccos 14915  tanctan 14916  πcpi 14917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-inf2 8651  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127  ax-addf 10128  ax-mulf 10129
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-iin 4631  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-se 5178  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-isom 6010  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-of 7014  df-om 7183  df-1st 7285  df-2nd 7286  df-supp 7416  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-oadd 7684  df-er 7862  df-map 7976  df-pm 7977  df-ixp 8026  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-fsupp 8392  df-fi 8433  df-sup 8464  df-inf 8465  df-oi 8531  df-card 8878  df-cda 9103  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-q 11903  df-rp 11947  df-xneg 12060  df-xadd 12061  df-xmul 12062  df-ioo 12293  df-ioc 12294  df-ico 12295  df-icc 12296  df-fz 12441  df-fzo 12581  df-fl 12708  df-seq 12917  df-exp 12976  df-fac 13176  df-bc 13205  df-hash 13233  df-shft 13927  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-limsup 14322  df-clim 14339  df-rlim 14340  df-sum 14537  df-ef 14918  df-sin 14920  df-cos 14921  df-tan 14922  df-pi 14923  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-starv 16079  df-sca 16080  df-vsca 16081  df-ip 16082  df-tset 16083  df-ple 16084  df-ds 16087  df-unif 16088  df-hom 16089  df-cco 16090  df-rest 16206  df-topn 16207  df-0g 16225  df-gsum 16226  df-topgen 16227  df-pt 16228  df-prds 16231  df-xrs 16285  df-qtop 16290  df-imas 16291  df-xps 16293  df-mre 16369  df-mrc 16370  df-acs 16372  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-submnd 17458  df-mulg 17663  df-cntz 17871  df-cmn 18316  df-psmet 19861  df-xmet 19862  df-met 19863  df-bl 19864  df-mopn 19865  df-fbas 19866  df-fg 19867  df-cnfld 19870  df-top 20822  df-topon 20839  df-topsp 20860  df-bases 20873  df-cld 20946  df-ntr 20947  df-cls 20948  df-nei 21025  df-lp 21063  df-perf 21064  df-cn 21154  df-cnp 21155  df-haus 21242  df-tx 21488  df-hmeo 21681  df-fil 21772  df-fm 21864  df-flim 21865  df-flf 21866  df-xms 22247  df-ms 22248  df-tms 22249  df-cncf 22803  df-limc 23750  df-dv 23751
This theorem is referenced by:  tanord  24404
  Copyright terms: Public domain W3C validator