Metamath Proof Explorer

Theorem tanhalfpim

Description: The tangent of _pi / 2 minus a number is the cotangent, here represented by cos A / sin A . (Contributed by SN, 2-Sep-2025)

Ref Expression
Hypotheses tanhalfpim.a 
|- ( ph -> A e. CC )
tanhalfpim.1 
|- ( ph -> ( sin ` A ) =/= 0 )
Assertion tanhalfpim 
|- ( ph -> ( tan ` ( ( _pi / 2 ) - A ) ) = ( ( cos ` A ) / ( sin ` A ) ) )

Proof

Step Hyp Ref Expression
1 tanhalfpim.a 
 |-  ( ph -> A e. CC )
2 tanhalfpim.1 
 |-  ( ph -> ( sin ` A ) =/= 0 )
3 picn 
 |-  _pi e. CC
4 2cn 
 |-  2 e. CC
5 2ne0 
 |-  2 =/= 0
6 3 4 5 divcli 
 |-  ( _pi / 2 ) e. CC
7 6 a1i 
 |-  ( ph -> ( _pi / 2 ) e. CC )
8 7 1 subcld 
 |-  ( ph -> ( ( _pi / 2 ) - A ) e. CC )
9 coshalfpim 
 |-  ( A e. CC -> ( cos ` ( ( _pi / 2 ) - A ) ) = ( sin ` A ) )
10 1 9 syl 
 |-  ( ph -> ( cos ` ( ( _pi / 2 ) - A ) ) = ( sin ` A ) )
11 10 2 eqnetrd 
 |-  ( ph -> ( cos ` ( ( _pi / 2 ) - A ) ) =/= 0 )
12 tanval 
 |-  ( ( ( ( _pi / 2 ) - A ) e. CC /\ ( cos ` ( ( _pi / 2 ) - A ) ) =/= 0 ) -> ( tan ` ( ( _pi / 2 ) - A ) ) = ( ( sin ` ( ( _pi / 2 ) - A ) ) / ( cos ` ( ( _pi / 2 ) - A ) ) ) )
13 8 11 12 syl2anc 
 |-  ( ph -> ( tan ` ( ( _pi / 2 ) - A ) ) = ( ( sin ` ( ( _pi / 2 ) - A ) ) / ( cos ` ( ( _pi / 2 ) - A ) ) ) )
14 sinhalfpim 
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
15 14 9 oveq12d 
 |-  ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) - A ) ) / ( cos ` ( ( _pi / 2 ) - A ) ) ) = ( ( cos ` A ) / ( sin ` A ) ) )
16 1 15 syl 
 |-  ( ph -> ( ( sin ` ( ( _pi / 2 ) - A ) ) / ( cos ` ( ( _pi / 2 ) - A ) ) ) = ( ( cos ` A ) / ( sin ` A ) ) )
17 13 16 eqtrd 
 |-  ( ph -> ( tan ` ( ( _pi / 2 ) - A ) ) = ( ( cos ` A ) / ( sin ` A ) ) )