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

Metamath Proof Explorer

Theorem asinsinb

Description: Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion asinsinb ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arcsin ‘ 𝐴 ) = 𝐵 ↔ ( sin ‘ 𝐵 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sinasin ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( arcsin ‘ 𝐴 ) ) = 𝐴 )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ ( arcsin ‘ 𝐴 ) ) = 𝐴 )
3 fveqeq2 ⊢ ( ( arcsin ‘ 𝐴 ) = 𝐵 → ( ( sin ‘ ( arcsin ‘ 𝐴 ) ) = 𝐴 ↔ ( sin ‘ 𝐵 ) = 𝐴 ) )
4 2 3 syl5ibcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arcsin ‘ 𝐴 ) = 𝐵 → ( sin ‘ 𝐵 ) = 𝐴 ) )
5 asinsin ⊢ ( ( 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐵 ) ) = 𝐵 )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐵 ) ) = 𝐵 )
7 fveqeq2 ⊢ ( ( sin ‘ 𝐵 ) = 𝐴 → ( ( arcsin ‘ ( sin ‘ 𝐵 ) ) = 𝐵 ↔ ( arcsin ‘ 𝐴 ) = 𝐵 ) )
8 6 7 syl5ibcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( sin ‘ 𝐵 ) = 𝐴 → ( arcsin ‘ 𝐴 ) = 𝐵 ) )
9 4 8 impbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arcsin ‘ 𝐴 ) = 𝐵 ↔ ( sin ‘ 𝐵 ) = 𝐴 ) )