Metamath Proof Explorer

Theorem asinbnd

Description: The arcsine function has range within a vertical strip of the complex plane with real part between -upi / 2 and pi / 2 . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion asinbnd ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )

Proof

Step Hyp Ref Expression
1 asinval ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) = ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
2 1 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) = ( ℜ ‘ ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
3 ax-icn ⊢ i ∈ ℂ
4 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
5 3 4 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
6 ax-1cn ⊢ 1 ∈ ℂ
7 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
8 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
9 6 7 8 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
10 9 sqrtcld ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
11 5 10 addcld ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
12 asinlem ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
13 11 12 logcld ⊢ ( 𝐴 ∈ ℂ → ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ )
14 imre ⊢ ( ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ℜ ‘ ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
15 13 14 syl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ℜ ‘ ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
16 2 15 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) = ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
17 asinlem3 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
18 argrege0 ⊢ ( ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 ∧ 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
19 11 12 17 18 syl3anc ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
20 16 19 eqeltrd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )