Step | Hyp | Ref
| Expression |
1 | | reelprrecn 9907 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ ℝ ∈ {ℝ, ℂ}) |
3 | | elioore 12076 |
. . . . . . . 8
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ) |
4 | 3 | recnd 9947 |
. . . . . . 7
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ) |
6 | | rpcn 11717 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ) |
8 | | rpne0 11724 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0) |
10 | 5, 7, 9 | divcld 10680 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ) |
11 | | asincl 24400 |
. . . . 5
⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ) |
13 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ) |
14 | 10 | sqcld 12868 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ) |
15 | 13, 14 | subcld 10271 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ) |
16 | 15 | sqrtcld 14024 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ) |
17 | 10, 16 | mulcld 9939 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
18 | 12, 17 | addcld 9938 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈
ℂ) |
19 | | ovex 6577 |
. . . 4
⊢ ((2
· (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V |
20 | 19 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V) |
21 | | rpre 11715 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
22 | 21 | renegcld 10336 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ) |
23 | 22 | rexrd 9968 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ*) |
24 | | rpxr 11716 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
25 | | elioo2 12087 |
. . . . . . . 8
⊢ ((-𝑅 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
26 | 23, 24, 25 | syl2anc 691 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
27 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℝ) |
28 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ) |
29 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ≠
0) |
30 | 27, 28, 29 | redivcld 10732 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 / 𝑅) ∈
ℝ) |
31 | 30 | a1d 25 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ)) |
32 | 6 | mulm1d 10361 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (-1 · 𝑅) =
-𝑅) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-1 · 𝑅) =
-𝑅) |
34 | 33 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-1 · 𝑅)
< 𝑡 ↔ -𝑅 < 𝑡)) |
35 | | neg1rr 11002 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℝ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ -1 ∈ ℝ) |
37 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ+) |
38 | 36, 27, 37 | ltmuldivd 11795 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-1 · 𝑅)
< 𝑡 ↔ -1 <
(𝑡 / 𝑅))) |
39 | 34, 38 | bitr3d 269 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅))) |
40 | 39 | biimpd 218 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅))) |
41 | 40 | adantrd 483 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → -1 < (𝑡 / 𝑅))) |
42 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℝ) |
43 | 27, 42, 37 | ltdivmuld 11799 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1))) |
44 | 6 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (𝑅 · 1) =
𝑅) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅 · 1) =
𝑅) |
46 | 45 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅)) |
47 | 43, 46 | bitr2d 268 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1)) |
48 | 47 | biimpd 218 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1)) |
49 | 48 | adantld 482 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (𝑡 / 𝑅) < 1)) |
50 | 31, 41, 49 | 3jcad 1236 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
51 | 50 | exp4b 630 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))))) |
52 | 51 | 3impd 1273 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
53 | 26, 52 | sylbid 229 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
54 | 53 | imp 444 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)) |
55 | 35 | rexri 9976 |
. . . . . 6
⊢ -1 ∈
ℝ* |
56 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
57 | 56 | rexri 9976 |
. . . . . 6
⊢ 1 ∈
ℝ* |
58 | | elioo2 12087 |
. . . . . 6
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
59 | 55, 57, 58 | mp2an 704 |
. . . . 5
⊢ ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)) |
60 | 54, 59 | sylibr 223 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1)) |
61 | | ovex 6577 |
. . . . 5
⊢ (1 /
𝑅) ∈
V |
62 | 61 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V) |
63 | | elioore 12076 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → 𝑢 ∈
ℝ) |
64 | 63 | recnd 9947 |
. . . . . 6
⊢ (𝑢 ∈ (-1(,)1) → 𝑢 ∈
ℂ) |
65 | | asincl 24400 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ →
(arcsin‘𝑢) ∈
ℂ) |
66 | | id 22 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ → 𝑢 ∈
ℂ) |
67 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → 1 ∈
ℂ) |
68 | | sqcl 12787 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → (𝑢↑2) ∈
ℂ) |
69 | 67, 68 | subcld 10271 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℂ → (1
− (𝑢↑2)) ∈
ℂ) |
70 | 69 | sqrtcld 14024 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ →
(√‘(1 − (𝑢↑2))) ∈ ℂ) |
71 | 66, 70 | mulcld 9939 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ → (𝑢 · (√‘(1
− (𝑢↑2))))
∈ ℂ) |
72 | 65, 71 | addcld 9938 |
. . . . . 6
⊢ (𝑢 ∈ ℂ →
((arcsin‘𝑢) + (𝑢 · (√‘(1
− (𝑢↑2)))))
∈ ℂ) |
73 | 64, 72 | syl 17 |
. . . . 5
⊢ (𝑢 ∈ (-1(,)1) →
((arcsin‘𝑢) + (𝑢 · (√‘(1
− (𝑢↑2)))))
∈ ℂ) |
74 | 73 | adantl 481 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ ((arcsin‘𝑢) +
(𝑢 ·
(√‘(1 − (𝑢↑2))))) ∈ ℂ) |
75 | | ovex 6577 |
. . . . 5
⊢ (2
· (√‘(1 − (𝑢↑2)))) ∈ V |
76 | 75 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (2 · (√‘(1 − (𝑢↑2)))) ∈ V) |
77 | | recn 9905 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℂ) |
78 | 77 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℂ) |
79 | | 1cnd 9935 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℂ) |
80 | 2 | dvmptid 23526 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
ℝ ↦ 𝑡)) =
(𝑡 ∈ ℝ ↦
1)) |
81 | | ioossre 12106 |
. . . . . . 7
⊢ (-𝑅(,)𝑅) ⊆ ℝ |
82 | 81 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (-𝑅(,)𝑅) ⊆
ℝ) |
83 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
84 | 83 | tgioo2 22414 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
85 | | iooretop 22379 |
. . . . . . 7
⊢ (-𝑅(,)𝑅) ∈ (topGen‘ran
(,)) |
86 | 85 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (-𝑅(,)𝑅) ∈ (topGen‘ran
(,))) |
87 | 2, 78, 79, 80, 82, 84, 83, 86 | dvmptres 23532 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1)) |
88 | 2, 5, 13, 87, 6, 8 | dvmptdivc 23534 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅))) |
89 | 64, 65 | syl 17 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) →
(arcsin‘𝑢) ∈
ℂ) |
90 | 89 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (arcsin‘𝑢)
∈ ℂ) |
91 | | ovex 6577 |
. . . . . . 7
⊢ (1 /
(√‘(1 − (𝑢↑2)))) ∈ V |
92 | 91 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (1 / (√‘(1 − (𝑢↑2)))) ∈ V) |
93 | | dvreasin 32668 |
. . . . . . 7
⊢ (ℝ
D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 /
(√‘(1 − (𝑢↑2))))) |
94 | | asinf 24399 |
. . . . . . . . . 10
⊢
arcsin:ℂ⟶ℂ |
95 | 94 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ arcsin:ℂ⟶ℂ) |
96 | | ioossre 12106 |
. . . . . . . . . . 11
⊢ (-1(,)1)
⊆ ℝ |
97 | | ax-resscn 9872 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
98 | 96, 97 | sstri 3577 |
. . . . . . . . . 10
⊢ (-1(,)1)
⊆ ℂ |
99 | 98 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ⊆ ℂ) |
100 | 95, 99 | feqresmpt 6160 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) |
101 | 100 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))) |
102 | 93, 101 | syl5reqr 2659 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 /
(√‘(1 − (𝑢↑2)))))) |
103 | 64, 71 | syl 17 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1
− (𝑢↑2))))
∈ ℂ) |
104 | 103 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (𝑢 ·
(√‘(1 − (𝑢↑2)))) ∈ ℂ) |
105 | | ovex 6577 |
. . . . . . 7
⊢ ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V |
106 | 105 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V) |
107 | 64 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ 𝑢 ∈
ℂ) |
108 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ 1 ∈ ℂ) |
109 | | recn 9905 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ → 𝑢 ∈
ℂ) |
110 | 109 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 𝑢 ∈
ℂ) |
111 | | 1cnd 9935 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 1 ∈ ℂ) |
112 | 2 | dvmptid 23526 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ 𝑢)) =
(𝑢 ∈ ℝ ↦
1)) |
113 | 96 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ⊆ ℝ) |
114 | | iooretop 22379 |
. . . . . . . . 9
⊢ (-1(,)1)
∈ (topGen‘ran (,)) |
115 | 114 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ∈ (topGen‘ran (,))) |
116 | 2, 110, 111, 112, 113, 84, 83, 115 | dvmptres 23532 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ 𝑢)) =
(𝑢 ∈ (-1(,)1) ↦
1)) |
117 | 64, 70 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) ∈ ℂ) |
118 | 117 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (√‘(1 − (𝑢↑2))) ∈ ℂ) |
119 | | ovex 6577 |
. . . . . . . 8
⊢ (-𝑢 / (√‘(1 −
(𝑢↑2)))) ∈
V |
120 | 119 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (-𝑢 /
(√‘(1 − (𝑢↑2)))) ∈ V) |
121 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → 1 ∈
ℝ) |
122 | 63 | resqcld 12897 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈
ℝ) |
123 | 121, 122 | resubcld 10337 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℝ) |
124 | | elioo2 12087 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1))) |
125 | 55, 57, 124 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1)) |
126 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → 𝑢 ∈
ℝ) |
127 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → 1 ∈
ℝ) |
128 | 126, 127 | absltd 14016 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ (-1 < 𝑢 ∧
𝑢 <
1))) |
129 | 109 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
(abs‘𝑢) ∈
ℝ) |
130 | 109 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → 0 ≤
(abs‘𝑢)) |
131 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
1 |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → 0 ≤
1) |
133 | 129, 127,
130, 132 | lt2sqd 12905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ ((abs‘𝑢)↑2) < (1↑2))) |
134 | | absresq 13890 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢)↑2) =
(𝑢↑2)) |
135 | | sq1 12820 |
. . . . . . . . . . . . . . . . . 18
⊢
(1↑2) = 1 |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
(1↑2) = 1) |
137 | 134, 136 | breq12d 4596 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ →
(((abs‘𝑢)↑2)
< (1↑2) ↔ (𝑢↑2) < 1)) |
138 | | resqcl 12793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → (𝑢↑2) ∈
ℝ) |
139 | 138, 127 | posdifd 10493 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1
− (𝑢↑2)))) |
140 | 133, 137,
139 | 3bitrd 293 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ 0 < (1 − (𝑢↑2)))) |
141 | 128, 140 | bitr3d 269 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ℝ → ((-1 <
𝑢 ∧ 𝑢 < 1) ↔ 0 < (1 − (𝑢↑2)))) |
142 | 141 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℝ → ((-1 <
𝑢 ∧ 𝑢 < 1) → 0 < (1 − (𝑢↑2)))) |
143 | 142 | 3impib 1254 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1) → 0 < (1 − (𝑢↑2))) |
144 | 125, 143 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 0 <
(1 − (𝑢↑2))) |
145 | 123, 144 | elrpd 11745 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℝ+) |
146 | 145 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (1 − (𝑢↑2)) ∈
ℝ+) |
147 | | negex 10158 |
. . . . . . . . . 10
⊢ -(2
· 𝑢) ∈
V |
148 | 147 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ -(2 · 𝑢)
∈ V) |
149 | | rpcn 11717 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ℝ+
→ 𝑣 ∈
ℂ) |
150 | 149 | sqrtcld 14024 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ℝ+
→ (√‘𝑣)
∈ ℂ) |
151 | 150 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → (√‘𝑣) ∈ ℂ) |
152 | | ovex 6577 |
. . . . . . . . . 10
⊢ (1 / (2
· (√‘𝑣))) ∈ V |
153 | 152 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V) |
154 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℝ → 1 ∈
ℂ) |
155 | 109 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℝ → (𝑢↑2) ∈
ℂ) |
156 | 154, 155 | subcld 10271 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ → (1
− (𝑢↑2)) ∈
ℂ) |
157 | 156 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (1 − (𝑢↑2)) ∈ ℂ) |
158 | 147 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ -(2 · 𝑢)
∈ V) |
159 | | 0red 9920 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 0 ∈ ℝ) |
160 | | 1cnd 9935 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ 1 ∈ ℂ) |
161 | 2, 160 | dvmptc 23527 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ 1)) = (𝑢
∈ ℝ ↦ 0)) |
162 | 155 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (𝑢↑2) ∈
ℂ) |
163 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (2
· 𝑢) ∈
V |
164 | 163 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (2 · 𝑢)
∈ V) |
165 | 83 | cnfldtopon 22396 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
166 | | toponmax 20543 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
167 | 165, 166 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ℂ ∈ (TopOpen‘ℂfld)) |
168 | | df-ss 3554 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
169 | 97, 168 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢ (ℝ
∩ ℂ) = ℝ |
170 | 169 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℝ ∩ ℂ) = ℝ) |
171 | 68 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℂ)
→ (𝑢↑2) ∈
ℂ) |
172 | 163 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℂ)
→ (2 · 𝑢)
∈ V) |
173 | | 2nn 11062 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
174 | | dvexp 23522 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 −
1))))) |
175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑢 ∈ ℂ ↦
(𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2
· (𝑢↑(2 −
1)))) |
176 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
177 | 176 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢↑(2 − 1)) = (𝑢↑1) |
178 | | exp1 12728 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢) |
179 | 177, 178 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢) |
180 | 179 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℂ → (2
· (𝑢↑(2 −
1))) = (2 · 𝑢)) |
181 | 180 | mpteq2ia 4668 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ ↦ (2
· (𝑢↑(2 −
1)))) = (𝑢 ∈ ℂ
↦ (2 · 𝑢)) |
182 | 175, 181 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑢 ∈ ℂ ↦
(𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2
· 𝑢)) |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℂ D (𝑢 ∈
ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))) |
184 | 83, 2, 167, 170, 171, 172, 183 | dvmptres3 23525 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢))) |
185 | 2, 111, 159, 161, 162, 164, 184 | dvmptsub 23536 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2
· 𝑢)))) |
186 | | df-neg 10148 |
. . . . . . . . . . . 12
⊢ -(2
· 𝑢) = (0 − (2
· 𝑢)) |
187 | 186 | mpteq2i 4669 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ ↦ -(2
· 𝑢)) = (𝑢 ∈ ℝ ↦ (0
− (2 · 𝑢))) |
188 | 185, 187 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢))) |
189 | 2, 157, 158, 188, 113, 84, 83, 115 | dvmptres 23532 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢))) |
190 | | dvsqrt 24283 |
. . . . . . . . . 10
⊢ (ℝ
D (𝑣 ∈
ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑣)))) |
191 | 190 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑣 ∈
ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑣))))) |
192 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = (1 − (𝑢↑2)) →
(√‘𝑣) =
(√‘(1 − (𝑢↑2)))) |
193 | 192 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑣 = (1 − (𝑢↑2)) → (2 ·
(√‘𝑣)) = (2
· (√‘(1 − (𝑢↑2))))) |
194 | 193 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑣 = (1 − (𝑢↑2)) → (1 / (2
· (√‘𝑣))) = (1 / (2 · (√‘(1
− (𝑢↑2)))))) |
195 | 2, 2, 146, 148, 151, 153, 189, 191, 192, 194 | dvmptco 23541 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 ·
(√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))) |
196 | | 2cnd 10970 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → 2 ∈
ℂ) |
197 | 196, 64 | mulneg2d 10363 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· -𝑢) = -(2 ·
𝑢)) |
198 | 197 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((2
· -𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 ·
(√‘(1 − (𝑢↑2)))))) |
199 | 64 | negcld 10258 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -𝑢 ∈
ℂ) |
200 | 144 | gt0ne0d 10471 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ≠
0) |
201 | 64, 69 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℂ) |
202 | 201 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈
ℂ) |
203 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (√‘(1
− (𝑢↑2))) =
0) |
204 | 202, 203 | sqr00d 14028 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0) |
205 | 204 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0)) |
206 | 205 | necon3d 2803 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → ((1
− (𝑢↑2)) ≠ 0
→ (√‘(1 − (𝑢↑2))) ≠ 0)) |
207 | 200, 206 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) ≠ 0) |
208 | | 2ne0 10990 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
209 | 208 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 2 ≠
0) |
210 | 199, 117,
196, 207, 209 | divcan5d 10706 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((2
· -𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2))))) |
211 | 196, 64 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (2
· 𝑢) ∈
ℂ) |
212 | 211 | negcld 10258 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -(2
· 𝑢) ∈
ℂ) |
213 | 196, 117 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) ∈ ℂ) |
214 | 196, 117,
209, 207 | mulne0d 10558 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) ≠ 0) |
215 | 212, 213,
214 | divrec2d 10684 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (-(2
· 𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = ((1 / (2 ·
(√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) |
216 | 198, 210,
215 | 3eqtr3rd 2653 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → ((1 / (2
· (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2))))) |
217 | 216 | mpteq2ia 4668 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) ↦ ((1 /
(2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))) |
218 | 195, 217 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
219 | 2, 107, 108, 116, 118, 120, 218 | dvmptmul 23530 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (𝑢
· (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 ·
(√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) |
220 | 2, 90, 92, 102, 104, 106, 219 | dvmptadd 23529 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))))) |
221 | 117 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (1
· (√‘(1 − (𝑢↑2)))) = (√‘(1 −
(𝑢↑2)))) |
222 | 199, 117,
207 | divcld 10680 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 −
(𝑢↑2)))) ∈
ℂ) |
223 | 222, 64 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 −
(𝑢↑2)))) ·
𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
224 | 64, 199, 117, 207 | divassd 10715 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
225 | 64, 64 | mulneg2d 10363 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢)) |
226 | 64 | sqvald 12867 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢)) |
227 | 226 | negeqd 10154 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢)) |
228 | 225, 227 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2)) |
229 | 228 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1
− (𝑢↑2))))) |
230 | 223, 224,
229 | 3eqtr2d 2650 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 −
(𝑢↑2)))) ·
𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) |
231 | 221, 230 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 −
(𝑢↑2))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
232 | 64 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈
ℂ) |
233 | 232 | negcld 10258 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈
ℂ) |
234 | 233, 117,
207 | divcld 10680 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1
− (𝑢↑2))))
∈ ℂ) |
235 | 117, 234 | addcomd 10117 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1
− (𝑢↑2)))) +
(√‘(1 − (𝑢↑2))))) |
236 | 231, 235 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2))))) |
237 | 236 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))) = ((1 /
(√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2)))))) |
238 | 117 | 2timesd 11152 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) = ((√‘(1 −
(𝑢↑2))) +
(√‘(1 − (𝑢↑2))))) |
239 | 67, 68 | negsubd 10277 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ → (1 +
-(𝑢↑2)) = (1 −
(𝑢↑2))) |
240 | 69 | sqsqrtd 14026 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ →
((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2))) |
241 | 70 | sqvald 12867 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ →
((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1
− (𝑢↑2)))
· (√‘(1 − (𝑢↑2))))) |
242 | 239, 240,
241 | 3eqtr2d 2650 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℂ → (1 +
-(𝑢↑2)) =
((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2))))) |
243 | 64, 242 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (1 +
-(𝑢↑2)) =
((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2))))) |
244 | 243 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((1 +
-(𝑢↑2)) /
(√‘(1 − (𝑢↑2)))) = (((√‘(1 −
(𝑢↑2))) ·
(√‘(1 − (𝑢↑2)))) / (√‘(1 −
(𝑢↑2))))) |
245 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 1 ∈
ℂ) |
246 | 245, 233,
117, 207 | divdird 10718 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((1 +
-(𝑢↑2)) /
(√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 −
(𝑢↑2)))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
247 | 117, 117,
207 | divcan3d 10685 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) →
(((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2)))) /
(√‘(1 − (𝑢↑2)))) = (√‘(1 −
(𝑢↑2)))) |
248 | 244, 246,
247 | 3eqtr3rd 2653 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 −
(𝑢↑2)))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
249 | 248 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 /
(√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1
− (𝑢↑2))))) |
250 | 117, 207 | reccld 10673 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → (1 /
(√‘(1 − (𝑢↑2)))) ∈ ℂ) |
251 | 250, 234,
117 | addassd 9941 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → (((1 /
(√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1
− (𝑢↑2)))) = ((1
/ (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2)))))) |
252 | 238, 249,
251 | 3eqtrrd 2649 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2))))) = (2
· (√‘(1 − (𝑢↑2))))) |
253 | 237, 252 | eqtrd 2644 |
. . . . . 6
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))) = (2 ·
(√‘(1 − (𝑢↑2))))) |
254 | 253 | mpteq2ia 4668 |
. . . . 5
⊢ (𝑢 ∈ (-1(,)1) ↦ ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2
· (√‘(1 − (𝑢↑2))))) |
255 | 220, 254 | syl6eq 2660 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2
· (√‘(1 − (𝑢↑2)))))) |
256 | | fveq2 6103 |
. . . . 5
⊢ (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅))) |
257 | | id 22 |
. . . . . 6
⊢ (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅)) |
258 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2)) |
259 | 258 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2))) |
260 | 259 | fveq2d 6107 |
. . . . . 6
⊢ (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1
− ((𝑡 / 𝑅)↑2)))) |
261 | 257, 260 | oveq12d 6567 |
. . . . 5
⊢ (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
262 | 256, 261 | oveq12d 6567 |
. . . 4
⊢ (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) =
((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
263 | 260 | oveq2d 6565 |
. . . 4
⊢ (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1
− (𝑢↑2)))) = (2
· (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
264 | 2, 2, 60, 62, 74, 76, 88, 255, 262, 263 | dvmptco 23541 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) |
265 | 6 | sqcld 12868 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) |
266 | 2, 18, 20, 264, 265 | dvmptcmul 23533 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))) |
267 | | 2cnd 10970 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ) |
268 | 267, 16 | mulcld 9939 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
269 | 6, 8 | reccld 10673 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (1 / 𝑅) ∈
ℂ) |
270 | 269 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ) |
271 | 268, 270 | mulcomd 9940 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))))) |
272 | 271 | oveq2d 6565 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))))) |
273 | 265 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ) |
274 | 273, 270,
268 | mulassd 9942 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))))) |
275 | 6 | sqvald 12867 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) = (𝑅 · 𝑅)) |
276 | 275 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅)) |
277 | 265, 6, 8 | divrecd 10683 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅))) |
278 | 6, 6, 8 | divcan3d 10685 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 · 𝑅) / 𝑅) = 𝑅) |
279 | 276, 277,
278 | 3eqtr3d 2652 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
(1 / 𝑅)) = 𝑅) |
280 | 279 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅) |
281 | 280 | oveq1d 6564 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
282 | 7, 267, 16 | mul12d 10124 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (2 ·
(𝑅 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
283 | 21 | resqcld 12897 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ) |
284 | 283 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ) |
285 | 21 | sqge0d 12898 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ (𝑅↑2)) |
286 | 285 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2)) |
287 | | 1red 9934 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ) |
288 | 3 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ) |
289 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ) |
290 | 288, 289,
9 | redivcld 10732 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ) |
291 | 290 | resqcld 12897 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ) |
292 | 287, 291 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ) |
293 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ) |
294 | 27, 28 | absltd 14016 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
295 | 77 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ →
(abs‘𝑡) ∈
ℝ) |
296 | 295 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (abs‘𝑡) ∈
ℝ) |
297 | 77 | absge0d 14031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ → 0 ≤
(abs‘𝑡)) |
298 | 297 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘𝑡)) |
299 | | rpge0 11721 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
300 | 299 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ 𝑅) |
301 | 296, 28, 298, 300 | lt2sqd 12905 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2))) |
302 | | absresq 13890 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ →
((abs‘𝑡)↑2) =
(𝑡↑2)) |
303 | 302 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡)↑2) = (𝑡↑2)) |
304 | 265 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℂ) |
305 | 304 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑅↑2) ·
1) = (𝑅↑2)) |
306 | 305 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) = ((𝑅↑2) ·
1)) |
307 | 303, 306 | breq12d 4596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1))) |
308 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℂ) |
309 | 78, 308, 29 | sqdivd 12883 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
310 | 309 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1)) |
311 | 30 | resqcld 12897 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) ∈
ℝ) |
312 | 311, 42 | posdifd 10493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) < 1 ↔ 0 <
(1 − ((𝑡 / 𝑅)↑2)))) |
313 | | resqcl 12793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
314 | 313 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡↑2) ∈
ℝ) |
315 | | rpgt0 11720 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ+
→ 0 < 𝑅) |
316 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ 0 ∈ ℝ) |
317 | | 0le0 10987 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
0 |
318 | 317 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 0) |
319 | 316, 21, 318, 299 | lt2sqd 12905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔
(0↑2) < (𝑅↑2))) |
320 | | sq0 12817 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0↑2) = 0 |
321 | 320 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ (0↑2) = 0) |
322 | 321 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2))) |
323 | 319, 322 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔ 0
< (𝑅↑2))) |
324 | 315, 323 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ+
→ 0 < (𝑅↑2)) |
325 | 283, 324 | elrpd 11745 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ+) |
326 | 325 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℝ+) |
327 | 314, 42, 326 | ltdivmuld 11799 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡↑2) /
(𝑅↑2)) < 1 ↔
(𝑡↑2) < ((𝑅↑2) ·
1))) |
328 | 310, 312,
327 | 3bitr3rd 298 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) <
((𝑅↑2) · 1)
↔ 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
329 | 301, 307,
328 | 3bitrd 293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ 0 < (1 −
((𝑡 / 𝑅)↑2)))) |
330 | 294, 329 | bitr3d 269 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
331 | 330 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
332 | 331 | exp4b 630 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2)))))) |
333 | 332 | 3impd 1273 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
334 | 26, 333 | sylbid 229 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
335 | 334 | imp 444 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2))) |
336 | 293, 292,
335 | ltled 10064 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))) |
337 | 284, 286,
292, 336 | sqrtmuld 14011 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))) |
338 | 273, 13, 14 | subdid 10365 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2)))) |
339 | 273 | mulid1d 9936 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2)) |
340 | 5, 7, 9 | sqdivd 12883 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
341 | 340 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2)))) |
342 | 4 | sqcld 12868 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ) |
343 | 342 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ) |
344 | | sqne0 12792 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0)) |
345 | 6, 344 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ≠ 0
↔ 𝑅 ≠
0)) |
346 | 8, 345 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ≠
0) |
347 | 346 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0) |
348 | 343, 273,
347 | divcan2d 10682 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2)) |
349 | 341, 348 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2)) |
350 | 339, 349 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
351 | 338, 350 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
352 | 351 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
353 | 21, 299 | sqrtsqd 14006 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (√‘(𝑅↑2)) = 𝑅) |
354 | 353 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅) |
355 | 354 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 −
((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
356 | 337, 352,
355 | 3eqtr3rd 2653 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
357 | 356 | oveq2d 6565 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
358 | 281, 282,
357 | 3eqtrd 2648 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
359 | 272, 274,
358 | 3eqtr2d 2650 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2))))) |
360 | 359 | mpteq2dva 4672 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |
361 | 266, 360 | eqtrd 2644 |
1
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |