atanbnd

Description: The arctangent function is bounded by _pi / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015)

		Ref	Expression
	Assertion	atanbnd	$⊢ A \in ℝ \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$

Proof

Step	Hyp	Ref	Expression
1		atanre	$⊢ A \in ℝ \to A \in dom arctan$
2	1	adantr	$⊢ (A \in ℝ \land A < 0) \to A \in dom arctan$
3		atanneg	$⊢ A \in dom arctan \to arctan (- A) = - arctan (A)$
4	2 3	syl	$⊢ (A \in ℝ \land A < 0) \to arctan (- A) = - arctan (A)$
5		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
6	5	adantr	$⊢ (A \in ℝ \land A < 0) \to - A \in ℝ$
7		lt0neg1	$⊢ A \in ℝ \to (A < 0 \leftrightarrow 0 < - A)$
8	7	biimpa	$⊢ (A \in ℝ \land A < 0) \to 0 < - A$
9	6 8	elrpd	$⊢ (A \in ℝ \land A < 0) \to - A \in ℝ^{+}$
10		atanbndlem	$⊢ - A \in ℝ^{+} \to arctan (- A) \in (- \frac{π}{2}, \frac{π}{2})$
11	9 10	syl	$⊢ (A \in ℝ \land A < 0) \to arctan (- A) \in (- \frac{π}{2}, \frac{π}{2})$
12	4 11	eqeltrrd	$⊢ (A \in ℝ \land A < 0) \to - arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$
13		halfpire	$⊢ \frac{π}{2} \in ℝ$
14	13	recni	$⊢ \frac{π}{2} \in ℂ$
15	14	negnegi	$⊢ - (- \frac{π}{2}) = \frac{π}{2}$
16	15	oveq2i	$⊢ (- \frac{π}{2}, - (- \frac{π}{2})) = (- \frac{π}{2}, \frac{π}{2})$
17	12 16	eleqtrrdi	$⊢ (A \in ℝ \land A < 0) \to - arctan (A) \in (- \frac{π}{2}, - (- \frac{π}{2}))$
18		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
19		atanrecl	$⊢ A \in ℝ \to arctan (A) \in ℝ$
20	19	adantr	$⊢ (A \in ℝ \land A < 0) \to arctan (A) \in ℝ$
21		iooneg	$⊢ (- \frac{π}{2} \in ℝ \land \frac{π}{2} \in ℝ \land arctan (A) \in ℝ) \to (arctan (A) \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow - arctan (A) \in (- \frac{π}{2}, - (- \frac{π}{2})))$
22	18 13 20 21	mp3an12i	$⊢ (A \in ℝ \land A < 0) \to (arctan (A) \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow - arctan (A) \in (- \frac{π}{2}, - (- \frac{π}{2})))$
23	17 22	mpbird	$⊢ (A \in ℝ \land A < 0) \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$
24		simpr	$⊢ (A \in ℝ \land A = 0) \to A = 0$
25	24	fveq2d	$⊢ (A \in ℝ \land A = 0) \to arctan (A) = arctan (0)$
26		atan0	$⊢ arctan (0) = 0$
27	25 26	syl6eq	$⊢ (A \in ℝ \land A = 0) \to arctan (A) = 0$
28		0re	$⊢ 0 \in ℝ$
29		pirp	$⊢ π \in ℝ^{+}$
30		rphalfcl	$⊢ π \in ℝ^{+} \to \frac{π}{2} \in ℝ^{+}$
31		rpgt0	$⊢ \frac{π}{2} \in ℝ^{+} \to 0 < \frac{π}{2}$
32	29 30 31	mp2b	$⊢ 0 < \frac{π}{2}$
33		lt0neg2	$⊢ \frac{π}{2} \in ℝ \to (0 < \frac{π}{2} \leftrightarrow - \frac{π}{2} < 0)$
34	13 33	ax-mp	$⊢ 0 < \frac{π}{2} \leftrightarrow - \frac{π}{2} < 0$
35	32 34	mpbi	$⊢ - \frac{π}{2} < 0$
36	18	rexri	$⊢ - \frac{π}{2} \in ℝ^{*}$
37	13	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
38		elioo2	$⊢ (- \frac{π}{2} \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (0 \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (0 \in ℝ \land - \frac{π}{2} < 0 \land 0 < \frac{π}{2}))$
39	36 37 38	mp2an	$⊢ 0 \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (0 \in ℝ \land - \frac{π}{2} < 0 \land 0 < \frac{π}{2})$
40	28 35 32 39	mpbir3an	$⊢ 0 \in (- \frac{π}{2}, \frac{π}{2})$
41	27 40	eqeltrdi	$⊢ (A \in ℝ \land A = 0) \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$
42		elrp	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$
43		atanbndlem	$⊢ A \in ℝ^{+} \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$
44	42 43	sylbir	$⊢ (A \in ℝ \land 0 < A) \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$
45		lttri4	$⊢ (A \in ℝ \land 0 \in ℝ) \to (A < 0 \lor A = 0 \lor 0 < A)$
46	28 45	mpan2	$⊢ A \in ℝ \to (A < 0 \lor A = 0 \lor 0 < A)$
47	23 41 44 46	mpjao3dan	$⊢ A \in ℝ \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$

Metamath Proof Explorer

Theorem atanbnd

Proof