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 ) ) ) )