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