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 )