Proof of Theorem dvacos
Step | Hyp | Ref
| Expression |
1 | | df-acos 24393 |
. . . . 5
⊢ arccos =
(𝑥 ∈ ℂ ↦
((π / 2) − (arcsin‘𝑥))) |
2 | 1 | reseq1i 5313 |
. . . 4
⊢ (arccos
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) |
3 | | dvasin.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
4 | | difss 3699 |
. . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ |
5 | 3, 4 | eqsstri 3598 |
. . . . 5
⊢ 𝐷 ⊆
ℂ |
6 | | resmpt 5369 |
. . . . 5
⊢ (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) |
7 | 5, 6 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥))) |
8 | 2, 7 | eqtri 2632 |
. . 3
⊢ (arccos
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥))) |
9 | 8 | oveq2i 6560 |
. 2
⊢ (ℂ
D (arccos ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) |
10 | | cnelprrecn 9908 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
12 | | halfpire 24020 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
13 | 12 | recni 9931 |
. . . . 5
⊢ (π /
2) ∈ ℂ |
14 | 13 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (π / 2)
∈ ℂ) |
15 | | c0ex 9913 |
. . . . 5
⊢ 0 ∈
V |
16 | 15 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 0 ∈
V) |
17 | 13 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (π / 2) ∈ ℂ) |
18 | 15 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 0 ∈ V) |
19 | 13 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (π / 2) ∈ ℂ) |
20 | 11, 19 | dvmptc 23527 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (π / 2))) = (𝑥 ∈ ℂ ↦ 0)) |
21 | 5 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐷 ⊆
ℂ) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
23 | 22 | cnfldtopon 22396 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
24 | 23 | toponunii 20547 |
. . . . . . . 8
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
25 | 24 | restid 15917 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
26 | 23, 25 | ax-mp 5 |
. . . . . 6
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
27 | 26 | eqcomi 2619 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
28 | 22 | recld2 22425 |
. . . . . . . . . 10
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) |
29 | | neg1rr 11002 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ |
30 | | iocmnfcld 22382 |
. . . . . . . . . . . 12
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) |
32 | 22 | tgioo2 22414 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
33 | 32 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
34 | 31, 33 | eleqtri 2686 |
. . . . . . . . . 10
⊢
(-∞(,]-1) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
35 | | restcldr 20788 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ (-∞(,]-1)
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → (-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld))) |
36 | 28, 34, 35 | mp2an 704 |
. . . . . . . . 9
⊢
(-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld)) |
37 | | 1re 9918 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
38 | | icopnfcld 22381 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) |
40 | 39, 33 | eleqtri 2686 |
. . . . . . . . . 10
⊢
(1[,)+∞) ∈ (Clsd‘((TopOpen‘ℂfld)
↾t ℝ)) |
41 | | restcldr 20788 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ (1[,)+∞)
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → (1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld))) |
42 | 28, 40, 41 | mp2an 704 |
. . . . . . . . 9
⊢
(1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld)) |
43 | | uncld 20655 |
. . . . . . . . 9
⊢
(((-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld)) ∧ (1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld))) → ((-∞(,]-1)
∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
44 | 36, 42, 43 | mp2an 704 |
. . . . . . . 8
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) |
45 | 24 | cldopn 20645 |
. . . . . . . 8
⊢
(((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . 7
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld) |
47 | 3, 46 | eqeltri 2684 |
. . . . . 6
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
48 | 47 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
49 | 11, 17, 18, 20, 21, 27, 22, 48 | dvmptres 23532 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (π / 2))) =
(𝑥 ∈ 𝐷 ↦ 0)) |
50 | 5 | sseli 3564 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
51 | | asincl 24400 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(arcsin‘𝑥) ∈
ℂ) |
52 | 50, 51 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (arcsin‘𝑥) ∈ ℂ) |
53 | 52 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(arcsin‘𝑥) ∈
ℂ) |
54 | | ovex 6577 |
. . . . 5
⊢ (1 /
(√‘(1 − (𝑥↑2)))) ∈ V |
55 | 54 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 /
(√‘(1 − (𝑥↑2)))) ∈ V) |
56 | 3 | dvasin 32666 |
. . . . 5
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |
57 | | asinf 24399 |
. . . . . . . 8
⊢
arcsin:ℂ⟶ℂ |
58 | 57 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ arcsin:ℂ⟶ℂ) |
59 | 58, 21 | feqresmpt 6160 |
. . . . . 6
⊢ (⊤
→ (arcsin ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥))) |
60 | 59 | oveq2d 6565 |
. . . . 5
⊢ (⊤
→ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥)))) |
61 | 56, 60 | syl5reqr 2659 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦
(arcsin‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2)))))) |
62 | 11, 14, 16, 49, 53, 55, 61 | dvmptsub 23536 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((π / 2)
− (arcsin‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ (0 − (1 /
(√‘(1 − (𝑥↑2))))))) |
63 | 62 | trud 1484 |
. 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) =
(𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1
− (𝑥↑2)))))) |
64 | | df-neg 10148 |
. . . 4
⊢ -(1 /
(√‘(1 − (𝑥↑2)))) = (0 − (1 /
(√‘(1 − (𝑥↑2))))) |
65 | | 1cnd 9935 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 1 ∈ ℂ) |
66 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
67 | 50 | sqcld 12868 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
68 | | subcl 10159 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) |
69 | 66, 67, 68 | sylancr 694 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) |
70 | 69 | sqrtcld 14024 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) |
71 | | eldifn 3695 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
72 | 71, 3 | eleq2s 2706 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
73 | | mnfxr 9975 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
74 | 29 | rexri 9976 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ* |
75 | | mnflt 11833 |
. . . . . . . . . . . . 13
⊢ (-1
∈ ℝ → -∞ < -1) |
76 | 29, 75 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ -∞
< -1 |
77 | | ubioc1 12098 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) |
78 | 73, 74, 76, 77 | mp3an 1416 |
. . . . . . . . . . 11
⊢ -1 ∈
(-∞(,]-1) |
79 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = -1 → (𝑥 ∈ (-∞(,]-1) ↔ -1 ∈
(-∞(,]-1))) |
80 | 78, 79 | mpbiri 247 |
. . . . . . . . . 10
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) |
81 | 37 | rexri 9976 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
82 | | pnfxr 9971 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
83 | | ltpnf 11830 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ → 1 < +∞) |
84 | 37, 83 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 1 <
+∞ |
85 | | lbico1 12099 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) |
86 | 81, 82, 84, 85 | mp3an 1416 |
. . . . . . . . . . 11
⊢ 1 ∈
(1[,)+∞) |
87 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ∈ (1[,)+∞) ↔ 1 ∈
(1[,)+∞))) |
88 | 86, 87 | mpbiri 247 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) |
89 | 80, 88 | orim12i 537 |
. . . . . . . . 9
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
90 | 89 | orcoms 403 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
91 | | elun 3715 |
. . . . . . . 8
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) |
92 | 90, 91 | sylibr 223 |
. . . . . . 7
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
93 | 72, 92 | nsyl 134 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) |
94 | | sq1 12820 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
95 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) |
96 | | sqcl 12787 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
97 | 96 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) |
98 | 66, 96, 68 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) |
99 | 98 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) |
100 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) |
101 | 99, 100 | sqr00d 14028 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) |
102 | 95, 97, 101 | subeq0d 10279 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) |
103 | 94, 102 | syl5req 2657 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) |
104 | 103 | ex 449 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) |
105 | | sqeqor 12840 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) |
106 | 66, 105 | mpan2 703 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) |
107 | 104, 106 | sylibd 228 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1))) |
108 | 107 | necon3bd 2796 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (¬
(𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1
− (𝑥↑2))) ≠
0)) |
109 | 50, 93, 108 | sylc 63 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠
0) |
110 | 65, 70, 109 | divnegd 10693 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → -(1 / (√‘(1 −
(𝑥↑2)))) = (-1 /
(√‘(1 − (𝑥↑2))))) |
111 | 64, 110 | syl5eqr 2658 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (0 − (1 / (√‘(1
− (𝑥↑2))))) =
(-1 / (√‘(1 − (𝑥↑2))))) |
112 | 111 | mpteq2ia 4668 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 −
(𝑥↑2))))) |
113 | 9, 63, 112 | 3eqtri 2636 |
1
⊢ (ℂ
D (arccos ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 −
(𝑥↑2))))) |