Metamath Proof Explorer


Theorem atandmtan

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

Ref Expression
Assertion atandmtan ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) ∈ dom arctan )

Proof

Step Hyp Ref Expression
1 tancl ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) ∈ ℂ )
2 tanval ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
3 2 oveq1d ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( tan ‘ 𝐴 ) ↑ 2 ) = ( ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ↑ 2 ) )
4 sincl ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
5 4 adantr ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sin ‘ 𝐴 ) ∈ ℂ )
6 coscl ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
7 6 adantr ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ∈ ℂ )
8 simpr ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ≠ 0 )
9 5 7 8 sqdivd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ↑ 2 ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) / ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
10 3 9 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( tan ‘ 𝐴 ) ↑ 2 ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) / ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
11 5 sqcld ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
12 7 sqcld ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
13 12 negcld ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → - ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
14 11 12 subnegd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) − - ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
15 sincossq ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
16 15 adantr ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
17 14 16 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) − - ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
18 ax-1ne0 1 ≠ 0
19 18 a1i ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → 1 ≠ 0 )
20 17 19 eqnetrd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) − - ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ≠ 0 )
21 11 13 20 subne0ad ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( sin ‘ 𝐴 ) ↑ 2 ) ≠ - ( ( cos ‘ 𝐴 ) ↑ 2 ) )
22 12 mulm1d ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( - 1 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = - ( ( cos ‘ 𝐴 ) ↑ 2 ) )
23 21 22 neeqtrrd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( sin ‘ 𝐴 ) ↑ 2 ) ≠ ( - 1 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
24 neg1cn - 1 ∈ ℂ
25 24 a1i ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → - 1 ∈ ℂ )
26 sqne0 ( ( cos ‘ 𝐴 ) ∈ ℂ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) ≠ 0 ↔ ( cos ‘ 𝐴 ) ≠ 0 ) )
27 6 26 syl ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) ≠ 0 ↔ ( cos ‘ 𝐴 ) ≠ 0 ) )
28 27 biimpar ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) ↑ 2 ) ≠ 0 )
29 11 25 12 28 divmul3d ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( sin ‘ 𝐴 ) ↑ 2 ) / ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = - 1 ↔ ( ( sin ‘ 𝐴 ) ↑ 2 ) = ( - 1 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) )
30 29 necon3bid ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( sin ‘ 𝐴 ) ↑ 2 ) / ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ≠ - 1 ↔ ( ( sin ‘ 𝐴 ) ↑ 2 ) ≠ ( - 1 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) )
31 23 30 mpbird ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) / ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ≠ - 1 )
32 10 31 eqnetrd ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( tan ‘ 𝐴 ) ↑ 2 ) ≠ - 1 )
33 atandm3 ( ( tan ‘ 𝐴 ) ∈ dom arctan ↔ ( ( tan ‘ 𝐴 ) ∈ ℂ ∧ ( ( tan ‘ 𝐴 ) ↑ 2 ) ≠ - 1 ) )
34 1 32 33 sylanbrc ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) ∈ dom arctan )