Proof of Theorem dvacos
| Step | Hyp | Ref
| Expression |
| 1 | | df-acos 26909 |
. . . . 5
⊢ arccos =
(𝑥 ∈ ℂ ↦
((π / 2) − (arcsin‘𝑥))) |
| 2 | 1 | reseq1i 5993 |
. . . 4
⊢ (arccos
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) |
| 3 | | dvasin.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
| 4 | | difss 4136 |
. . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ |
| 5 | 3, 4 | eqsstri 4030 |
. . . . 5
⊢ 𝐷 ⊆
ℂ |
| 6 | | resmpt 6055 |
. . . . 5
⊢ (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) |
| 7 | 5, 6 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ ℂ ↦ ((π /
2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥))) |
| 8 | 2, 7 | eqtri 2765 |
. . 3
⊢ (arccos
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥))) |
| 9 | 8 | oveq2i 7442 |
. 2
⊢ (ℂ
D (arccos ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) |
| 10 | | cnelprrecn 11248 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
| 11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 12 | | halfpire 26506 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
| 13 | 12 | recni 11275 |
. . . . 5
⊢ (π /
2) ∈ ℂ |
| 14 | 13 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (π / 2)
∈ ℂ) |
| 15 | | c0ex 11255 |
. . . . 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 25996 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (π / 2))) = (𝑥 ∈ ℂ ↦ 0)) |
| 21 | 5 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐷 ⊆
ℂ) |
| 22 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 23 | 22 | cnfldtopon 24803 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 24 | 23 | toponrestid 22927 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 25 | 22 | recld2 24836 |
. . . . . . . . . 10
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) |
| 26 | | neg1rr 12381 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ |
| 27 | | iocmnfcld 24789 |
. . . . . . . . . . . 12
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) |
| 28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) |
| 29 | | tgioo4 24826 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 30 | 29 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
| 31 | 28, 30 | eleqtri 2839 |
. . . . . . . . . 10
⊢
(-∞(,]-1) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
| 32 | | restcldr 23182 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ (-∞(,]-1)
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → (-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 33 | 25, 31, 32 | mp2an 692 |
. . . . . . . . 9
⊢
(-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld)) |
| 34 | | 1re 11261 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
| 35 | | icopnfcld 24788 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) |
| 37 | 36, 30 | eleqtri 2839 |
. . . . . . . . . 10
⊢
(1[,)+∞) ∈ (Clsd‘((TopOpen‘ℂfld)
↾t ℝ)) |
| 38 | | restcldr 23182 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ (1[,)+∞)
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → (1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 39 | 25, 37, 38 | mp2an 692 |
. . . . . . . . 9
⊢
(1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld)) |
| 40 | | uncld 23049 |
. . . . . . . . 9
⊢
(((-∞(,]-1) ∈
(Clsd‘(TopOpen‘ℂfld)) ∧ (1[,)+∞) ∈
(Clsd‘(TopOpen‘ℂfld))) → ((-∞(,]-1)
∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 41 | 33, 39, 40 | mp2an 692 |
. . . . . . . 8
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) |
| 42 | 23 | toponunii 22922 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 43 | 42 | cldopn 23039 |
. . . . . . . 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 2837 |
. . . . . 6
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
| 46 | 45 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
| 47 | 11, 17, 18, 20, 21, 24, 22, 46 | dvmptres 26001 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (π / 2))) =
(𝑥 ∈ 𝐷 ↦ 0)) |
| 48 | 5 | sseli 3979 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
| 49 | | asincl 26916 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(arcsin‘𝑥) ∈
ℂ) |
| 50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (arcsin‘𝑥) ∈ ℂ) |
| 51 | 50 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(arcsin‘𝑥) ∈
ℂ) |
| 52 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 /
(√‘(1 − (𝑥↑2)))) ∈ V) |
| 53 | | asinf 26915 |
. . . . . . . 8
⊢
arcsin:ℂ⟶ℂ |
| 54 | 53 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ arcsin:ℂ⟶ℂ) |
| 55 | 54, 21 | feqresmpt 6978 |
. . . . . 6
⊢ (⊤
→ (arcsin ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥))) |
| 56 | 55 | oveq2d 7447 |
. . . . 5
⊢ (⊤
→ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥)))) |
| 57 | 3 | dvasin 37711 |
. . . . 5
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |
| 58 | 56, 57 | eqtr3di 2792 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦
(arcsin‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2)))))) |
| 59 | 11, 14, 16, 47, 51, 52, 58 | dvmptsub 26005 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((π / 2)
− (arcsin‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ (0 − (1 /
(√‘(1 − (𝑥↑2))))))) |
| 60 | 59 | mptru 1547 |
. 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ ((π / 2) −
(arcsin‘𝑥)))) =
(𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1
− (𝑥↑2)))))) |
| 61 | | df-neg 11495 |
. . . 4
⊢ -(1 /
(√‘(1 − (𝑥↑2)))) = (0 − (1 /
(√‘(1 − (𝑥↑2))))) |
| 62 | | 1cnd 11256 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 1 ∈ ℂ) |
| 63 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 64 | 48 | sqcld 14184 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
| 65 | | subcl 11507 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) |
| 66 | 63, 64, 65 | sylancr 587 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) |
| 67 | 66 | sqrtcld 15476 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) |
| 68 | | eldifn 4132 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
| 69 | 68, 3 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
| 70 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 71 | 26 | rexri 11319 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ* |
| 72 | | mnflt 13165 |
. . . . . . . . . . . . 13
⊢ (-1
∈ ℝ → -∞ < -1) |
| 73 | 26, 72 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ -∞
< -1 |
| 74 | | ubioc1 13440 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) |
| 75 | 70, 71, 73, 74 | mp3an 1463 |
. . . . . . . . . . 11
⊢ -1 ∈
(-∞(,]-1) |
| 76 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = -1 → (𝑥 ∈ (-∞(,]-1) ↔ -1 ∈
(-∞(,]-1))) |
| 77 | 75, 76 | mpbiri 258 |
. . . . . . . . . 10
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) |
| 78 | 34 | rexri 11319 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
| 79 | | pnfxr 11315 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
| 80 | | ltpnf 13162 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ → 1 < +∞) |
| 81 | 34, 80 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 1 <
+∞ |
| 82 | | lbico1 13441 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) |
| 83 | 78, 79, 81, 82 | mp3an 1463 |
. . . . . . . . . . 11
⊢ 1 ∈
(1[,)+∞) |
| 84 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ∈ (1[,)+∞) ↔ 1 ∈
(1[,)+∞))) |
| 85 | 83, 84 | mpbiri 258 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) |
| 86 | 77, 85 | orim12i 909 |
. . . . . . . . 9
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
| 87 | 86 | orcoms 873 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
| 88 | | elun 4153 |
. . . . . . . 8
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) |
| 89 | 87, 88 | sylibr 234 |
. . . . . . 7
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
| 90 | 69, 89 | nsyl 140 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) |
| 91 | | sq1 14234 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
| 92 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) |
| 93 | | sqcl 14158 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) |
| 95 | 63, 93, 65 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) |
| 96 | 95 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) |
| 97 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) |
| 98 | 96, 97 | sqr00d 15480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) |
| 99 | 92, 94, 98 | subeq0d 11628 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) |
| 100 | 91, 99 | eqtr2id 2790 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) |
| 101 | 100 | ex 412 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) |
| 102 | | sqeqor 14255 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) |
| 103 | 63, 102 | mpan2 691 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) |
| 104 | 101, 103 | sylibd 239 |
. . . . . . 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 12056 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → -(1 / (√‘(1 −
(𝑥↑2)))) = (-1 /
(√‘(1 − (𝑥↑2))))) |
| 108 | 61, 107 | eqtr3id 2791 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (0 − (1 / (√‘(1
− (𝑥↑2))))) =
(-1 / (√‘(1 − (𝑥↑2))))) |
| 109 | 108 | mpteq2ia 5245 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 −
(𝑥↑2))))) |
| 110 | 9, 60, 109 | 3eqtri 2769 |
1
⊢ (ℂ
D (arccos ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 −
(𝑥↑2))))) |