atanrecl

Description: The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	atanrecl	$⊢ A \in ℝ \to arctan (A) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ \land A = 0) \to A = 0$
2	1	fveq2d	$⊢ (A \in ℝ \land A = 0) \to arctan (A) = arctan (0)$
3		atan0	$⊢ arctan (0) = 0$
4		0re	$⊢ 0 \in ℝ$
5	3 4	eqeltri	$⊢ arctan (0) \in ℝ$
6	2 5	eqeltrdi	$⊢ (A \in ℝ \land A = 0) \to arctan (A) \in ℝ$
7		atanre	$⊢ A \in ℝ \to A \in dom arctan$
8	7	adantr	$⊢ (A \in ℝ \land A \neq 0) \to A \in dom arctan$
9		atancl	$⊢ A \in dom arctan \to arctan (A) \in ℂ$
10	8 9	syl	$⊢ (A \in ℝ \land A \neq 0) \to arctan (A) \in ℂ$
11		simpl	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℝ$
12	11	recnd	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℂ$
13		rere	$⊢ A \in ℝ \to ℜ (A) = A$
14	13	adantr	$⊢ (A \in ℝ \land A \neq 0) \to ℜ (A) = A$
15		simpr	$⊢ (A \in ℝ \land A \neq 0) \to A \neq 0$
16	14 15	eqnetrd	$⊢ (A \in ℝ \land A \neq 0) \to ℜ (A) \neq 0$
17		atancj	$⊢ (A \in ℂ \land ℜ (A) \neq 0) \to (A \in dom arctan \land \overline{arctan (A)} = arctan (\overline{A}))$
18	12 16 17	syl2anc	$⊢ (A \in ℝ \land A \neq 0) \to (A \in dom arctan \land \overline{arctan (A)} = arctan (\overline{A}))$
19	18	simprd	$⊢ (A \in ℝ \land A \neq 0) \to \overline{arctan (A)} = arctan (\overline{A})$
20		cjre	$⊢ A \in ℝ \to \overline{A} = A$
21	20	adantr	$⊢ (A \in ℝ \land A \neq 0) \to \overline{A} = A$
22	21	fveq2d	$⊢ (A \in ℝ \land A \neq 0) \to arctan (\overline{A}) = arctan (A)$
23	19 22	eqtrd	$⊢ (A \in ℝ \land A \neq 0) \to \overline{arctan (A)} = arctan (A)$
24	10 23	cjrebd	$⊢ (A \in ℝ \land A \neq 0) \to arctan (A) \in ℝ$
25	6 24	pm2.61dane	$⊢ A \in ℝ \to arctan (A) \in ℝ$

Metamath Proof Explorer

Theorem atanrecl

Proof