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