Metamath Proof Explorer

Theorem atantanb

Description: Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atantanb ⊢ A ∈ dom ⁡ arctan ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arctan ⁡ A = B ↔ tan ⁡ B = A

Proof

Step Hyp Ref Expression
1 tanatan ⊢ A ∈ dom ⁡ arctan → tan ⁡ arctan ⁡ A = A
2 1 3ad2ant1 ⊢ A ∈ dom ⁡ arctan ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → tan ⁡ arctan ⁡ A = A
3 fveqeq2 ⊢ arctan ⁡ A = B → tan ⁡ arctan ⁡ A = A ↔ tan ⁡ B = A
4 2 3 syl5ibcom ⊢ A ∈ dom ⁡ arctan ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arctan ⁡ A = B → tan ⁡ B = A
5 atantan ⊢ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arctan ⁡ tan ⁡ B = B
6 5 3adant1 ⊢ A ∈ dom ⁡ arctan ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arctan ⁡ tan ⁡ B = B
7 fveqeq2 ⊢ tan ⁡ B = A → arctan ⁡ tan ⁡ B = B ↔ arctan ⁡ A = B
8 6 7 syl5ibcom ⊢ A ∈ dom ⁡ arctan ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → tan ⁡ B = A → arctan ⁡ A = B
9 4 8 impbid ⊢ A ∈ dom ⁡ arctan ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arctan ⁡ A = B ↔ tan ⁡ B = A