Metamath Proof Explorer

Theorem acoscos

Description: The arccosine function is an inverse to cos . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acoscos ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( arccos ‘ ( cos ‘ 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( cos ‘ 𝐴 ) ∈ ℂ )
3 acosval ⊢ ( ( cos ‘ 𝐴 ) ∈ ℂ → ( arccos ‘ ( cos ‘ 𝐴 ) ) = ( ( π / 2 ) − ( arcsin ‘ ( cos ‘ 𝐴 ) ) ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( arccos ‘ ( cos ‘ 𝐴 ) ) = ( ( π / 2 ) − ( arcsin ‘ ( cos ‘ 𝐴 ) ) ) )
5 picn ⊢ π ∈ ℂ
6 halfcl ⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
7 5 6 ax-mp ⊢ ( π / 2 ) ∈ ℂ
8 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → 𝐴 ∈ ℂ )
9 nncan ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) = 𝐴 )
10 7 8 9 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) = 𝐴 )
11 10 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( cos ‘ ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ) = ( cos ‘ 𝐴 ) )
12 subcl ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℂ )
13 7 8 12 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ℂ )
14 coshalfpim ⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ) = ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
15 13 14 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( cos ‘ ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ) = ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
16 11 15 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( cos ‘ 𝐴 ) = ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
17 16 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( arcsin ‘ ( cos ‘ 𝐴 ) ) = ( arcsin ‘ ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ) )
18 halfpire ⊢ ( π / 2 ) ∈ ℝ
19 18 recni ⊢ ( π / 2 ) ∈ ℂ
20 resub ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℜ ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( ℜ ‘ ( π / 2 ) ) − ( ℜ ‘ 𝐴 ) ) )
21 19 8 20 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ℜ ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( ℜ ‘ ( π / 2 ) ) − ( ℜ ‘ 𝐴 ) ) )
22 rere ⊢ ( ( π / 2 ) ∈ ℝ → ( ℜ ‘ ( π / 2 ) ) = ( π / 2 ) )
23 18 22 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( π / 2 )
24 23 oveq1i ⊢ ( ( ℜ ‘ ( π / 2 ) ) − ( ℜ ‘ 𝐴 ) ) = ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) )
25 21 24 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ℜ ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) )
26 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
28 resubcl ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
29 18 27 28 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
30 18 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( π / 2 ) ∈ ℝ )
31 neghalfpire ⊢ - ( π / 2 ) ∈ ℝ
32 31 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → - ( π / 2 ) ∈ ℝ )
33 eliooord ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) → ( 0 < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < π ) )
34 33 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( 0 < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < π ) )
35 34 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ℜ ‘ 𝐴 ) < π )
36 19 19 subnegi ⊢ ( ( π / 2 ) − - ( π / 2 ) ) = ( ( π / 2 ) + ( π / 2 ) )
37 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
38 36 37 eqtri ⊢ ( ( π / 2 ) − - ( π / 2 ) ) = π
39 35 38 breqtrrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ℜ ‘ 𝐴 ) < ( ( π / 2 ) − - ( π / 2 ) ) )
40 27 30 32 39 ltsub13d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → - ( π / 2 ) < ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) )
41 34 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → 0 < ( ℜ ‘ 𝐴 ) )
42 ltsubpos ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 0 < ( ℜ ‘ 𝐴 ) ↔ ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) < ( π / 2 ) ) )
43 27 18 42 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( 0 < ( ℜ ‘ 𝐴 ) ↔ ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) < ( π / 2 ) ) )
44 41 43 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) < ( π / 2 ) )
45 31 rexri ⊢ - ( π / 2 ) ∈ ℝ*
46 18 rexri ⊢ ( π / 2 ) ∈ ℝ*
47 elioo2 ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) < ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∧ ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) < ( π / 2 ) ) ) )
48 45 46 47 mp2an ⊢ ( ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) < ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∧ ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) < ( π / 2 ) ) )
49 29 40 44 48 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − ( ℜ ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
50 25 49 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ℜ ‘ ( ( π / 2 ) − 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
51 asinsin ⊢ ( ( ( ( π / 2 ) − 𝐴 ) ∈ ℂ ∧ ( ℜ ‘ ( ( π / 2 ) − 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ) = ( ( π / 2 ) − 𝐴 ) )
52 13 50 51 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( arcsin ‘ ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ) = ( ( π / 2 ) − 𝐴 ) )
53 17 52 eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − 𝐴 ) = ( arcsin ‘ ( cos ‘ 𝐴 ) ) )
54 asincl ⊢ ( ( cos ‘ 𝐴 ) ∈ ℂ → ( arcsin ‘ ( cos ‘ 𝐴 ) ) ∈ ℂ )
55 2 54 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( arcsin ‘ ( cos ‘ 𝐴 ) ) ∈ ℂ )
56 subsub23 ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( arcsin ‘ ( cos ‘ 𝐴 ) ) ∈ ℂ ) → ( ( ( π / 2 ) − 𝐴 ) = ( arcsin ‘ ( cos ‘ 𝐴 ) ) ↔ ( ( π / 2 ) − ( arcsin ‘ ( cos ‘ 𝐴 ) ) ) = 𝐴 ) )
57 19 8 55 56 mp3an2i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( ( π / 2 ) − 𝐴 ) = ( arcsin ‘ ( cos ‘ 𝐴 ) ) ↔ ( ( π / 2 ) − ( arcsin ‘ ( cos ‘ 𝐴 ) ) ) = 𝐴 ) )
58 53 57 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( ( π / 2 ) − ( arcsin ‘ ( cos ‘ 𝐴 ) ) ) = 𝐴 )
59 4 58 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) π ) ) → ( arccos ‘ ( cos ‘ 𝐴 ) ) = 𝐴 )