Theorem atantanb

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

	Ref	Expression
Assertion	atantanb	⊢ ( ( 𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arctan ‘ 𝐴 ) = 𝐵 ↔ ( tan ‘ 𝐵 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tanatan	⊢ ( 𝐴 ∈ dom arctan → ( tan ‘ ( arctan ‘ 𝐴 ) ) = 𝐴 )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( tan ‘ ( arctan ‘ 𝐴 ) ) = 𝐴 )
3		fveqeq2	⊢ ( ( arctan ‘ 𝐴 ) = 𝐵 → ( ( tan ‘ ( arctan ‘ 𝐴 ) ) = 𝐴 ↔ ( tan ‘ 𝐵 ) = 𝐴 ) )
4	2 3	syl5ibcom	⊢ ( ( 𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arctan ‘ 𝐴 ) = 𝐵 → ( tan ‘ 𝐵 ) = 𝐴 ) )
5		atantan	⊢ ( ( 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arctan ‘ ( tan ‘ 𝐵 ) ) = 𝐵 )
6	5	3adant1	⊢ ( ( 𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arctan ‘ ( tan ‘ 𝐵 ) ) = 𝐵 )
7		fveqeq2	⊢ ( ( tan ‘ 𝐵 ) = 𝐴 → ( ( arctan ‘ ( tan ‘ 𝐵 ) ) = 𝐵 ↔ ( arctan ‘ 𝐴 ) = 𝐵 ) )
8	6 7	syl5ibcom	⊢ ( ( 𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( tan ‘ 𝐵 ) = 𝐴 → ( arctan ‘ 𝐴 ) = 𝐵 ) )
9	4 8	impbid	⊢ ( ( 𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arctan ‘ 𝐴 ) = 𝐵 ↔ ( tan ‘ 𝐵 ) = 𝐴 ) )