Metamath Proof Explorer

Theorem acosbnd

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

Ref Expression
Assertion acosbnd ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arccos ‘ 𝐴 ) ) ∈ ( 0 [,] π ) )

Proof

Step Hyp Ref Expression
1 acosval ⊢ ( 𝐴 ∈ ℂ → ( arccos ‘ 𝐴 ) = ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) )
2 1 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arccos ‘ 𝐴 ) ) = ( ℜ ‘ ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ) )
3 halfpire ⊢ ( π / 2 ) ∈ ℝ
4 3 recni ⊢ ( π / 2 ) ∈ ℂ
5 asincl ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) ∈ ℂ )
6 resub ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ ( arcsin ‘ 𝐴 ) ∈ ℂ ) → ( ℜ ‘ ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ) = ( ( ℜ ‘ ( π / 2 ) ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) )
7 4 5 6 sylancr ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ) = ( ( ℜ ‘ ( π / 2 ) ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) )
8 rere ⊢ ( ( π / 2 ) ∈ ℝ → ( ℜ ‘ ( π / 2 ) ) = ( π / 2 ) )
9 3 8 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( π / 2 )
10 9 oveq1i ⊢ ( ( ℜ ‘ ( π / 2 ) ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) = ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) )
11 7 10 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ) = ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) )
12 2 11 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arccos ‘ 𝐴 ) ) = ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) )
13 5 recld ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ℝ )
14 resubcl ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ℝ ) → ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ∈ ℝ )
15 3 13 14 sylancr ⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ∈ ℝ )
16 asinbnd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
17 neghalfpire ⊢ - ( π / 2 ) ∈ ℝ
18 17 3 elicc2i ⊢ ( ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) ≤ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∧ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
19 16 18 sylib ⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) ≤ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∧ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
20 19 simp3d ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ≤ ( π / 2 ) )
21 subge0 ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 ≤ ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ↔ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
22 3 13 21 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 0 ≤ ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ↔ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
23 20 22 mpbird ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) )
24 3 a1i ⊢ ( 𝐴 ∈ ℂ → ( π / 2 ) ∈ ℝ )
25 pire ⊢ π ∈ ℝ
26 25 a1i ⊢ ( 𝐴 ∈ ℂ → π ∈ ℝ )
27 25 recni ⊢ π ∈ ℂ
28 17 recni ⊢ - ( π / 2 ) ∈ ℂ
29 27 4 negsubi ⊢ ( π + - ( π / 2 ) ) = ( π − ( π / 2 ) )
30 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
31 27 4 4 30 subaddrii ⊢ ( π − ( π / 2 ) ) = ( π / 2 )
32 29 31 eqtri ⊢ ( π + - ( π / 2 ) ) = ( π / 2 )
33 4 27 28 32 subaddrii ⊢ ( ( π / 2 ) − π ) = - ( π / 2 )
34 19 simp2d ⊢ ( 𝐴 ∈ ℂ → - ( π / 2 ) ≤ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) )
35 33 34 eqbrtrid ⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) − π ) ≤ ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) )
36 24 26 13 35 subled ⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ≤ π )
37 0re ⊢ 0 ∈ ℝ
38 37 25 elicc2i ⊢ ( ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ↔ ( ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ∧ ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ≤ π ) )
39 15 23 36 38 syl3anbrc ⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) − ( ℜ ‘ ( arcsin ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) )
40 12 39 eqeltrd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( arccos ‘ 𝐴 ) ) ∈ ( 0 [,] π ) )