Metamath Proof Explorer

Theorem coshalfpip

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

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

Proof

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