Metamath Proof Explorer


Theorem tancl

Description: The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014)

Ref Expression
Assertion tancl AcosA0tanA

Proof

Step Hyp Ref Expression
1 tanval AcosA0tanA=sinAcosA
2 sincl AsinA
3 2 adantr AcosA0sinA
4 coscl AcosA
5 4 adantr AcosA0cosA
6 simpr AcosA0cosA0
7 3 5 6 divcld AcosA0sinAcosA
8 1 7 eqeltrd AcosA0tanA