Proof of Theorem acoscos
Step | Hyp | Ref
| Expression |
1 | | coscl 15836 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (cos‘𝐴) ∈ ℂ) |
3 | | acosval 26033 |
. . 3
⊢
((cos‘𝐴)
∈ ℂ → (arccos‘(cos‘𝐴)) = ((π / 2) −
(arcsin‘(cos‘𝐴)))) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (arccos‘(cos‘𝐴)) = ((π / 2) −
(arcsin‘(cos‘𝐴)))) |
5 | | picn 25616 |
. . . . . . . . 9
⊢ π
∈ ℂ |
6 | | halfcl 12198 |
. . . . . . . . 9
⊢ (π
∈ ℂ → (π / 2) ∈ ℂ) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢ (π /
2) ∈ ℂ |
8 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → 𝐴 ∈
ℂ) |
9 | | nncan 11250 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) − ((π / 2) − 𝐴)) = 𝐴) |
10 | 7, 8, 9 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − ((π / 2) − 𝐴)) = 𝐴) |
11 | 10 | fveq2d 6778 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (cos‘((π / 2) − ((π / 2) − 𝐴))) = (cos‘𝐴)) |
12 | | subcl 11220 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) − 𝐴) ∈ ℂ) |
13 | 7, 8, 12 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − 𝐴) ∈ ℂ) |
14 | | coshalfpim 25652 |
. . . . . . 7
⊢ (((π /
2) − 𝐴) ∈
ℂ → (cos‘((π / 2) − ((π / 2) − 𝐴))) = (sin‘((π / 2)
− 𝐴))) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (cos‘((π / 2) − ((π / 2) − 𝐴))) = (sin‘((π / 2)
− 𝐴))) |
16 | 11, 15 | eqtr3d 2780 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (cos‘𝐴) = (sin‘((π / 2) − 𝐴))) |
17 | 16 | fveq2d 6778 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (arcsin‘(cos‘𝐴)) = (arcsin‘(sin‘((π / 2)
− 𝐴)))) |
18 | | halfpire 25621 |
. . . . . . . . 9
⊢ (π /
2) ∈ ℝ |
19 | 18 | recni 10989 |
. . . . . . . 8
⊢ (π /
2) ∈ ℂ |
20 | | resub 14838 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → (ℜ‘((π / 2) − 𝐴)) = ((ℜ‘(π / 2)) −
(ℜ‘𝐴))) |
21 | 19, 8, 20 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (ℜ‘((π / 2) − 𝐴)) = ((ℜ‘(π / 2)) −
(ℜ‘𝐴))) |
22 | | rere 14833 |
. . . . . . . . 9
⊢ ((π /
2) ∈ ℝ → (ℜ‘(π / 2)) = (π /
2)) |
23 | 18, 22 | ax-mp 5 |
. . . . . . . 8
⊢
(ℜ‘(π / 2)) = (π / 2) |
24 | 23 | oveq1i 7285 |
. . . . . . 7
⊢
((ℜ‘(π / 2)) − (ℜ‘𝐴)) = ((π / 2) − (ℜ‘𝐴)) |
25 | 21, 24 | eqtrdi 2794 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (ℜ‘((π / 2) − 𝐴)) = ((π / 2) − (ℜ‘𝐴))) |
26 | | recl 14821 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (ℜ‘𝐴) ∈ ℝ) |
28 | | resubcl 11285 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → ((π / 2) −
(ℜ‘𝐴)) ∈
ℝ) |
29 | 18, 27, 28 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − (ℜ‘𝐴)) ∈ ℝ) |
30 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (π / 2) ∈ ℝ) |
31 | | neghalfpire 25622 |
. . . . . . . . 9
⊢ -(π /
2) ∈ ℝ |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → -(π / 2) ∈ ℝ) |
33 | | eliooord 13138 |
. . . . . . . . . . 11
⊢
((ℜ‘𝐴)
∈ (0(,)π) → (0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < π)) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < π)) |
35 | 34 | simprd 496 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (ℜ‘𝐴) < π) |
36 | 19, 19 | subnegi 11300 |
. . . . . . . . . 10
⊢ ((π /
2) − -(π / 2)) = ((π / 2) + (π / 2)) |
37 | | pidiv2halves 25624 |
. . . . . . . . . 10
⊢ ((π /
2) + (π / 2)) = π |
38 | 36, 37 | eqtri 2766 |
. . . . . . . . 9
⊢ ((π /
2) − -(π / 2)) = π |
39 | 35, 38 | breqtrrdi 5116 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (ℜ‘𝐴) < ((π / 2) − -(π /
2))) |
40 | 27, 30, 32, 39 | ltsub13d 11581 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → -(π / 2) < ((π / 2) − (ℜ‘𝐴))) |
41 | 34 | simpld 495 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → 0 < (ℜ‘𝐴)) |
42 | | ltsubpos 11467 |
. . . . . . . . 9
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ (π / 2) ∈ ℝ) → (0 <
(ℜ‘𝐴) ↔
((π / 2) − (ℜ‘𝐴)) < (π / 2))) |
43 | 27, 18, 42 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (0 < (ℜ‘𝐴) ↔ ((π / 2) −
(ℜ‘𝐴)) <
(π / 2))) |
44 | 41, 43 | mpbid 231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − (ℜ‘𝐴)) < (π / 2)) |
45 | 31 | rexri 11033 |
. . . . . . . 8
⊢ -(π /
2) ∈ ℝ* |
46 | 18 | rexri 11033 |
. . . . . . . 8
⊢ (π /
2) ∈ ℝ* |
47 | | elioo2 13120 |
. . . . . . . 8
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ (((π / 2) − (ℜ‘𝐴)) ∈ (-(π / 2)(,)(π / 2)) ↔
(((π / 2) − (ℜ‘𝐴)) ∈ ℝ ∧ -(π / 2) <
((π / 2) − (ℜ‘𝐴)) ∧ ((π / 2) −
(ℜ‘𝐴)) <
(π / 2)))) |
48 | 45, 46, 47 | mp2an 689 |
. . . . . . 7
⊢ (((π /
2) − (ℜ‘𝐴)) ∈ (-(π / 2)(,)(π / 2)) ↔
(((π / 2) − (ℜ‘𝐴)) ∈ ℝ ∧ -(π / 2) <
((π / 2) − (ℜ‘𝐴)) ∧ ((π / 2) −
(ℜ‘𝐴)) <
(π / 2))) |
49 | 29, 40, 44, 48 | syl3anbrc 1342 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − (ℜ‘𝐴)) ∈ (-(π / 2)(,)(π /
2))) |
50 | 25, 49 | eqeltrd 2839 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (ℜ‘((π / 2) − 𝐴)) ∈ (-(π / 2)(,)(π /
2))) |
51 | | asinsin 26042 |
. . . . 5
⊢ ((((π
/ 2) − 𝐴) ∈
ℂ ∧ (ℜ‘((π / 2) − 𝐴)) ∈ (-(π / 2)(,)(π / 2))) →
(arcsin‘(sin‘((π / 2) − 𝐴))) = ((π / 2) − 𝐴)) |
52 | 13, 50, 51 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (arcsin‘(sin‘((π / 2) − 𝐴))) = ((π / 2) − 𝐴)) |
53 | 17, 52 | eqtr2d 2779 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − 𝐴) = (arcsin‘(cos‘𝐴))) |
54 | | asincl 26023 |
. . . . 5
⊢
((cos‘𝐴)
∈ ℂ → (arcsin‘(cos‘𝐴)) ∈ ℂ) |
55 | 2, 54 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (arcsin‘(cos‘𝐴)) ∈ ℂ) |
56 | | subsub23 11226 |
. . . 4
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ ∧ (arcsin‘(cos‘𝐴)) ∈ ℂ) → (((π / 2)
− 𝐴) =
(arcsin‘(cos‘𝐴)) ↔ ((π / 2) −
(arcsin‘(cos‘𝐴))) = 𝐴)) |
57 | 19, 8, 55, 56 | mp3an2i 1465 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (((π / 2) − 𝐴) = (arcsin‘(cos‘𝐴)) ↔ ((π / 2) −
(arcsin‘(cos‘𝐴))) = 𝐴)) |
58 | 53, 57 | mpbid 231 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → ((π / 2) − (arcsin‘(cos‘𝐴))) = 𝐴) |
59 | 4, 58 | eqtrd 2778 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)π)) → (arccos‘(cos‘𝐴)) = 𝐴) |