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 ⊢A∈ℂ→ℜ⁡arccos⁡A∈0π

Proof

Step Hyp Ref Expression
1 acosval ⊢A∈ℂ→arccos⁡A=π2−arcsin⁡A
2 1 fveq2d ⊢A∈ℂ→ℜ⁡arccos⁡A=ℜ⁡π2−arcsin⁡A
3 halfpire ⊢π2∈ℝ
4 3 recni ⊢π2∈ℂ
5 asincl ⊢A∈ℂ→arcsin⁡A∈ℂ
6 resub ⊢π2∈ℂ∧arcsin⁡A∈ℂ→ℜ⁡π2−arcsin⁡A=ℜ⁡π2−ℜ⁡arcsin⁡A
7 4 5 6 sylancr ⊢A∈ℂ→ℜ⁡π2−arcsin⁡A=ℜ⁡π2−ℜ⁡arcsin⁡A
8 rere ⊢π2∈ℝ→ℜ⁡π2=π2
9 3 8 ax-mp ⊢ℜ⁡π2=π2
10 9 oveq1i ⊢ℜ⁡π2−ℜ⁡arcsin⁡A=π2−ℜ⁡arcsin⁡A
11 7 10 eqtrdi ⊢A∈ℂ→ℜ⁡π2−arcsin⁡A=π2−ℜ⁡arcsin⁡A
12 2 11 eqtrd ⊢A∈ℂ→ℜ⁡arccos⁡A=π2−ℜ⁡arcsin⁡A
13 5 recld ⊢A∈ℂ→ℜ⁡arcsin⁡A∈ℝ
14 resubcl ⊢π2∈ℝ∧ℜ⁡arcsin⁡A∈ℝ→π2−ℜ⁡arcsin⁡A∈ℝ
15 3 13 14 sylancr ⊢A∈ℂ→π2−ℜ⁡arcsin⁡A∈ℝ
16 asinbnd ⊢A∈ℂ→ℜ⁡arcsin⁡A∈−π2π2
17 neghalfpire ⊢−π2∈ℝ
18 17 3 elicc2i ⊢ℜ⁡arcsin⁡A∈−π2π2↔ℜ⁡arcsin⁡A∈ℝ∧−π2≤ℜ⁡arcsin⁡A∧ℜ⁡arcsin⁡A≤π2
19 16 18 sylib ⊢A∈ℂ→ℜ⁡arcsin⁡A∈ℝ∧−π2≤ℜ⁡arcsin⁡A∧ℜ⁡arcsin⁡A≤π2
20 19 simp3d ⊢A∈ℂ→ℜ⁡arcsin⁡A≤π2
21 subge0 ⊢π2∈ℝ∧ℜ⁡arcsin⁡A∈ℝ→0≤π2−ℜ⁡arcsin⁡A↔ℜ⁡arcsin⁡A≤π2
22 3 13 21 sylancr ⊢A∈ℂ→0≤π2−ℜ⁡arcsin⁡A↔ℜ⁡arcsin⁡A≤π2
23 20 22 mpbird ⊢A∈ℂ→0≤π2−ℜ⁡arcsin⁡A
24 3 a1i ⊢A∈ℂ→π2∈ℝ
25 pire ⊢π∈ℝ
26 25 a1i ⊢A∈ℂ→π∈ℝ
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 ⊢A∈ℂ→−π2≤ℜ⁡arcsin⁡A
35 33 34 eqbrtrid ⊢A∈ℂ→π2−π≤ℜ⁡arcsin⁡A
36 24 26 13 35 subled ⊢A∈ℂ→π2−ℜ⁡arcsin⁡A≤π
37 0re ⊢0∈ℝ
38 37 25 elicc2i ⊢π2−ℜ⁡arcsin⁡A∈0π↔π2−ℜ⁡arcsin⁡A∈ℝ∧0≤π2−ℜ⁡arcsin⁡A∧π2−ℜ⁡arcsin⁡A≤π
39 15 23 36 38 syl3anbrc ⊢A∈ℂ→π2−ℜ⁡arcsin⁡A∈0π
40 12 39 eqeltrd ⊢A∈ℂ→ℜ⁡arccos⁡A∈0π