tanord

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

		Ref	Expression
	Assertion	tanord	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land B \in (- \frac{π}{2}, \frac{π}{2})) \to (A < B \leftrightarrow \tan A < \tan B)$

Proof

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2		fveq2	$⊢ x = y \to \tan x = \tan y$
3		fveq2	$⊢ x = A \to \tan x = \tan A$
4		fveq2	$⊢ x = B \to \tan x = \tan B$
5		ioossre	$⊢ (- \frac{π}{2}, \frac{π}{2}) \subseteq ℝ$
6		elioore	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to x \in ℝ$
7	6	recnd	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to x \in ℂ$
8	6	rered	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to ℜ (x) = x$
9		id	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to x \in (- \frac{π}{2}, \frac{π}{2})$
10	8 9	eqeltrd	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to ℜ (x) \in (- \frac{π}{2}, \frac{π}{2})$
11		cosne0	$⊢ (x \in ℂ \land ℜ (x) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos x \neq 0$
12	7 10 11	syl2anc	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to \cos x \neq 0$
13	6 12	retancld	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to \tan x \in ℝ$
14	13	adantl	$⊢ (⊤ \land x \in (- \frac{π}{2}, \frac{π}{2})) \to \tan x \in ℝ$
15	6	3ad2ant1	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to x \in ℝ$
16	15	adantr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to x \in ℝ$
17	16	recnd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to x \in ℂ$
18	17	negnegd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to - (- x) = x$
19	18	fveq2d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \tan (- (- x)) = \tan x$
20	17	negcld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to - x \in ℂ$
21		cosneg	$⊢ x \in ℂ \to \cos (- x) = \cos x$
22	17 21	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \cos (- x) = \cos x$
23		simpl1	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to x \in (- \frac{π}{2}, \frac{π}{2})$
24	23 12	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \cos x \neq 0$
25	22 24	eqnetrd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \cos (- x) \neq 0$
26		tanneg	$⊢ (- x \in ℂ \land \cos (- x) \neq 0) \to \tan (- (- x)) = - \tan (- x)$
27	20 25 26	syl2anc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \tan (- (- x)) = - \tan (- x)$
28	19 27	eqtr3d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \tan x = - \tan (- x)$
29	15	adantr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to x \in ℝ$
30	29	renegcld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - x \in ℝ$
31	25	adantrr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to \cos (- x) \neq 0$
32	30 31	retancld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to \tan (- x) \in ℝ$
33	32	renegcld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - \tan (- x) \in ℝ$
34		0red	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to 0 \in ℝ$
35		simp2	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to y \in (- \frac{π}{2}, \frac{π}{2})$
36	5 35	sselid	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to y \in ℝ$
37	36	adantr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to y \in ℝ$
38		simpl2	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to y \in (- \frac{π}{2}, \frac{π}{2})$
39		elioore	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to y \in ℝ$
40	39	recnd	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to y \in ℂ$
41	39	rered	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to ℜ (y) = y$
42		id	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to y \in (- \frac{π}{2}, \frac{π}{2})$
43	41 42	eqeltrd	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to ℜ (y) \in (- \frac{π}{2}, \frac{π}{2})$
44		cosne0	$⊢ (y \in ℂ \land ℜ (y) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos y \neq 0$
45	40 43 44	syl2anc	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to \cos y \neq 0$
46	38 45	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to \cos y \neq 0$
47	37 46	retancld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to \tan y \in ℝ$
48		simprl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to x < 0$
49	29	lt0neg1d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to (x < 0 \leftrightarrow 0 < - x)$
50	48 49	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to 0 < - x$
51		simpl1	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to x \in (- \frac{π}{2}, \frac{π}{2})$
52		eliooord	$⊢ x \in (- \frac{π}{2}, \frac{π}{2}) \to (- \frac{π}{2} < x \land x < \frac{π}{2})$
53	51 52	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to (- \frac{π}{2} < x \land x < \frac{π}{2})$
54	53	simpld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - \frac{π}{2} < x$
55		halfpire	$⊢ \frac{π}{2} \in ℝ$
56		ltnegcon1	$⊢ (\frac{π}{2} \in ℝ \land x \in ℝ) \to (- \frac{π}{2} < x \leftrightarrow - x < \frac{π}{2})$
57	55 29 56	sylancr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to (- \frac{π}{2} < x \leftrightarrow - x < \frac{π}{2})$
58	54 57	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - x < \frac{π}{2}$
59		0xr	$⊢ 0 \in ℝ^{*}$
60	55	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
61		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (- x \in (0, \frac{π}{2}) \leftrightarrow (- x \in ℝ \land 0 < - x \land - x < \frac{π}{2}))$
62	59 60 61	mp2an	$⊢ - x \in (0, \frac{π}{2}) \leftrightarrow (- x \in ℝ \land 0 < - x \land - x < \frac{π}{2})$
63	30 50 58 62	syl3anbrc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - x \in (0, \frac{π}{2})$
64		tanrpcl	$⊢ - x \in (0, \frac{π}{2}) \to \tan (- x) \in ℝ^{+}$
65	63 64	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to \tan (- x) \in ℝ^{+}$
66	65	rpgt0d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to 0 < \tan (- x)$
67	32	lt0neg2d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to (0 < \tan (- x) \leftrightarrow - \tan (- x) < 0)$
68	66 67	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - \tan (- x) < 0$
69		simprr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to 0 < y$
70		eliooord	$⊢ y \in (- \frac{π}{2}, \frac{π}{2}) \to (- \frac{π}{2} < y \land y < \frac{π}{2})$
71	38 70	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to (- \frac{π}{2} < y \land y < \frac{π}{2})$
72	71	simprd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to y < \frac{π}{2}$
73		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (y \in (0, \frac{π}{2}) \leftrightarrow (y \in ℝ \land 0 < y \land y < \frac{π}{2}))$
74	59 60 73	mp2an	$⊢ y \in (0, \frac{π}{2}) \leftrightarrow (y \in ℝ \land 0 < y \land y < \frac{π}{2})$
75	37 69 72 74	syl3anbrc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to y \in (0, \frac{π}{2})$
76		tanrpcl	$⊢ y \in (0, \frac{π}{2}) \to \tan y \in ℝ^{+}$
77	75 76	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to \tan y \in ℝ^{+}$
78	77	rpgt0d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to 0 < \tan y$
79	33 34 47 68 78	lttrd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land (x < 0 \land 0 < y)) \to - \tan (- x) < \tan y$
80	79	anassrs	$⊢ (((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \land 0 < y) \to - \tan (- x) < \tan y$
81		simpl3	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to x < y$
82	15	adantr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to x \in ℝ$
83	36	adantr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to y \in ℝ$
84	82 83	ltnegd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (x < y \leftrightarrow - y < - x)$
85	81 84	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - y < - x$
86	83	renegcld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - y \in ℝ$
87		simpr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to y \leq 0$
88	83	le0neg1d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (y \leq 0 \leftrightarrow 0 \leq - y)$
89	87 88	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to 0 \leq - y$
90		simpl2	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to y \in (- \frac{π}{2}, \frac{π}{2})$
91	90 70	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (- \frac{π}{2} < y \land y < \frac{π}{2})$
92	91	simpld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - \frac{π}{2} < y$
93		ltnegcon1	$⊢ (\frac{π}{2} \in ℝ \land y \in ℝ) \to (- \frac{π}{2} < y \leftrightarrow - y < \frac{π}{2})$
94	55 83 93	sylancr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (- \frac{π}{2} < y \leftrightarrow - y < \frac{π}{2})$
95	92 94	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - y < \frac{π}{2}$
96		0re	$⊢ 0 \in ℝ$
97		elico2	$⊢ (0 \in ℝ \land \frac{π}{2} \in ℝ^{*}) \to (- y \in [0, \frac{π}{2}) \leftrightarrow (- y \in ℝ \land 0 \leq - y \land - y < \frac{π}{2}))$
98	96 60 97	mp2an	$⊢ - y \in [0, \frac{π}{2}) \leftrightarrow (- y \in ℝ \land 0 \leq - y \land - y < \frac{π}{2})$
99	86 89 95 98	syl3anbrc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - y \in [0, \frac{π}{2})$
100	82	renegcld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - x \in ℝ$
101		simp3	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to x < y$
102		0red	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to 0 \in ℝ$
103		ltletr	$⊢ (x \in ℝ \land y \in ℝ \land 0 \in ℝ) \to ((x < y \land y \leq 0) \to x < 0)$
104	15 36 102 103	syl3anc	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to ((x < y \land y \leq 0) \to x < 0)$
105	101 104	mpand	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to (y \leq 0 \to x < 0)$
106	105	imp	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to x < 0$
107		ltle	$⊢ (x \in ℝ \land 0 \in ℝ) \to (x < 0 \to x \leq 0)$
108	82 96 107	sylancl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (x < 0 \to x \leq 0)$
109	106 108	mpd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to x \leq 0$
110	82	le0neg1d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (x \leq 0 \leftrightarrow 0 \leq - x)$
111	109 110	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to 0 \leq - x$
112		simpl1	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to x \in (- \frac{π}{2}, \frac{π}{2})$
113	112 52	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (- \frac{π}{2} < x \land x < \frac{π}{2})$
114	113	simpld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - \frac{π}{2} < x$
115	55 82 56	sylancr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (- \frac{π}{2} < x \leftrightarrow - x < \frac{π}{2})$
116	114 115	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - x < \frac{π}{2}$
117		elico2	$⊢ (0 \in ℝ \land \frac{π}{2} \in ℝ^{*}) \to (- x \in [0, \frac{π}{2}) \leftrightarrow (- x \in ℝ \land 0 \leq - x \land - x < \frac{π}{2}))$
118	96 60 117	mp2an	$⊢ - x \in [0, \frac{π}{2}) \leftrightarrow (- x \in ℝ \land 0 \leq - x \land - x < \frac{π}{2})$
119	100 111 116 118	syl3anbrc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - x \in [0, \frac{π}{2})$
120		tanord1	$⊢ (- y \in [0, \frac{π}{2}) \land - x \in [0, \frac{π}{2})) \to (- y < - x \leftrightarrow \tan (- y) < \tan (- x))$
121	99 119 120	syl2anc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (- y < - x \leftrightarrow \tan (- y) < \tan (- x))$
122	85 121	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \tan (- y) < \tan (- x)$
123	83	recnd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to y \in ℂ$
124		cosneg	$⊢ y \in ℂ \to \cos (- y) = \cos y$
125	123 124	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \cos (- y) = \cos y$
126	90 45	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \cos y \neq 0$
127	125 126	eqnetrd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \cos (- y) \neq 0$
128	86 127	retancld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \tan (- y) \in ℝ$
129	106 25	syldan	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \cos (- x) \neq 0$
130	100 129	retancld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \tan (- x) \in ℝ$
131	128 130	ltnegd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to (\tan (- y) < \tan (- x) \leftrightarrow - \tan (- x) < - \tan (- y))$
132	122 131	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - \tan (- x) < - \tan (- y)$
133	123	negnegd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - (- y) = y$
134	133	fveq2d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \tan (- (- y)) = \tan y$
135	123	negcld	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - y \in ℂ$
136		tanneg	$⊢ (- y \in ℂ \land \cos (- y) \neq 0) \to \tan (- (- y)) = - \tan (- y)$
137	135 127 136	syl2anc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \tan (- (- y)) = - \tan (- y)$
138	134 137	eqtr3d	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to \tan y = - \tan (- y)$
139	132 138	breqtrrd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land y \leq 0) \to - \tan (- x) < \tan y$
140	139	adantlr	$⊢ (((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \land y \leq 0) \to - \tan (- x) < \tan y$
141		0red	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to 0 \in ℝ$
142		simpl2	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to y \in (- \frac{π}{2}, \frac{π}{2})$
143	5 142	sselid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to y \in ℝ$
144	80 140 141 143	ltlecasei	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to - \tan (- x) < \tan y$
145	28 144	eqbrtrd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land x < 0) \to \tan x < \tan y$
146		simpl3	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to x < y$
147	15	adantr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to x \in ℝ$
148		simpr	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to 0 \leq x$
149		simpl1	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to x \in (- \frac{π}{2}, \frac{π}{2})$
150	149 52	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to (- \frac{π}{2} < x \land x < \frac{π}{2})$
151	150	simprd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to x < \frac{π}{2}$
152		elico2	$⊢ (0 \in ℝ \land \frac{π}{2} \in ℝ^{*}) \to (x \in [0, \frac{π}{2}) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < \frac{π}{2}))$
153	96 60 152	mp2an	$⊢ x \in [0, \frac{π}{2}) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < \frac{π}{2})$
154	147 148 151 153	syl3anbrc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to x \in [0, \frac{π}{2})$
155		simpl2	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to y \in (- \frac{π}{2}, \frac{π}{2})$
156	5 155	sselid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to y \in ℝ$
157		0red	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to 0 \in ℝ$
158	147 156 146	ltled	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to x \leq y$
159	157 147 156 148 158	letrd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to 0 \leq y$
160	155 70	syl	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to (- \frac{π}{2} < y \land y < \frac{π}{2})$
161	160	simprd	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to y < \frac{π}{2}$
162		elico2	$⊢ (0 \in ℝ \land \frac{π}{2} \in ℝ^{*}) \to (y \in [0, \frac{π}{2}) \leftrightarrow (y \in ℝ \land 0 \leq y \land y < \frac{π}{2}))$
163	96 60 162	mp2an	$⊢ y \in [0, \frac{π}{2}) \leftrightarrow (y \in ℝ \land 0 \leq y \land y < \frac{π}{2})$
164	156 159 161 163	syl3anbrc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to y \in [0, \frac{π}{2})$
165		tanord1	$⊢ (x \in [0, \frac{π}{2}) \land y \in [0, \frac{π}{2})) \to (x < y \leftrightarrow \tan x < \tan y)$
166	154 164 165	syl2anc	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to (x < y \leftrightarrow \tan x < \tan y)$
167	146 166	mpbid	$⊢ ((x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \land 0 \leq x) \to \tan x < \tan y$
168	145 167 15 102	ltlecasei	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}) \land x < y) \to \tan x < \tan y$
169	168	3expia	$⊢ (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2})) \to (x < y \to \tan x < \tan y)$
170	169	adantl	$⊢ (⊤ \land (x \in (- \frac{π}{2}, \frac{π}{2}) \land y \in (- \frac{π}{2}, \frac{π}{2}))) \to (x < y \to \tan x < \tan y)$
171	2 3 4 5 14 170	ltord1	$⊢ (⊤ \land (A \in (- \frac{π}{2}, \frac{π}{2}) \land B \in (- \frac{π}{2}, \frac{π}{2}))) \to (A < B \leftrightarrow \tan A < \tan B)$
172	1 171	mpan	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land B \in (- \frac{π}{2}, \frac{π}{2})) \to (A < B \leftrightarrow \tan A < \tan B)$

Metamath Proof Explorer

Theorem tanord

Proof