Metamath Proof Explorer

Theorem sincosq1eq

Description: Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008)

Ref Expression
Assertion sincosq1eq 
|- ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( sin ` ( A x. ( _pi / 2 ) ) ) = ( cos ` ( B x. ( _pi / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 2cn 
 |-  2 e. CC
3 2ne0 
 |-  2 =/= 0
4 1 2 3 divcli 
 |-  ( _pi / 2 ) e. CC
5 mulcl 
 |-  ( ( A e. CC /\ ( _pi / 2 ) e. CC ) -> ( A x. ( _pi / 2 ) ) e. CC )
6 4 5 mpan2 
 |-  ( A e. CC -> ( A x. ( _pi / 2 ) ) e. CC )
7 coshalfpim 
 |-  ( ( A x. ( _pi / 2 ) ) e. CC -> ( cos ` ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) ) = ( sin ` ( A x. ( _pi / 2 ) ) ) )
8 6 7 syl 
 |-  ( A e. CC -> ( cos ` ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) ) = ( sin ` ( A x. ( _pi / 2 ) ) ) )
9 8 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( cos ` ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) ) = ( sin ` ( A x. ( _pi / 2 ) ) ) )
10 adddir 
 |-  ( ( A e. CC /\ B e. CC /\ ( _pi / 2 ) e. CC ) -> ( ( A + B ) x. ( _pi / 2 ) ) = ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) )
11 4 10 mp3an3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) x. ( _pi / 2 ) ) = ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) )
12 11 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( ( A + B ) x. ( _pi / 2 ) ) = ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) )
13 oveq1 
 |-  ( ( A + B ) = 1 -> ( ( A + B ) x. ( _pi / 2 ) ) = ( 1 x. ( _pi / 2 ) ) )
14 4 mulid2i 
 |-  ( 1 x. ( _pi / 2 ) ) = ( _pi / 2 )
15 13 14 eqtrdi 
 |-  ( ( A + B ) = 1 -> ( ( A + B ) x. ( _pi / 2 ) ) = ( _pi / 2 ) )
16 15 3ad2ant3 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( ( A + B ) x. ( _pi / 2 ) ) = ( _pi / 2 ) )
17 12 16 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) = ( _pi / 2 ) )
18 mulcl 
 |-  ( ( B e. CC /\ ( _pi / 2 ) e. CC ) -> ( B x. ( _pi / 2 ) ) e. CC )
19 4 18 mpan2 
 |-  ( B e. CC -> ( B x. ( _pi / 2 ) ) e. CC )
20 subadd 
 |-  ( ( ( _pi / 2 ) e. CC /\ ( A x. ( _pi / 2 ) ) e. CC /\ ( B x. ( _pi / 2 ) ) e. CC ) -> ( ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) = ( B x. ( _pi / 2 ) ) <-> ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) = ( _pi / 2 ) ) )
21 4 6 19 20 mp3an3an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) = ( B x. ( _pi / 2 ) ) <-> ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) = ( _pi / 2 ) ) )
22 21 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) = ( B x. ( _pi / 2 ) ) <-> ( ( A x. ( _pi / 2 ) ) + ( B x. ( _pi / 2 ) ) ) = ( _pi / 2 ) ) )
23 17 22 mpbird 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) = ( B x. ( _pi / 2 ) ) )
24 23 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( cos ` ( ( _pi / 2 ) - ( A x. ( _pi / 2 ) ) ) ) = ( cos ` ( B x. ( _pi / 2 ) ) ) )
25 9 24 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( sin ` ( A x. ( _pi / 2 ) ) ) = ( cos ` ( B x. ( _pi / 2 ) ) ) )