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	⊢ ( 𝐴 ∈ dom arctan → ( cos ‘ ( arctan ‘ 𝐴 ) ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		cosatan	⊢ ( 𝐴 ∈ dom arctan → ( cos ‘ ( arctan ‘ 𝐴 ) ) = ( 1 / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )
2		ax-1cn	⊢ 1 ∈ ℂ
3		atandm4	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ≠ 0 ) )
4	3	simplbi	⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
5	4	sqcld	⊢ ( 𝐴 ∈ dom arctan → ( 𝐴 ↑ 2 ) ∈ ℂ )
6		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ )
7	2 5 6	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ )
8	7	sqrtcld	⊢ ( 𝐴 ∈ dom arctan → ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
9	7	sqsqrtd	⊢ ( 𝐴 ∈ dom arctan → ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
10	3	simprbi	⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( 𝐴 ↑ 2 ) ) ≠ 0 )
11	9 10	eqnetrd	⊢ ( 𝐴 ∈ dom arctan → ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) ≠ 0 )
12		sqne0	⊢ ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ∈ ℂ → ( ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ≠ 0 ) )
13	8 12	syl	⊢ ( 𝐴 ∈ dom arctan → ( ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ≠ 0 ) )
14	11 13	mpbid	⊢ ( 𝐴 ∈ dom arctan → ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ≠ 0 )
15	8 14	recne0d	⊢ ( 𝐴 ∈ dom arctan → ( 1 / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
16	1 15	eqnetrd	⊢ ( 𝐴 ∈ dom arctan → ( cos ‘ ( arctan ‘ 𝐴 ) ) ≠ 0 )