Proof of Theorem dvacos
Step | Hyp | Ref
| Expression |
1 | | df-acos 26122 |
. . . . 5
⊢ arccos =
(𝑥 ∈ ℂ ↦
((π / 2) − (arcsin‘𝑥))) |
2 | 1 | reseq1i 5919 |
. . . 4
⊢ (arccos
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) |
3 | | dvasin.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
4 | | difss 4078 |
. . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ |
5 | 3, 4 | eqsstri 3966 |
. . . . 5
⊢ 𝐷 ⊆
ℂ |
6 | | resmpt 5977 |
. . . . 5
⊢ (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) |
7 | 5, 6 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥))) |
8 | 2, 7 | eqtri 2764 |
. . 3
⊢ (arccos
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥))) |
9 | 8 | oveq2i 7348 |
. 2
⊢ (ℂ
D (arccos ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) |
10 | | cnelprrecn 11065 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
12 | | halfpire 25727 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
13 | 12 | recni 11090 |
. . . . 5
⊢ (π /
2) ∈ ℂ |
14 | 13 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (π / 2)
∈ ℂ) |
15 | | c0ex 11070 |
. . . . 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 25228 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (π / 2))) = (𝑥 ∈ ℂ ↦ 0)) |
21 | 5 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐷 ⊆
ℂ) |
22 | | eqid 2736 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
23 | 22 | cnfldtopon 24052 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
24 | 23 | toponrestid 22176 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
25 | 22 | recld2 24083 |
. . . . . . . . . 10
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) |
26 | | neg1rr 12189 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ |
27 | | iocmnfcld 24038 |
. . . . . . . . . . . 12
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) |
29 | 22 | tgioo2 24072 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
30 | 29 | fveq2i 6828 |
. . . . . . . . . . 11
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
31 | 28, 30 | eleqtri 2835 |
. . . . . . . . . 10
⊢
(-∞(,]-1) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
32 | | restcldr 22431 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ (-∞(,]-1)
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → (-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld))) |
33 | 25, 31, 32 | mp2an 689 |
. . . . . . . . 9
⊢
(-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld)) |
34 | | 1re 11076 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
35 | | icopnfcld 24037 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) |
37 | 36, 30 | eleqtri 2835 |
. . . . . . . . . 10
⊢
(1[,)+∞) ∈ (Clsd‘((TopOpen‘ℂfld)
↾t ℝ)) |
38 | | restcldr 22431 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ (1[,)+∞)
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → (1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld))) |
39 | 25, 37, 38 | mp2an 689 |
. . . . . . . . 9
⊢
(1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld)) |
40 | | uncld 22298 |
. . . . . . . . 9
⊢
(((-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld)) ∧ (1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld))) → ((-∞(,]-1)
∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
41 | 33, 39, 40 | mp2an 689 |
. . . . . . . 8
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) |
42 | 23 | toponunii 22171 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
43 | 42 | cldopn 22288 |
. . . . . . . 8
⊢
(((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld)) |
44 | 41, 43 | ax-mp 5 |
. . . . . . 7
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld) |
45 | 3, 44 | eqeltri 2833 |
. . . . . 6
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
46 | 45 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
47 | 11, 17, 18, 20, 21, 24, 22, 46 | dvmptres 25233 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (π / 2))) =
(𝑥 ∈ 𝐷 ↦ 0)) |
48 | 5 | sseli 3928 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
49 | | asincl 26129 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(arcsin‘𝑥) ∈
ℂ) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (arcsin‘𝑥) ∈ ℂ) |
51 | 50 | adantl 482 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(arcsin‘𝑥) ∈
ℂ) |
52 | | ovexd 7372 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 /
(√‘(1 − (𝑥↑2)))) ∈ V) |
53 | | asinf 26128 |
. . . . . . . 8
⊢
arcsin:ℂ⟶ℂ |
54 | 53 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ arcsin:ℂ⟶ℂ) |
55 | 54, 21 | feqresmpt 6894 |
. . . . . 6
⊢ (⊤
→ (arcsin ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥))) |
56 | 55 | oveq2d 7353 |
. . . . 5
⊢ (⊤
→ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥)))) |
57 | 3 | dvasin 35974 |
. . . . 5
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |
58 | 56, 57 | eqtr3di 2791 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦
(arcsin‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2)))))) |
59 | 11, 14, 16, 47, 51, 52, 58 | dvmptsub 25237 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((π / 2)
− (arcsin‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ (0 − (1 /
(√‘(1 − (𝑥↑2))))))) |
60 | 59 | mptru 1547 |
. 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) =
(𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1
− (𝑥↑2)))))) |
61 | | df-neg 11309 |
. . . 4
⊢ -(1 /
(√‘(1 − (𝑥↑2)))) = (0 − (1 /
(√‘(1 − (𝑥↑2))))) |
62 | | 1cnd 11071 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 1 ∈ ℂ) |
63 | | ax-1cn 11030 |
. . . . . . 7
⊢ 1 ∈
ℂ |
64 | 48 | sqcld 13963 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
65 | | subcl 11321 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) |
66 | 63, 64, 65 | sylancr 587 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) |
67 | 66 | sqrtcld 15248 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) |
68 | | eldifn 4074 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
69 | 68, 3 | eleq2s 2855 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
70 | | mnfxr 11133 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
71 | 26 | rexri 11134 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ* |
72 | | mnflt 12960 |
. . . . . . . . . . . . 13
⊢ (-1
∈ ℝ → -∞ < -1) |
73 | 26, 72 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ -∞
< -1 |
74 | | ubioc1 13233 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) |
75 | 70, 71, 73, 74 | mp3an 1460 |
. . . . . . . . . . 11
⊢ -1 ∈
(-∞(,]-1) |
76 | | eleq1 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = -1 → (𝑥 ∈ (-∞(,]-1) ↔ -1 ∈
(-∞(,]-1))) |
77 | 75, 76 | mpbiri 257 |
. . . . . . . . . 10
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) |
78 | 34 | rexri 11134 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
79 | | pnfxr 11130 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
80 | | ltpnf 12957 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ → 1 < +∞) |
81 | 34, 80 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 1 <
+∞ |
82 | | lbico1 13234 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) |
83 | 78, 79, 81, 82 | mp3an 1460 |
. . . . . . . . . . 11
⊢ 1 ∈
(1[,)+∞) |
84 | | eleq1 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ∈ (1[,)+∞) ↔ 1 ∈
(1[,)+∞))) |
85 | 83, 84 | mpbiri 257 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) |
86 | 77, 85 | orim12i 906 |
. . . . . . . . 9
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
87 | 86 | orcoms 869 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
88 | | elun 4095 |
. . . . . . . 8
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) |
89 | 87, 88 | sylibr 233 |
. . . . . . 7
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
90 | 69, 89 | nsyl 140 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) |
91 | | sq1 14013 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
92 | | 1cnd 11071 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) |
93 | | sqcl 13939 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
94 | 93 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) |
95 | 63, 93, 65 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) |
96 | 95 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) |
97 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) |
98 | 96, 97 | sqr00d 15252 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) |
99 | 92, 94, 98 | subeq0d 11441 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) |
100 | 91, 99 | eqtr2id 2789 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) |
101 | 100 | ex 413 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) |
102 | | sqeqor 14033 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) |
103 | 63, 102 | mpan2 688 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) |
104 | 101, 103 | sylibd 238 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1))) |
105 | 104 | necon3bd 2954 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (¬
(𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1
− (𝑥↑2))) ≠
0)) |
106 | 48, 90, 105 | sylc 65 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠
0) |
107 | 62, 67, 106 | divnegd 11865 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → -(1 / (√‘(1 −
(𝑥↑2)))) = (-1 /
(√‘(1 − (𝑥↑2))))) |
108 | 61, 107 | eqtr3id 2790 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (0 − (1 / (√‘(1
− (𝑥↑2))))) =
(-1 / (√‘(1 − (𝑥↑2))))) |
109 | 108 | mpteq2ia 5195 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 −
(𝑥↑2))))) |
110 | 9, 60, 109 | 3eqtri 2768 |
1
⊢ (ℂ
D (arccos ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 −
(𝑥↑2))))) |