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 ( 𝐴 ∈ ℂ → ( sin ‘ ( arccos ‘ 𝐴 ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )

Proof

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