Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  areacirclem1 Structured version   Visualization version   GIF version

Theorem areacirclem1 35161
 Description: Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
Assertion
Ref Expression
areacirclem1 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
Distinct variable group:   𝑡,𝑅

Proof of Theorem areacirclem1
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reelprrecn 10620 . . . 4 ℝ ∈ {ℝ, ℂ}
21a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℝ ∈ {ℝ, ℂ})
3 elioore 12758 . . . . . . . 8 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
43recnd 10660 . . . . . . 7 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ)
54adantl 485 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ)
6 rpcn 12389 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
76adantr 484 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ)
8 rpne0 12395 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ≠ 0)
98adantr 484 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0)
105, 7, 9divcld 11407 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
11 asincl 25466 . . . . 5 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
1210, 11syl 17 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
13 1cnd 10627 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ)
1410sqcld 13506 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
1513, 14subcld 10988 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
1615sqrtcld 14791 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
1710, 16mulcld 10652 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
1812, 17addcld 10651 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ℂ)
19 ovexd 7170 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V)
20 rpre 12387 . . . . . . . . . 10 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
2120renegcld 11058 . . . . . . . . 9 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
2221rexrd 10682 . . . . . . . 8 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ*)
23 rpxr 12388 . . . . . . . 8 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
24 elioo2 12769 . . . . . . . 8 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
2522, 23, 24syl2anc 587 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
26 simpr 488 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2720adantr 484 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
288adantr 484 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
2926, 27, 28redivcld 11459 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
3029a1d 25 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ))
316mulm1d 11083 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (-1 · 𝑅) = -𝑅)
3231adantr 484 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-1 · 𝑅) = -𝑅)
3332breq1d 5040 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -𝑅 < 𝑡))
34 neg1rr 11742 . . . . . . . . . . . . . . 15 -1 ∈ ℝ
3534a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → -1 ∈ ℝ)
36 simpl 486 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ+)
3735, 26, 36ltmuldivd 12468 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3833, 37bitr3d 284 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3938biimpd 232 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅)))
4039adantrd 495 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → -1 < (𝑡 / 𝑅)))
41 1red 10633 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
4226, 41, 36ltdivmuld 12472 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1)))
436mulid1d 10649 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (𝑅 · 1) = 𝑅)
4443adantr 484 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅 · 1) = 𝑅)
4544breq2d 5042 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅))
4642, 45bitr2d 283 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1))
4746biimpd 232 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1))
4847adantld 494 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) < 1))
4930, 40, 483jcad 1126 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5049exp4b 434 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))))
51503impd 1345 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5225, 51sylbid 243 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5352imp 410 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5434rexri 10690 . . . . . 6 -1 ∈ ℝ*
55 1xr 10691 . . . . . 6 1 ∈ ℝ*
56 elioo2 12769 . . . . . 6 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5754, 55, 56mp2an 691 . . . . 5 ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5853, 57sylibr 237 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1))
59 ovexd 7170 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V)
60 elioore 12758 . . . . . . 7 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℝ)
6160recnd 10660 . . . . . 6 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℂ)
62 asincl 25466 . . . . . . 7 (𝑢 ∈ ℂ → (arcsin‘𝑢) ∈ ℂ)
63 id 22 . . . . . . . 8 (𝑢 ∈ ℂ → 𝑢 ∈ ℂ)
64 1cnd 10627 . . . . . . . . . 10 (𝑢 ∈ ℂ → 1 ∈ ℂ)
65 sqcl 13482 . . . . . . . . . 10 (𝑢 ∈ ℂ → (𝑢↑2) ∈ ℂ)
6664, 65subcld 10988 . . . . . . . . 9 (𝑢 ∈ ℂ → (1 − (𝑢↑2)) ∈ ℂ)
6766sqrtcld 14791 . . . . . . . 8 (𝑢 ∈ ℂ → (√‘(1 − (𝑢↑2))) ∈ ℂ)
6863, 67mulcld 10652 . . . . . . 7 (𝑢 ∈ ℂ → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
6962, 68addcld 10651 . . . . . 6 (𝑢 ∈ ℂ → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7061, 69syl 17 . . . . 5 (𝑢 ∈ (-1(,)1) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7170adantl 485 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
72 ovexd 7170 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (2 · (√‘(1 − (𝑢↑2)))) ∈ V)
73 recn 10618 . . . . . . 7 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
7473adantl 485 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
75 1cnd 10627 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℂ)
762dvmptid 24567 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
77 ioossre 12788 . . . . . . 7 (-𝑅(,)𝑅) ⊆ ℝ
7877a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ⊆ ℝ)
79 eqid 2798 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8079tgioo2 23415 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
81 iooretop 23378 . . . . . . 7 (-𝑅(,)𝑅) ∈ (topGen‘ran (,))
8281a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ∈ (topGen‘ran (,)))
832, 74, 75, 76, 78, 80, 79, 82dvmptres 24573 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1))
842, 5, 13, 83, 6, 8dvmptdivc 24575 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅)))
8561, 62syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (arcsin‘𝑢) ∈ ℂ)
8685adantl 485 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (arcsin‘𝑢) ∈ ℂ)
87 ovexd 7170 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 / (√‘(1 − (𝑢↑2)))) ∈ V)
88 dvreasin 35159 . . . . . . 7 (ℝ D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2)))))
89 asinf 25465 . . . . . . . . . 10 arcsin:ℂ⟶ℂ
9089a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → arcsin:ℂ⟶ℂ)
91 ioossre 12788 . . . . . . . . . . 11 (-1(,)1) ⊆ ℝ
92 ax-resscn 10585 . . . . . . . . . . 11 ℝ ⊆ ℂ
9391, 92sstri 3924 . . . . . . . . . 10 (-1(,)1) ⊆ ℂ
9493a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℂ)
9590, 94feqresmpt 6709 . . . . . . . 8 (𝑅 ∈ ℝ+ → (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))
9695oveq2d 7151 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))))
9788, 96syl5reqr 2848 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2))))))
9861, 68syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
9998adantl 485 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
100 ovexd 7170 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V)
10161adantl 485 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 𝑢 ∈ ℂ)
102 1cnd 10627 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 1 ∈ ℂ)
103 recn 10618 . . . . . . . . 9 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
104103adantl 485 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 𝑢 ∈ ℂ)
105 1cnd 10627 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 1 ∈ ℂ)
1062dvmptid 24567 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 𝑢)) = (𝑢 ∈ ℝ ↦ 1))
10791a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℝ)
108 iooretop 23378 . . . . . . . . 9 (-1(,)1) ∈ (topGen‘ran (,))
109108a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ∈ (topGen‘ran (,)))
1102, 104, 105, 106, 107, 80, 79, 109dvmptres 24573 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ 𝑢)) = (𝑢 ∈ (-1(,)1) ↦ 1))
11161, 67syl 17 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
112111adantl 485 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
113 ovexd 7170 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ V)
114 1red 10633 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 1 ∈ ℝ)
11560resqcld 13609 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℝ)
116114, 115resubcld 11059 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ)
117 elioo2 12769 . . . . . . . . . . . . 13 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1)))
11854, 55, 117mp2an 691 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1))
119 id 22 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ)
120 1red 10633 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 1 ∈ ℝ)
121119, 120absltd 14783 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ (-1 < 𝑢𝑢 < 1)))
122103abscld 14790 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
123103absge0d 14798 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
124 0le1 11154 . . . . . . . . . . . . . . . . . 18 0 ≤ 1
125124a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ 1)
126122, 120, 123, 125lt2sqd 13617 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ ((abs‘𝑢)↑2) < (1↑2)))
127 absresq 14656 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
128 sq1 13556 . . . . . . . . . . . . . . . . . 18 (1↑2) = 1
129128a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (1↑2) = 1)
130127, 129breq12d 5043 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → (((abs‘𝑢)↑2) < (1↑2) ↔ (𝑢↑2) < 1))
131 resqcl 13488 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
132131, 120posdifd 11218 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1 − (𝑢↑2))))
133126, 130, 1323bitrd 308 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ 0 < (1 − (𝑢↑2))))
134121, 133bitr3d 284 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) ↔ 0 < (1 − (𝑢↑2))))
135134biimpd 232 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2))))
1361353impib 1113 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2)))
137118, 136sylbi 220 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 0 < (1 − (𝑢↑2)))
138116, 137elrpd 12418 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ+)
139138adantl 485 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 − (𝑢↑2)) ∈ ℝ+)
140 negex 10875 . . . . . . . . . 10 -(2 · 𝑢) ∈ V
141140a1i 11 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → -(2 · 𝑢) ∈ V)
142 rpcn 12389 . . . . . . . . . . 11 (𝑣 ∈ ℝ+𝑣 ∈ ℂ)
143142sqrtcld 14791 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (√‘𝑣) ∈ ℂ)
144143adantl 485 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (√‘𝑣) ∈ ℂ)
145 ovexd 7170 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V)
146 1cnd 10627 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 1 ∈ ℂ)
147103sqcld 13506 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℂ)
148146, 147subcld 10988 . . . . . . . . . . 11 (𝑢 ∈ ℝ → (1 − (𝑢↑2)) ∈ ℂ)
149148adantl 485 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (1 − (𝑢↑2)) ∈ ℂ)
150140a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → -(2 · 𝑢) ∈ V)
151 0red 10635 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 0 ∈ ℝ)
152 1cnd 10627 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → 1 ∈ ℂ)
1532, 152dvmptc 24568 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 1)) = (𝑢 ∈ ℝ ↦ 0))
154147adantl 485 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℂ)
155 ovexd 7170 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (2 · 𝑢) ∈ V)
15679cnfldtopon 23395 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
157 toponmax 21538 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
158156, 157mp1i 13 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ℂ ∈ (TopOpen‘ℂfld))
159 df-ss 3898 . . . . . . . . . . . . . . 15 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
16092, 159mpbi 233 . . . . . . . . . . . . . 14 (ℝ ∩ ℂ) = ℝ
161160a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ ∩ ℂ) = ℝ)
16265adantl 485 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (𝑢↑2) ∈ ℂ)
163 ovexd 7170 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (2 · 𝑢) ∈ V)
164 2nn 11700 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
165 dvexp 24563 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))))
166164, 165ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1))))
167 2m1e1 11753 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
168167oveq2i 7146 . . . . . . . . . . . . . . . . . 18 (𝑢↑(2 − 1)) = (𝑢↑1)
169 exp1 13433 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢)
170168, 169syl5eq 2845 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢)
171170oveq2d 7151 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℂ → (2 · (𝑢↑(2 − 1))) = (2 · 𝑢))
172171mpteq2ia 5121 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
173166, 172eqtri 2821 . . . . . . . . . . . . . 14 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
174173a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢)))
17579, 2, 158, 161, 162, 163, 174dvmptres3 24566 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢)))
1762, 105, 151, 153, 154, 155, 175dvmptsub 24577 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢))))
177 df-neg 10864 . . . . . . . . . . . 12 -(2 · 𝑢) = (0 − (2 · 𝑢))
178177mpteq2i 5122 . . . . . . . . . . 11 (𝑢 ∈ ℝ ↦ -(2 · 𝑢)) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢)))
179176, 178eqtr4di 2851 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢)))
1802, 149, 150, 179, 107, 80, 79, 109dvmptres 24573 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢)))
181 dvsqrt 25338 . . . . . . . . . 10 (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣))))
182181a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣)))))
183 fveq2 6645 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (√‘𝑣) = (√‘(1 − (𝑢↑2))))
184183oveq2d 7151 . . . . . . . . . 10 (𝑣 = (1 − (𝑢↑2)) → (2 · (√‘𝑣)) = (2 · (√‘(1 − (𝑢↑2)))))
185184oveq2d 7151 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (1 / (2 · (√‘𝑣))) = (1 / (2 · (√‘(1 − (𝑢↑2))))))
1862, 2, 139, 141, 144, 145, 180, 182, 183, 185dvmptco 24582 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))))
187 2cnd 11705 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 2 ∈ ℂ)
188187, 61mulneg2d 11085 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · -𝑢) = -(2 · 𝑢))
189188oveq1d 7150 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))))
19061negcld 10975 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -𝑢 ∈ ℂ)
191137gt0ne0d 11195 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ≠ 0)
19261, 66syl 17 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℂ)
193192adantr 484 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈ ℂ)
194 simpr 488 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (√‘(1 − (𝑢↑2))) = 0)
195193, 194sqr00d 14795 . . . . . . . . . . . . . 14 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0)
196195ex 416 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0))
197196necon3d 3008 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → ((1 − (𝑢↑2)) ≠ 0 → (√‘(1 − (𝑢↑2))) ≠ 0))
198191, 197mpd 15 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ≠ 0)
199 2ne0 11731 . . . . . . . . . . . 12 2 ≠ 0
200199a1i 11 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 2 ≠ 0)
201190, 111, 187, 198, 200divcan5d 11433 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
202187, 61mulcld 10652 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (2 · 𝑢) ∈ ℂ)
203202negcld 10975 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(2 · 𝑢) ∈ ℂ)
204187, 111mulcld 10652 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
205187, 111, 200, 198mulne0d 11283 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ≠ 0)
206203, 204, 205divrec2d 11411 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))
207189, 201, 2063eqtr3rd 2842 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
208207mpteq2ia 5121 . . . . . . . 8 (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))
209186, 208eqtrdi 2849 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))))
2102, 101, 102, 110, 112, 113, 209dvmptmul 24571 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (𝑢 · (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))))
2112, 86, 87, 97, 99, 100, 210dvmptadd 24570 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))))
212111mulid2d 10650 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 · (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
213190, 111, 198divcld 11407 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
214213, 61mulcomd 10653 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21561, 190, 111, 198divassd 11442 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21661, 61mulneg2d 11085 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢))
21761sqvald 13505 . . . . . . . . . . . . . 14 (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢))
218217negeqd 10871 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢))
219216, 218eqtr4d 2836 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2))
220219oveq1d 7150 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
221214, 215, 2203eqtr2d 2839 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
222212, 221oveq12d 7153 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
22361sqcld 13506 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℂ)
224223negcld 10975 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈ ℂ)
225224, 111, 198divcld 11407 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
226111, 225addcomd 10833 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
227222, 226eqtrd 2833 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
228227oveq2d 7151 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
2291112timesd 11870 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) = ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))))
23064, 65negsubd 10994 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = (1 − (𝑢↑2)))
23166sqsqrtd 14793 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2)))
23267sqvald 13505 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
233230, 231, 2323eqtr2d 2839 . . . . . . . . . . . 12 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
23461, 233syl 17 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
235234oveq1d 7150 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))))
236 1cnd 10627 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 1 ∈ ℂ)
237236, 224, 111, 198divdird 11445 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
238111, 111, 198divcan3d 11412 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
239235, 237, 2383eqtr3rd 2842 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
240239oveq1d 7150 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))))
241111, 198reccld 11400 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (1 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
242241, 225, 111addassd 10654 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
243229, 240, 2423eqtrrd 2838 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))) = (2 · (√‘(1 − (𝑢↑2)))))
244228, 243eqtrd 2833 . . . . . 6 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = (2 · (√‘(1 − (𝑢↑2)))))
245244mpteq2ia 5121 . . . . 5 (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2)))))
246211, 245eqtrdi 2849 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2))))))
247 fveq2 6645 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅)))
248 id 22 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅))
249 oveq1 7142 . . . . . . . 8 (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2))
250249oveq2d 7151 . . . . . . 7 (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2)))
251250fveq2d 6649 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
252248, 251oveq12d 7153 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
253247, 252oveq12d 7153 . . . 4 (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) = ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
254251oveq2d 7151 . . . 4 (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1 − (𝑢↑2)))) = (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
2552, 2, 58, 59, 71, 72, 84, 246, 253, 254dvmptco 24582 . . 3 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))
2566sqcld 13506 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
2572, 18, 19, 255, 256dvmptcmul 24574 . 2 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))))
258 2cnd 11705 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ)
259258, 16mulcld 10652 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
2606, 8reccld 11400 . . . . . . 7 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
261260adantr 484 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ)
262259, 261mulcomd 10653 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
263262oveq2d 7151 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
264256adantr 484 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ)
265264, 261, 259mulassd 10655 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2666sqvald 13505 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) = (𝑅 · 𝑅))
267266oveq1d 7150 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅))
268256, 6, 8divrecd 11410 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅)))
2696, 6, 8divcan3d 11412 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅 · 𝑅) / 𝑅) = 𝑅)
270267, 268, 2693eqtr3d 2841 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
271270adantr 484 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
272271oveq1d 7150 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
2737, 258, 16mul12d 10840 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
27420resqcld 13609 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
275274adantr 484 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ)
27620sqge0d 13610 . . . . . . . . 9 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
277276adantr 484 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2))
278 1red 10633 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ)
2793adantl 485 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ)
28020adantr 484 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
281279, 280, 9redivcld 11459 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
282281resqcld 13609 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
283278, 282resubcld 11059 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
284 0red 10635 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
28526, 27absltd 14783 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
28673abscld 14790 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
287286adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
28873absge0d 14798 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
289288adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
290 rpge0 12392 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
291290adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
292287, 27, 289, 291lt2sqd 13617 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
293 absresq 14656 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
294293adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
295256adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
296295mulid1d 10649 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) · 1) = (𝑅↑2))
297296eqcomd 2804 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) = ((𝑅↑2) · 1))
298294, 297breq12d 5043 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
2996adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
30074, 299, 28sqdivd 13521 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
301300breq1d 5040 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1))
30229resqcld 13609 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
303302, 41posdifd 11218 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
304 resqcl 13488 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
305304adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
306 rpgt0 12391 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → 0 < 𝑅)
307 0red 10635 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
308 0le0 11728 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
309308a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ≤ 0)
310307, 20, 309, 290lt2sqd 13617 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
311 sq0 13553 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
312311a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0↑2) = 0)
313312breq1d 5040 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
314310, 313bitrd 282 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
315306, 314mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
316274, 315elrpd 12418 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
317316adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
318305, 41, 317ltdivmuld 12472 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) < 1 ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
319301, 303, 3183bitr3rd 313 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < ((𝑅↑2) · 1) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
320292, 298, 3193bitrd 308 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
321285, 320bitr3d 284 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
322321biimpd 232 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
323322exp4b 434 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2))))))
3243233impd 1345 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
32525, 324sylbid 243 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
326325imp 410 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2)))
327284, 283, 326ltled 10779 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
328275, 277, 283, 327sqrtmuld 14778 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
329264, 13, 14subdid 11087 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
330264mulid1d 10649 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
3315, 7, 9sqdivd 13521 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
332331oveq2d 7151 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
3334sqcld 13506 . . . . . . . . . . . . 13 (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ)
334333adantl 485 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ)
335 sqne0 13487 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3366, 335syl 17 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3378, 336mpbird 260 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
338337adantr 484 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0)
339334, 264, 338divcan2d 11409 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
340332, 339eqtrd 2833 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
341330, 340oveq12d 7153 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
342329, 341eqtrd 2833 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
343342fveq2d 6649 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
34420, 290sqrtsqd 14773 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (√‘(𝑅↑2)) = 𝑅)
345344adantr 484 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅)
346345oveq1d 7150 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
347328, 343, 3463eqtr3rd 2842 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
348347oveq2d 7151 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
349272, 273, 3483eqtrd 2837 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
350263, 265, 3493eqtr2d 2839 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
351350mpteq2dva 5125 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
352257, 351eqtrd 2833 1 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  {cpr 4527   class class class wbr 5030   ↦ cmpt 5110  ran crn 5520   ↾ cres 5521  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℂcc 10526  ℝcr 10527  0cc0 10528  1c1 10529   + caddc 10531   · cmul 10533  ℝ*cxr 10665   < clt 10666   ≤ cle 10667   − cmin 10861  -cneg 10862   / cdiv 11288  ℕcn 11627  2c2 11682  ℝ+crp 12379  (,)cioo 12728  ↑cexp 13427  √csqrt 14586  abscabs 14587  TopOpenctopn 16689  topGenctg 16705  ℂfldccnfld 20094  TopOnctopon 21522   D cdv 24473  arcsincasin 25455 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606  ax-addf 10607  ax-mulf 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7390  df-om 7563  df-1st 7673  df-2nd 7674  df-supp 7816  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-2o 8088  df-oadd 8091  df-er 8274  df-map 8393  df-pm 8394  df-ixp 8447  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-fsupp 8820  df-fi 8861  df-sup 8892  df-inf 8893  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-4 11692  df-5 11693  df-6 11694  df-7 11695  df-8 11696  df-9 11697  df-n0 11888  df-z 11972  df-dec 12089  df-uz 12234  df-q 12339  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ioc 12733  df-ico 12734  df-icc 12735  df-fz 12888  df-fzo 13031  df-fl 13159  df-mod 13235  df-seq 13367  df-exp 13428  df-fac 13632  df-bc 13661  df-hash 13689  df-shft 14420  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-limsup 14822  df-clim 14839  df-rlim 14840  df-sum 15037  df-ef 15415  df-sin 15417  df-cos 15418  df-tan 15419  df-pi 15420  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-starv 16574  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-hom 16583  df-cco 16584  df-rest 16690  df-topn 16691  df-0g 16709  df-gsum 16710  df-topgen 16711  df-pt 16712  df-prds 16715  df-xrs 16769  df-qtop 16774  df-imas 16775  df-xps 16777  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-mulg 18220  df-cntz 18442  df-cmn 18903  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-fbas 20091  df-fg 20092  df-cnfld 20095  df-top 21506  df-topon 21523  df-topsp 21545  df-bases 21558  df-cld 21631  df-ntr 21632  df-cls 21633  df-nei 21710  df-lp 21748  df-perf 21749  df-cn 21839  df-cnp 21840  df-haus 21927  df-cmp 21999  df-tx 22174  df-hmeo 22367  df-fil 22458  df-fm 22550  df-flim 22551  df-flf 22552  df-xms 22934  df-ms 22935  df-tms 22936  df-cncf 23490  df-limc 24476  df-dv 24477  df-log 25155  df-cxp 25156  df-asin 25458 This theorem is referenced by:  areacirc  35166
 Copyright terms: Public domain W3C validator