This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coshalfpim

Description: The cosine of _pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion coshalfpim ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 halfpire ⊢ ( π / 2 ) ∈ ℝ
2 1 recni ⊢ ( π / 2 ) ∈ ℂ
3 cossub ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) )
4 2 3 mpan ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) )
5 coshalfpi ⊢ ( cos ‘ ( π / 2 ) ) = 0
6 5 oveq1i ⊢ ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) = ( 0 · ( cos ‘ 𝐴 ) )
7 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
8 7 mul02d ⊢ ( 𝐴 ∈ ℂ → ( 0 · ( cos ‘ 𝐴 ) ) = 0 )
9 6 8 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) = 0 )
10 sinhalfpi ⊢ ( sin ‘ ( π / 2 ) ) = 1
11 10 oveq1i ⊢ ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) = ( 1 · ( sin ‘ 𝐴 ) )
12 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
13 12 mullidd ⊢ ( 𝐴 ∈ ℂ → ( 1 · ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
14 11 13 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
15 9 14 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) = ( 0 + ( sin ‘ 𝐴 ) ) )
16 12 addlidd ⊢ ( 𝐴 ∈ ℂ → ( 0 + ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
17 4 15 16 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )