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

Metamath Proof Explorer

Theorem tanord1

Proof