This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )