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

Metamath Proof Explorer

Theorem sinacos

Description: The sine of the arccosine of A is sqrt ( 1 - A ^ 2 ) . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion sinacos ⊢ A ∈ ℂ → sin ⁡ arccos ⁡ A = 1 − A 2

Proof

Step Hyp Ref Expression
1 acosval ⊢ A ∈ ℂ → arccos ⁡ A = π 2 − arcsin ⁡ A
2 1 oveq2d ⊢ A ∈ ℂ → π 2 − arccos ⁡ A = π 2 − π 2 − arcsin ⁡ A
3 picn ⊢ π ∈ ℂ
4 halfcl ⊢ π ∈ ℂ → π 2 ∈ ℂ
5 3 4 ax-mp ⊢ π 2 ∈ ℂ
6 asincl ⊢ A ∈ ℂ → arcsin ⁡ A ∈ ℂ
7 nncan ⊢ π 2 ∈ ℂ ∧ arcsin ⁡ A ∈ ℂ → π 2 − π 2 − arcsin ⁡ A = arcsin ⁡ A
8 5 6 7 sylancr ⊢ A ∈ ℂ → π 2 − π 2 − arcsin ⁡ A = arcsin ⁡ A
9 2 8 eqtrd ⊢ A ∈ ℂ → π 2 − arccos ⁡ A = arcsin ⁡ A
10 9 fveq2d ⊢ A ∈ ℂ → cos ⁡ π 2 − arccos ⁡ A = cos ⁡ arcsin ⁡ A
11 acoscl ⊢ A ∈ ℂ → arccos ⁡ A ∈ ℂ
12 coshalfpim ⊢ arccos ⁡ A ∈ ℂ → cos ⁡ π 2 − arccos ⁡ A = sin ⁡ arccos ⁡ A
13 11 12 syl ⊢ A ∈ ℂ → cos ⁡ π 2 − arccos ⁡ A = sin ⁡ arccos ⁡ A
14 cosasin ⊢ A ∈ ℂ → cos ⁡ arcsin ⁡ A = 1 − A 2
15 10 13 14 3eqtr3d ⊢ A ∈ ℂ → sin ⁡ arccos ⁡ A = 1 − A 2