| Step | Hyp | Ref
| Expression |
| 1 | | reelprrecn 11247 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ ℝ ∈ {ℝ, ℂ}) |
| 3 | | elioore 13417 |
. . . . . . . 8
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ) |
| 4 | 3 | recnd 11289 |
. . . . . . 7
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ) |
| 6 | | rpcn 13045 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ) |
| 8 | | rpne0 13051 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) |
| 9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0) |
| 10 | 5, 7, 9 | divcld 12043 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ) |
| 11 | | asincl 26916 |
. . . . 5
⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ) |
| 12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ) |
| 13 | | 1cnd 11256 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ) |
| 14 | 10 | sqcld 14184 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ) |
| 15 | 13, 14 | subcld 11620 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ) |
| 16 | 15 | sqrtcld 15476 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ) |
| 17 | 10, 16 | mulcld 11281 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
| 18 | 12, 17 | addcld 11280 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈
ℂ) |
| 19 | | ovexd 7466 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V) |
| 20 | | rpre 13043 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
| 21 | 20 | renegcld 11690 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ) |
| 22 | 21 | rexrd 11311 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ*) |
| 23 | | rpxr 13044 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
| 24 | | elioo2 13428 |
. . . . . . . 8
⊢ ((-𝑅 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
| 26 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℝ) |
| 27 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ) |
| 28 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ≠
0) |
| 29 | 26, 27, 28 | redivcld 12095 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 / 𝑅) ∈
ℝ) |
| 30 | 29 | a1d 25 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ)) |
| 31 | 6 | mulm1d 11715 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (-1 · 𝑅) =
-𝑅) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-1 · 𝑅) =
-𝑅) |
| 33 | 32 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-1 · 𝑅)
< 𝑡 ↔ -𝑅 < 𝑡)) |
| 34 | | neg1rr 12381 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℝ |
| 35 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ -1 ∈ ℝ) |
| 36 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ+) |
| 37 | 35, 26, 36 | ltmuldivd 13124 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-1 · 𝑅)
< 𝑡 ↔ -1 <
(𝑡 / 𝑅))) |
| 38 | 33, 37 | bitr3d 281 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅))) |
| 39 | 38 | biimpd 229 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅))) |
| 40 | 39 | adantrd 491 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → -1 < (𝑡 / 𝑅))) |
| 41 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℝ) |
| 42 | 26, 41, 36 | ltdivmuld 13128 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1))) |
| 43 | 6 | mulridd 11278 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (𝑅 · 1) =
𝑅) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅 · 1) =
𝑅) |
| 45 | 44 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅)) |
| 46 | 42, 45 | bitr2d 280 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1)) |
| 47 | 46 | biimpd 229 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1)) |
| 48 | 47 | adantld 490 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (𝑡 / 𝑅) < 1)) |
| 49 | 30, 40, 48 | 3jcad 1130 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
| 50 | 49 | exp4b 430 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))))) |
| 51 | 50 | 3impd 1349 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
| 52 | 25, 51 | sylbid 240 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
| 53 | 52 | imp 406 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)) |
| 54 | 34 | rexri 11319 |
. . . . . 6
⊢ -1 ∈
ℝ* |
| 55 | | 1xr 11320 |
. . . . . 6
⊢ 1 ∈
ℝ* |
| 56 | | elioo2 13428 |
. . . . . 6
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
| 57 | 54, 55, 56 | mp2an 692 |
. . . . 5
⊢ ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)) |
| 58 | 53, 57 | sylibr 234 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1)) |
| 59 | | ovexd 7466 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V) |
| 60 | | elioore 13417 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → 𝑢 ∈
ℝ) |
| 61 | 60 | recnd 11289 |
. . . . . 6
⊢ (𝑢 ∈ (-1(,)1) → 𝑢 ∈
ℂ) |
| 62 | | asincl 26916 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ →
(arcsin‘𝑢) ∈
ℂ) |
| 63 | | id 22 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ → 𝑢 ∈
ℂ) |
| 64 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → 1 ∈
ℂ) |
| 65 | | sqcl 14158 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → (𝑢↑2) ∈
ℂ) |
| 66 | 64, 65 | subcld 11620 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℂ → (1
− (𝑢↑2)) ∈
ℂ) |
| 67 | 66 | sqrtcld 15476 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ →
(√‘(1 − (𝑢↑2))) ∈ ℂ) |
| 68 | 63, 67 | mulcld 11281 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ → (𝑢 · (√‘(1
− (𝑢↑2))))
∈ ℂ) |
| 69 | 62, 68 | addcld 11280 |
. . . . . 6
⊢ (𝑢 ∈ ℂ →
((arcsin‘𝑢) + (𝑢 · (√‘(1
− (𝑢↑2)))))
∈ ℂ) |
| 70 | 61, 69 | syl 17 |
. . . . 5
⊢ (𝑢 ∈ (-1(,)1) →
((arcsin‘𝑢) + (𝑢 · (√‘(1
− (𝑢↑2)))))
∈ ℂ) |
| 71 | 70 | adantl 481 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ ((arcsin‘𝑢) +
(𝑢 ·
(√‘(1 − (𝑢↑2))))) ∈ ℂ) |
| 72 | | ovexd 7466 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (2 · (√‘(1 − (𝑢↑2)))) ∈ V) |
| 73 | | recn 11245 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℂ) |
| 74 | 73 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℂ) |
| 75 | | 1cnd 11256 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℂ) |
| 76 | 2 | dvmptid 25995 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
ℝ ↦ 𝑡)) =
(𝑡 ∈ ℝ ↦
1)) |
| 77 | | ioossre 13448 |
. . . . . . 7
⊢ (-𝑅(,)𝑅) ⊆ ℝ |
| 78 | 77 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (-𝑅(,)𝑅) ⊆
ℝ) |
| 79 | | tgioo4 24826 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 80 | | eqid 2737 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 81 | | iooretop 24786 |
. . . . . . 7
⊢ (-𝑅(,)𝑅) ∈ (topGen‘ran
(,)) |
| 82 | 81 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (-𝑅(,)𝑅) ∈ (topGen‘ran
(,))) |
| 83 | 2, 74, 75, 76, 78, 79, 80, 82 | dvmptres 26001 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1)) |
| 84 | 2, 5, 13, 83, 6, 8 | dvmptdivc 26003 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅))) |
| 85 | 61, 62 | syl 17 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) →
(arcsin‘𝑢) ∈
ℂ) |
| 86 | 85 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (arcsin‘𝑢)
∈ ℂ) |
| 87 | | ovexd 7466 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (1 / (√‘(1 − (𝑢↑2)))) ∈ V) |
| 88 | | asinf 26915 |
. . . . . . . . . 10
⊢
arcsin:ℂ⟶ℂ |
| 89 | 88 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ arcsin:ℂ⟶ℂ) |
| 90 | | ioossre 13448 |
. . . . . . . . . . 11
⊢ (-1(,)1)
⊆ ℝ |
| 91 | | ax-resscn 11212 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
| 92 | 90, 91 | sstri 3993 |
. . . . . . . . . 10
⊢ (-1(,)1)
⊆ ℂ |
| 93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ⊆ ℂ) |
| 94 | 89, 93 | feqresmpt 6978 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) |
| 95 | 94 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))) |
| 96 | | dvreasin 37713 |
. . . . . . 7
⊢ (ℝ
D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 /
(√‘(1 − (𝑢↑2))))) |
| 97 | 95, 96 | eqtr3di 2792 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 /
(√‘(1 − (𝑢↑2)))))) |
| 98 | 61, 68 | syl 17 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1
− (𝑢↑2))))
∈ ℂ) |
| 99 | 98 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (𝑢 ·
(√‘(1 − (𝑢↑2)))) ∈ ℂ) |
| 100 | | ovexd 7466 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V) |
| 101 | 61 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ 𝑢 ∈
ℂ) |
| 102 | | 1cnd 11256 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ 1 ∈ ℂ) |
| 103 | | recn 11245 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ → 𝑢 ∈
ℂ) |
| 104 | 103 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 𝑢 ∈
ℂ) |
| 105 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 1 ∈ ℂ) |
| 106 | 2 | dvmptid 25995 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ 𝑢)) =
(𝑢 ∈ ℝ ↦
1)) |
| 107 | 90 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ⊆ ℝ) |
| 108 | | iooretop 24786 |
. . . . . . . . 9
⊢ (-1(,)1)
∈ (topGen‘ran (,)) |
| 109 | 108 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ∈ (topGen‘ran (,))) |
| 110 | 2, 104, 105, 106, 107, 79, 80, 109 | dvmptres 26001 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ 𝑢)) =
(𝑢 ∈ (-1(,)1) ↦
1)) |
| 111 | 61, 67 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) ∈ ℂ) |
| 112 | 111 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (√‘(1 − (𝑢↑2))) ∈ ℂ) |
| 113 | | ovexd 7466 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (-𝑢 /
(√‘(1 − (𝑢↑2)))) ∈ V) |
| 114 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → 1 ∈
ℝ) |
| 115 | 60 | resqcld 14165 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈
ℝ) |
| 116 | 114, 115 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℝ) |
| 117 | | elioo2 13428 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1))) |
| 118 | 54, 55, 117 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1)) |
| 119 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → 𝑢 ∈
ℝ) |
| 120 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → 1 ∈
ℝ) |
| 121 | 119, 120 | absltd 15468 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ (-1 < 𝑢 ∧
𝑢 <
1))) |
| 122 | 103 | abscld 15475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
(abs‘𝑢) ∈
ℝ) |
| 123 | 103 | absge0d 15483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → 0 ≤
(abs‘𝑢)) |
| 124 | | 0le1 11786 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
1 |
| 125 | 124 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → 0 ≤
1) |
| 126 | 122, 120,
123, 125 | lt2sqd 14295 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ ((abs‘𝑢)↑2) < (1↑2))) |
| 127 | | absresq 15341 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢)↑2) =
(𝑢↑2)) |
| 128 | | sq1 14234 |
. . . . . . . . . . . . . . . . . 18
⊢
(1↑2) = 1 |
| 129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
(1↑2) = 1) |
| 130 | 127, 129 | breq12d 5156 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ →
(((abs‘𝑢)↑2)
< (1↑2) ↔ (𝑢↑2) < 1)) |
| 131 | | resqcl 14164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → (𝑢↑2) ∈
ℝ) |
| 132 | 131, 120 | posdifd 11850 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1
− (𝑢↑2)))) |
| 133 | 126, 130,
132 | 3bitrd 305 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ 0 < (1 − (𝑢↑2)))) |
| 134 | 121, 133 | bitr3d 281 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ℝ → ((-1 <
𝑢 ∧ 𝑢 < 1) ↔ 0 < (1 − (𝑢↑2)))) |
| 135 | 134 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℝ → ((-1 <
𝑢 ∧ 𝑢 < 1) → 0 < (1 − (𝑢↑2)))) |
| 136 | 135 | 3impib 1117 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1) → 0 < (1 − (𝑢↑2))) |
| 137 | 118, 136 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 0 <
(1 − (𝑢↑2))) |
| 138 | 116, 137 | elrpd 13074 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℝ+) |
| 139 | 138 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (1 − (𝑢↑2)) ∈
ℝ+) |
| 140 | | negex 11506 |
. . . . . . . . . 10
⊢ -(2
· 𝑢) ∈
V |
| 141 | 140 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ -(2 · 𝑢)
∈ V) |
| 142 | | rpcn 13045 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ℝ+
→ 𝑣 ∈
ℂ) |
| 143 | 142 | sqrtcld 15476 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ℝ+
→ (√‘𝑣)
∈ ℂ) |
| 144 | 143 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → (√‘𝑣) ∈ ℂ) |
| 145 | | ovexd 7466 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V) |
| 146 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℝ → 1 ∈
ℂ) |
| 147 | 103 | sqcld 14184 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℝ → (𝑢↑2) ∈
ℂ) |
| 148 | 146, 147 | subcld 11620 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ → (1
− (𝑢↑2)) ∈
ℂ) |
| 149 | 148 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (1 − (𝑢↑2)) ∈ ℂ) |
| 150 | 140 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ -(2 · 𝑢)
∈ V) |
| 151 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 0 ∈ ℝ) |
| 152 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ 1 ∈ ℂ) |
| 153 | 2, 152 | dvmptc 25996 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ 1)) = (𝑢
∈ ℝ ↦ 0)) |
| 154 | 147 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (𝑢↑2) ∈
ℂ) |
| 155 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (2 · 𝑢)
∈ V) |
| 156 | 80 | cnfldtopon 24803 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 157 | | toponmax 22932 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
| 158 | 156, 157 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ℂ ∈ (TopOpen‘ℂfld)) |
| 159 | | dfss2 3969 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
| 160 | 91, 159 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢ (ℝ
∩ ℂ) = ℝ |
| 161 | 160 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℝ ∩ ℂ) = ℝ) |
| 162 | 65 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℂ)
→ (𝑢↑2) ∈
ℂ) |
| 163 | | ovexd 7466 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℂ)
→ (2 · 𝑢)
∈ V) |
| 164 | | 2nn 12339 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
| 165 | | dvexp 25991 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 −
1))))) |
| 166 | 164, 165 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑢 ∈ ℂ ↦
(𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2
· (𝑢↑(2 −
1)))) |
| 167 | | 2m1e1 12392 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
| 168 | 167 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢↑(2 − 1)) = (𝑢↑1) |
| 169 | | exp1 14108 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢) |
| 170 | 168, 169 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢) |
| 171 | 170 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℂ → (2
· (𝑢↑(2 −
1))) = (2 · 𝑢)) |
| 172 | 171 | mpteq2ia 5245 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ ↦ (2
· (𝑢↑(2 −
1)))) = (𝑢 ∈ ℂ
↦ (2 · 𝑢)) |
| 173 | 166, 172 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑢 ∈ ℂ ↦
(𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2
· 𝑢)) |
| 174 | 173 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℂ D (𝑢 ∈
ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))) |
| 175 | 80, 2, 158, 161, 162, 163, 174 | dvmptres3 25994 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢))) |
| 176 | 2, 105, 151, 153, 154, 155, 175 | dvmptsub 26005 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2
· 𝑢)))) |
| 177 | | df-neg 11495 |
. . . . . . . . . . . 12
⊢ -(2
· 𝑢) = (0 − (2
· 𝑢)) |
| 178 | 177 | mpteq2i 5247 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ ↦ -(2
· 𝑢)) = (𝑢 ∈ ℝ ↦ (0
− (2 · 𝑢))) |
| 179 | 176, 178 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢))) |
| 180 | 2, 149, 150, 179, 107, 79, 80, 109 | dvmptres 26001 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢))) |
| 181 | | dvsqrt 26784 |
. . . . . . . . . 10
⊢ (ℝ
D (𝑣 ∈
ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑣)))) |
| 182 | 181 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑣 ∈
ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑣))))) |
| 183 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑣 = (1 − (𝑢↑2)) →
(√‘𝑣) =
(√‘(1 − (𝑢↑2)))) |
| 184 | 183 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑣 = (1 − (𝑢↑2)) → (2 ·
(√‘𝑣)) = (2
· (√‘(1 − (𝑢↑2))))) |
| 185 | 184 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑣 = (1 − (𝑢↑2)) → (1 / (2
· (√‘𝑣))) = (1 / (2 · (√‘(1
− (𝑢↑2)))))) |
| 186 | 2, 2, 139, 141, 144, 145, 180, 182, 183, 185 | dvmptco 26010 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 ·
(√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))) |
| 187 | | 2cnd 12344 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → 2 ∈
ℂ) |
| 188 | 187, 61 | mulneg2d 11717 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· -𝑢) = -(2 ·
𝑢)) |
| 189 | 188 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((2
· -𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 ·
(√‘(1 − (𝑢↑2)))))) |
| 190 | 61 | negcld 11607 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -𝑢 ∈
ℂ) |
| 191 | 137 | gt0ne0d 11827 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ≠
0) |
| 192 | 61, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℂ) |
| 193 | 192 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈
ℂ) |
| 194 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (√‘(1
− (𝑢↑2))) =
0) |
| 195 | 193, 194 | sqr00d 15480 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0) |
| 196 | 195 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0)) |
| 197 | 196 | necon3d 2961 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → ((1
− (𝑢↑2)) ≠ 0
→ (√‘(1 − (𝑢↑2))) ≠ 0)) |
| 198 | 191, 197 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) ≠ 0) |
| 199 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 200 | 199 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 2 ≠
0) |
| 201 | 190, 111,
187, 198, 200 | divcan5d 12069 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((2
· -𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2))))) |
| 202 | 187, 61 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (2
· 𝑢) ∈
ℂ) |
| 203 | 202 | negcld 11607 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -(2
· 𝑢) ∈
ℂ) |
| 204 | 187, 111 | mulcld 11281 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) ∈ ℂ) |
| 205 | 187, 111,
200, 198 | mulne0d 11915 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) ≠ 0) |
| 206 | 203, 204,
205 | divrec2d 12047 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (-(2
· 𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = ((1 / (2 ·
(√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) |
| 207 | 189, 201,
206 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → ((1 / (2
· (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2))))) |
| 208 | 207 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) ↦ ((1 /
(2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))) |
| 209 | 186, 208 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
| 210 | 2, 101, 102, 110, 112, 113, 209 | dvmptmul 25999 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (𝑢
· (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 ·
(√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) |
| 211 | 2, 86, 87, 97, 99, 100, 210 | dvmptadd 25998 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))))) |
| 212 | 111 | mullidd 11279 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (1
· (√‘(1 − (𝑢↑2)))) = (√‘(1 −
(𝑢↑2)))) |
| 213 | 190, 111,
198 | divcld 12043 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 −
(𝑢↑2)))) ∈
ℂ) |
| 214 | 213, 61 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 −
(𝑢↑2)))) ·
𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
| 215 | 61, 190, 111, 198 | divassd 12078 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
| 216 | 61, 61 | mulneg2d 11717 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢)) |
| 217 | 61 | sqvald 14183 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢)) |
| 218 | 217 | negeqd 11502 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢)) |
| 219 | 216, 218 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2)) |
| 220 | 219 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1
− (𝑢↑2))))) |
| 221 | 214, 215,
220 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 −
(𝑢↑2)))) ·
𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) |
| 222 | 212, 221 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 −
(𝑢↑2))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
| 223 | 61 | sqcld 14184 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈
ℂ) |
| 224 | 223 | negcld 11607 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈
ℂ) |
| 225 | 224, 111,
198 | divcld 12043 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1
− (𝑢↑2))))
∈ ℂ) |
| 226 | 111, 225 | addcomd 11463 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1
− (𝑢↑2)))) +
(√‘(1 − (𝑢↑2))))) |
| 227 | 222, 226 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2))))) |
| 228 | 227 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))) = ((1 /
(√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2)))))) |
| 229 | 111 | 2timesd 12509 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) = ((√‘(1 −
(𝑢↑2))) +
(√‘(1 − (𝑢↑2))))) |
| 230 | 64, 65 | negsubd 11626 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ → (1 +
-(𝑢↑2)) = (1 −
(𝑢↑2))) |
| 231 | 66 | sqsqrtd 15478 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ →
((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2))) |
| 232 | 67 | sqvald 14183 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ →
((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1
− (𝑢↑2)))
· (√‘(1 − (𝑢↑2))))) |
| 233 | 230, 231,
232 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℂ → (1 +
-(𝑢↑2)) =
((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2))))) |
| 234 | 61, 233 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (1 +
-(𝑢↑2)) =
((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2))))) |
| 235 | 234 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((1 +
-(𝑢↑2)) /
(√‘(1 − (𝑢↑2)))) = (((√‘(1 −
(𝑢↑2))) ·
(√‘(1 − (𝑢↑2)))) / (√‘(1 −
(𝑢↑2))))) |
| 236 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 1 ∈
ℂ) |
| 237 | 236, 224,
111, 198 | divdird 12081 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((1 +
-(𝑢↑2)) /
(√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 −
(𝑢↑2)))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
| 238 | 111, 111,
198 | divcan3d 12048 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) →
(((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2)))) /
(√‘(1 − (𝑢↑2)))) = (√‘(1 −
(𝑢↑2)))) |
| 239 | 235, 237,
238 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 −
(𝑢↑2)))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
| 240 | 239 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 /
(√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1
− (𝑢↑2))))) |
| 241 | 111, 198 | reccld 12036 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → (1 /
(√‘(1 − (𝑢↑2)))) ∈ ℂ) |
| 242 | 241, 225,
111 | addassd 11283 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → (((1 /
(√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1
− (𝑢↑2)))) = ((1
/ (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2)))))) |
| 243 | 229, 240,
242 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2))))) = (2
· (√‘(1 − (𝑢↑2))))) |
| 244 | 228, 243 | eqtrd 2777 |
. . . . . 6
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))) = (2 ·
(√‘(1 − (𝑢↑2))))) |
| 245 | 244 | mpteq2ia 5245 |
. . . . 5
⊢ (𝑢 ∈ (-1(,)1) ↦ ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2
· (√‘(1 − (𝑢↑2))))) |
| 246 | 211, 245 | eqtrdi 2793 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2
· (√‘(1 − (𝑢↑2)))))) |
| 247 | | fveq2 6906 |
. . . . 5
⊢ (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅))) |
| 248 | | id 22 |
. . . . . 6
⊢ (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅)) |
| 249 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2)) |
| 250 | 249 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2))) |
| 251 | 250 | fveq2d 6910 |
. . . . . 6
⊢ (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1
− ((𝑡 / 𝑅)↑2)))) |
| 252 | 248, 251 | oveq12d 7449 |
. . . . 5
⊢ (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
| 253 | 247, 252 | oveq12d 7449 |
. . . 4
⊢ (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) =
((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
| 254 | 251 | oveq2d 7447 |
. . . 4
⊢ (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1
− (𝑢↑2)))) = (2
· (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
| 255 | 2, 2, 58, 59, 71, 72, 84, 246, 253, 254 | dvmptco 26010 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) |
| 256 | 6 | sqcld 14184 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) |
| 257 | 2, 18, 19, 255, 256 | dvmptcmul 26002 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))) |
| 258 | | 2cnd 12344 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ) |
| 259 | 258, 16 | mulcld 11281 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
| 260 | 6, 8 | reccld 12036 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (1 / 𝑅) ∈
ℂ) |
| 261 | 260 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ) |
| 262 | 259, 261 | mulcomd 11282 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))))) |
| 263 | 262 | oveq2d 7447 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))))) |
| 264 | 256 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ) |
| 265 | 264, 261,
259 | mulassd 11284 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))))) |
| 266 | 6 | sqvald 14183 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) = (𝑅 · 𝑅)) |
| 267 | 266 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅)) |
| 268 | 256, 6, 8 | divrecd 12046 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅))) |
| 269 | 6, 6, 8 | divcan3d 12048 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 · 𝑅) / 𝑅) = 𝑅) |
| 270 | 267, 268,
269 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
(1 / 𝑅)) = 𝑅) |
| 271 | 270 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅) |
| 272 | 271 | oveq1d 7446 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
| 273 | 7, 258, 16 | mul12d 11470 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (2 ·
(𝑅 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
| 274 | 20 | resqcld 14165 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ) |
| 275 | 274 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ) |
| 276 | 20 | sqge0d 14177 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ (𝑅↑2)) |
| 277 | 276 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2)) |
| 278 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ) |
| 279 | 3 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ) |
| 280 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ) |
| 281 | 279, 280,
9 | redivcld 12095 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ) |
| 282 | 281 | resqcld 14165 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ) |
| 283 | 278, 282 | resubcld 11691 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ) |
| 284 | | 0red 11264 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ) |
| 285 | 26, 27 | absltd 15468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
| 286 | 73 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ →
(abs‘𝑡) ∈
ℝ) |
| 287 | 286 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (abs‘𝑡) ∈
ℝ) |
| 288 | 73 | absge0d 15483 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ → 0 ≤
(abs‘𝑡)) |
| 289 | 288 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘𝑡)) |
| 290 | | rpge0 13048 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
| 291 | 290 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ 𝑅) |
| 292 | 287, 27, 289, 291 | lt2sqd 14295 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2))) |
| 293 | | absresq 15341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ →
((abs‘𝑡)↑2) =
(𝑡↑2)) |
| 294 | 293 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡)↑2) = (𝑡↑2)) |
| 295 | 256 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℂ) |
| 296 | 295 | mulridd 11278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑅↑2) ·
1) = (𝑅↑2)) |
| 297 | 296 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) = ((𝑅↑2) ·
1)) |
| 298 | 294, 297 | breq12d 5156 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1))) |
| 299 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℂ) |
| 300 | 74, 299, 28 | sqdivd 14199 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
| 301 | 300 | breq1d 5153 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1)) |
| 302 | 29 | resqcld 14165 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) ∈
ℝ) |
| 303 | 302, 41 | posdifd 11850 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) < 1 ↔ 0 <
(1 − ((𝑡 / 𝑅)↑2)))) |
| 304 | | resqcl 14164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
| 305 | 304 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡↑2) ∈
ℝ) |
| 306 | | rpgt0 13047 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ+
→ 0 < 𝑅) |
| 307 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ 0 ∈ ℝ) |
| 308 | | 0le0 12367 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
0 |
| 309 | 308 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 0) |
| 310 | 307, 20, 309, 290 | lt2sqd 14295 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔
(0↑2) < (𝑅↑2))) |
| 311 | | sq0 14231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0↑2) = 0 |
| 312 | 311 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ (0↑2) = 0) |
| 313 | 312 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2))) |
| 314 | 310, 313 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔ 0
< (𝑅↑2))) |
| 315 | 306, 314 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ+
→ 0 < (𝑅↑2)) |
| 316 | 274, 315 | elrpd 13074 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ+) |
| 317 | 316 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℝ+) |
| 318 | 305, 41, 317 | ltdivmuld 13128 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡↑2) /
(𝑅↑2)) < 1 ↔
(𝑡↑2) < ((𝑅↑2) ·
1))) |
| 319 | 301, 303,
318 | 3bitr3rd 310 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) <
((𝑅↑2) · 1)
↔ 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
| 320 | 292, 298,
319 | 3bitrd 305 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ 0 < (1 −
((𝑡 / 𝑅)↑2)))) |
| 321 | 285, 320 | bitr3d 281 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
| 322 | 321 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
| 323 | 322 | exp4b 430 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2)))))) |
| 324 | 323 | 3impd 1349 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
| 325 | 25, 324 | sylbid 240 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
| 326 | 325 | imp 406 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2))) |
| 327 | 284, 283,
326 | ltled 11409 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))) |
| 328 | 275, 277,
283, 327 | sqrtmuld 15463 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))) |
| 329 | 264, 13, 14 | subdid 11719 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2)))) |
| 330 | 264 | mulridd 11278 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2)) |
| 331 | 5, 7, 9 | sqdivd 14199 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
| 332 | 331 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2)))) |
| 333 | 4 | sqcld 14184 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ) |
| 334 | 333 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ) |
| 335 | | sqne0 14163 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0)) |
| 336 | 6, 335 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ≠ 0
↔ 𝑅 ≠
0)) |
| 337 | 8, 336 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ≠
0) |
| 338 | 337 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0) |
| 339 | 334, 264,
338 | divcan2d 12045 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2)) |
| 340 | 332, 339 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2)) |
| 341 | 330, 340 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
| 342 | 329, 341 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
| 343 | 342 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
| 344 | 20, 290 | sqrtsqd 15458 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (√‘(𝑅↑2)) = 𝑅) |
| 345 | 344 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅) |
| 346 | 345 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 −
((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
| 347 | 328, 343,
346 | 3eqtr3rd 2786 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
| 348 | 347 | oveq2d 7447 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
| 349 | 272, 273,
348 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
| 350 | 263, 265,
349 | 3eqtr2d 2783 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2))))) |
| 351 | 350 | mpteq2dva 5242 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |
| 352 | 257, 351 | eqtrd 2777 |
1
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |