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

Metamath Proof Explorer

Theorem sinhalfpip

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

Ref Expression
Assertion sinhalfpip ⊢ A ∈ ℂ → sin ⁡ π 2 + A = cos ⁡ A

Proof

Step Hyp Ref Expression
1 halfpire ⊢ π 2 ∈ ℝ
2 1 recni ⊢ π 2 ∈ ℂ
3 sinadd ⊢ π 2 ∈ ℂ ∧ A ∈ ℂ → sin ⁡ π 2 + A = sin ⁡ π 2 ⁢ cos ⁡ A + cos ⁡ π 2 ⁢ sin ⁡ A
4 2 3 mpan ⊢ A ∈ ℂ → sin ⁡ π 2 + A = sin ⁡ π 2 ⁢ cos ⁡ A + cos ⁡ π 2 ⁢ sin ⁡ A
5 sinhalfpi ⊢ sin ⁡ π 2 = 1
6 5 oveq1i ⊢ sin ⁡ π 2 ⁢ cos ⁡ A = 1 ⁢ cos ⁡ A
7 coscl ⊢ A ∈ ℂ → cos ⁡ A ∈ ℂ
8 7 mullidd ⊢ A ∈ ℂ → 1 ⁢ cos ⁡ A = cos ⁡ A
9 6 8 eqtrid ⊢ A ∈ ℂ → sin ⁡ π 2 ⁢ cos ⁡ A = cos ⁡ A
10 coshalfpi ⊢ cos ⁡ π 2 = 0
11 10 oveq1i ⊢ cos ⁡ π 2 ⁢ sin ⁡ A = 0 ⋅ sin ⁡ A
12 sincl ⊢ A ∈ ℂ → sin ⁡ A ∈ ℂ
13 12 mul02d ⊢ A ∈ ℂ → 0 ⋅ sin ⁡ A = 0
14 11 13 eqtrid ⊢ A ∈ ℂ → cos ⁡ π 2 ⁢ sin ⁡ A = 0
15 9 14 oveq12d ⊢ A ∈ ℂ → sin ⁡ π 2 ⁢ cos ⁡ A + cos ⁡ π 2 ⁢ sin ⁡ A = cos ⁡ A + 0
16 7 addridd ⊢ A ∈ ℂ → cos ⁡ A + 0 = cos ⁡ A
17 4 15 16 3eqtrd ⊢ A ∈ ℂ → sin ⁡ π 2 + A = cos ⁡ A