Theorem 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 \mathrm{dom}arctan\to \cos arctan\left(A\right)\ne 0$$

Proof

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