Metamath Proof Explorer

Theorem asinsinb

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

Ref Expression
Assertion asinsinb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arcsin ⁡ A = B ↔ sin ⁡ B = A

Proof

Step Hyp Ref Expression
1 sinasin ⊢ A ∈ ℂ → sin ⁡ arcsin ⁡ A = A
2 1 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → sin ⁡ arcsin ⁡ A = A
3 fveqeq2 ⊢ arcsin ⁡ A = B → sin ⁡ arcsin ⁡ A = A ↔ sin ⁡ B = A
4 2 3 syl5ibcom ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arcsin ⁡ A = B → sin ⁡ B = A
5 asinsin ⊢ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arcsin ⁡ sin ⁡ B = B
6 5 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arcsin ⁡ sin ⁡ B = B
7 fveqeq2 ⊢ sin ⁡ B = A → arcsin ⁡ sin ⁡ B = B ↔ arcsin ⁡ A = B
8 6 7 syl5ibcom ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → sin ⁡ B = A → arcsin ⁡ A = B
9 4 8 impbid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ − π 2 π 2 → arcsin ⁡ A = B ↔ sin ⁡ B = A