tanabsge

Description: The tangent function is greater than or equal to its argument in absolute value. (Contributed by Mario Carneiro, 25-Feb-2015)

		Ref	Expression
	Assertion	tanabsge	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to \|A\| \leq \|\tan A\|$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A \in ℝ$
2	1	adantr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to A \in ℝ$
3	2	renegcld	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - A \in ℝ$
4	1	lt0neg1d	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (A < 0 \leftrightarrow 0 < - A)$
5	4	biimpa	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to 0 < - A$
6		eliooord	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (- \frac{π}{2} < A \land A < \frac{π}{2})$
7	6	simpld	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to - \frac{π}{2} < A$
8	7	adantr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - \frac{π}{2} < A$
9		halfpire	$⊢ \frac{π}{2} \in ℝ$
10		ltnegcon1	$⊢ (\frac{π}{2} \in ℝ \land A \in ℝ) \to (- \frac{π}{2} < A \leftrightarrow - A < \frac{π}{2})$
11	9 2 10	sylancr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to (- \frac{π}{2} < A \leftrightarrow - A < \frac{π}{2})$
12	8 11	mpbid	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - A < \frac{π}{2}$
13		0xr	$⊢ 0 \in ℝ^{*}$
14	9	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
15		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (- A \in (0, \frac{π}{2}) \leftrightarrow (- A \in ℝ \land 0 < - A \land - A < \frac{π}{2}))$
16	13 14 15	mp2an	$⊢ - A \in (0, \frac{π}{2}) \leftrightarrow (- A \in ℝ \land 0 < - A \land - A < \frac{π}{2})$
17	3 5 12 16	syl3anbrc	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - A \in (0, \frac{π}{2})$
18		sincosq1sgn	$⊢ - A \in (0, \frac{π}{2}) \to (0 < \sin (- A) \land 0 < \cos (- A))$
19	17 18	syl	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to (0 < \sin (- A) \land 0 < \cos (- A))$
20	19	simprd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to 0 < \cos (- A)$
21	20	gt0ne0d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \cos (- A) \neq 0$
22	3 21	retancld	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \tan (- A) \in ℝ$
23		tangtx	$⊢ - A \in (0, \frac{π}{2}) \to - A < \tan (- A)$
24	17 23	syl	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - A < \tan (- A)$
25	3 22 24	ltled	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - A \leq \tan (- A)$
26		0re	$⊢ 0 \in ℝ$
27		ltle	$⊢ (A \in ℝ \land 0 \in ℝ) \to (A < 0 \to A \leq 0)$
28	1 26 27	sylancl	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (A < 0 \to A \leq 0)$
29	28	imp	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to A \leq 0$
30	2 29	absnidd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \|A\| = - A$
31	1	recnd	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A \in ℂ$
32	31	adantr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to A \in ℂ$
33	32	negnegd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - (- A) = A$
34	33	fveq2d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \tan (- (- A)) = \tan A$
35	32	negcld	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to - A \in ℂ$
36		tanneg	$⊢ (- A \in ℂ \land \cos (- A) \neq 0) \to \tan (- (- A)) = - \tan (- A)$
37	35 21 36	syl2anc	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \tan (- (- A)) = - \tan (- A)$
38	34 37	eqtr3d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \tan A = - \tan (- A)$
39	38	fveq2d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \|\tan A\| = \|- \tan (- A)\|$
40	22	recnd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \tan (- A) \in ℂ$
41	40	absnegd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \|- \tan (- A)\| = \|\tan (- A)\|$
42		0red	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to 0 \in ℝ$
43		ltle	$⊢ (0 \in ℝ \land - A \in ℝ) \to (0 < - A \to 0 \leq - A)$
44	26 3 43	sylancr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to (0 < - A \to 0 \leq - A)$
45	5 44	mpd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to 0 \leq - A$
46	42 3 22 45 25	letrd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to 0 \leq \tan (- A)$
47	22 46	absidd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \|\tan (- A)\| = \tan (- A)$
48	39 41 47	3eqtrd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \|\tan A\| = \tan (- A)$
49	25 30 48	3brtr4d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A < 0) \to \|A\| \leq \|\tan A\|$
50		abs0	$⊢ \|0\| = 0$
51	50 26	eqeltri	$⊢ \|0\| \in ℝ$
52	51	leidi	$⊢ \|0\| \leq \|0\|$
53	52	a1i	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to \|0\| \leq \|0\|$
54		simpr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to A = 0$
55	54	fveq2d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to \|A\| = \|0\|$
56	54	fveq2d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to \tan A = \tan 0$
57		tan0	$⊢ \tan 0 = 0$
58	56 57	eqtrdi	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to \tan A = 0$
59	58	fveq2d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to \|\tan A\| = \|0\|$
60	53 55 59	3brtr4d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land A = 0) \to \|A\| \leq \|\tan A\|$
61	1	adantr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to A \in ℝ$
62		simpr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to 0 < A$
63	6	simprd	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A < \frac{π}{2}$
64	63	adantr	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to A < \frac{π}{2}$
65		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (A \in (0, \frac{π}{2}) \leftrightarrow (A \in ℝ \land 0 < A \land A < \frac{π}{2}))$
66	13 14 65	mp2an	$⊢ A \in (0, \frac{π}{2}) \leftrightarrow (A \in ℝ \land 0 < A \land A < \frac{π}{2})$
67	61 62 64 66	syl3anbrc	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to A \in (0, \frac{π}{2})$
68		sincosq1sgn	$⊢ A \in (0, \frac{π}{2}) \to (0 < \sin A \land 0 < \cos A)$
69	67 68	syl	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to (0 < \sin A \land 0 < \cos A)$
70	69	simprd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to 0 < \cos A$
71	70	gt0ne0d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to \cos A \neq 0$
72	61 71	retancld	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to \tan A \in ℝ$
73		tangtx	$⊢ A \in (0, \frac{π}{2}) \to A < \tan A$
74	67 73	syl	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to A < \tan A$
75	61 72 74	ltled	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to A \leq \tan A$
76		ltle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \to 0 \leq A)$
77	26 1 76	sylancr	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (0 < A \to 0 \leq A)$
78	77	imp	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to 0 \leq A$
79	61 78	absidd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to \|A\| = A$
80		0red	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to 0 \in ℝ$
81	80 61 72 78 75	letrd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to 0 \leq \tan A$
82	72 81	absidd	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to \|\tan A\| = \tan A$
83	75 79 82	3brtr4d	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \land 0 < A) \to \|A\| \leq \|\tan A\|$
84		lttri4	$⊢ (A \in ℝ \land 0 \in ℝ) \to (A < 0 \lor A = 0 \lor 0 < A)$
85	1 26 84	sylancl	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (A < 0 \lor A = 0 \lor 0 < A)$
86	49 60 83 85	mpjao3dan	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to \|A\| \leq \|\tan A\|$

Metamath Proof Explorer

Theorem tanabsge

Proof