cosatanne0

Description: The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015)

		Ref	Expression
	Assertion	cosatanne0	$⊢ A \in dom arctan \to \cos arctan (A) \neq 0$

Step	Hyp	Ref	Expression
1		cosatan	$⊢ A \in dom arctan \to \cos arctan (A) = \frac{1}{\sqrt{1 + A^{2}}}$
2		ax-1cn	$⊢ 1 \in ℂ$
3		atandm4	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 + A^{2} \neq 0)$
4	3	simplbi	$⊢ A \in dom arctan \to A \in ℂ$
5	4	sqcld	$⊢ A \in dom arctan \to A^{2} \in ℂ$
6		addcl	$⊢ (1 \in ℂ \land A^{2} \in ℂ) \to 1 + A^{2} \in ℂ$
7	2 5 6	sylancr	$⊢ A \in dom arctan \to 1 + A^{2} \in ℂ$
8	7	sqrtcld	$⊢ A \in dom arctan \to \sqrt{1 + A^{2}} \in ℂ$
9	7	sqsqrtd	$⊢ A \in dom arctan \to {\sqrt{1 + A^{2}}}^{2} = 1 + A^{2}$
10	3	simprbi	$⊢ A \in dom arctan \to 1 + A^{2} \neq 0$
11	9 10	eqnetrd	$⊢ A \in dom arctan \to {\sqrt{1 + A^{2}}}^{2} \neq 0$
12		sqne0	$⊢ \sqrt{1 + A^{2}} \in ℂ \to ({\sqrt{1 + A^{2}}}^{2} \neq 0 \leftrightarrow \sqrt{1 + A^{2}} \neq 0)$
13	8 12	syl	$⊢ A \in dom arctan \to ({\sqrt{1 + A^{2}}}^{2} \neq 0 \leftrightarrow \sqrt{1 + A^{2}} \neq 0)$
14	11 13	mpbid	$⊢ A \in dom arctan \to \sqrt{1 + A^{2}} \neq 0$
15	8 14	recne0d	$⊢ A \in dom arctan \to \frac{1}{\sqrt{1 + A^{2}}} \neq 0$
16	1 15	eqnetrd	$⊢ A \in dom arctan \to \cos arctan (A) \neq 0$

Metamath Proof Explorer