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∈ℂ∧B∈ℂ∧A+B=1→sin⁡A⁢π2=cos⁡B⁢π2

Proof

Step Hyp Ref Expression
1 picn ⊢π∈ℂ
2 2cn ⊢2∈ℂ
3 2ne0 ⊢2≠0
4 1 2 3 divcli ⊢π2∈ℂ
5 mulcl ⊢A∈ℂ∧π2∈ℂ→A⁢π2∈ℂ
6 4 5 mpan2 ⊢A∈ℂ→A⁢π2∈ℂ
7 coshalfpim ⊢A⁢π2∈ℂ→cos⁡π2−A⁢π2=sin⁡A⁢π2
8 6 7 syl ⊢A∈ℂ→cos⁡π2−A⁢π2=sin⁡A⁢π2
9 8 3ad2ant1 ⊢A∈ℂ∧B∈ℂ∧A+B=1→cos⁡π2−A⁢π2=sin⁡A⁢π2
10 adddir ⊢A∈ℂ∧B∈ℂ∧π2∈ℂ→A+B⁢π2=A⁢π2+B⁢π2
11 4 10 mp3an3 ⊢A∈ℂ∧B∈ℂ→A+B⁢π2=A⁢π2+B⁢π2
12 11 3adant3 ⊢A∈ℂ∧B∈ℂ∧A+B=1→A+B⁢π2=A⁢π2+B⁢π2
13 oveq1 ⊢A+B=1→A+B⁢π2=1⁢π2
14 4 mullidi ⊢1⁢π2=π2
15 13 14 eqtrdi ⊢A+B=1→A+B⁢π2=π2
16 15 3ad2ant3 ⊢A∈ℂ∧B∈ℂ∧A+B=1→A+B⁢π2=π2
17 12 16 eqtr3d ⊢A∈ℂ∧B∈ℂ∧A+B=1→A⁢π2+B⁢π2=π2
18 mulcl ⊢B∈ℂ∧π2∈ℂ→B⁢π2∈ℂ
19 4 18 mpan2 ⊢B∈ℂ→B⁢π2∈ℂ
20 subadd ⊢π2∈ℂ∧A⁢π2∈ℂ∧B⁢π2∈ℂ→π2−A⁢π2=B⁢π2↔A⁢π2+B⁢π2=π2
21 4 6 19 20 mp3an3an ⊢A∈ℂ∧B∈ℂ→π2−A⁢π2=B⁢π2↔A⁢π2+B⁢π2=π2
22 21 3adant3 ⊢A∈ℂ∧B∈ℂ∧A+B=1→π2−A⁢π2=B⁢π2↔A⁢π2+B⁢π2=π2
23 17 22 mpbird ⊢A∈ℂ∧B∈ℂ∧A+B=1→π2−A⁢π2=B⁢π2
24 23 fveq2d ⊢A∈ℂ∧B∈ℂ∧A+B=1→cos⁡π2−A⁢π2=cos⁡B⁢π2
25 9 24 eqtr3d ⊢A∈ℂ∧B∈ℂ∧A+B=1→sin⁡A⁢π2=cos⁡B⁢π2