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

Theorem areacirclem1 37694
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 11244 . . . 4 ℝ ∈ {ℝ, ℂ}
21a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℝ ∈ {ℝ, ℂ})
3 elioore 13413 . . . . . . . 8 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
43recnd 11286 . . . . . . 7 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ)
54adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ)
6 rpcn 13042 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
76adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ)
8 rpne0 13048 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ≠ 0)
98adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0)
105, 7, 9divcld 12040 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
11 asincl 26930 . . . . 5 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
1210, 11syl 17 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
13 1cnd 11253 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ)
1410sqcld 14180 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
1513, 14subcld 11617 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
1615sqrtcld 15472 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
1710, 16mulcld 11278 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
1812, 17addcld 11277 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ℂ)
19 ovexd 7465 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V)
20 rpre 13040 . . . . . . . . . 10 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
2120renegcld 11687 . . . . . . . . 9 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
2221rexrd 11308 . . . . . . . 8 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ*)
23 rpxr 13041 . . . . . . . 8 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
24 elioo2 13424 . . . . . . . 8 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
2522, 23, 24syl2anc 584 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
26 simpr 484 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2720adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
288adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
2926, 27, 28redivcld 12092 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
3029a1d 25 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ))
316mulm1d 11712 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (-1 · 𝑅) = -𝑅)
3231adantr 480 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-1 · 𝑅) = -𝑅)
3332breq1d 5157 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -𝑅 < 𝑡))
34 neg1rr 12378 . . . . . . . . . . . . . . 15 -1 ∈ ℝ
3534a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → -1 ∈ ℝ)
36 simpl 482 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ+)
3735, 26, 36ltmuldivd 13121 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3833, 37bitr3d 281 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3938biimpd 229 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅)))
4039adantrd 491 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → -1 < (𝑡 / 𝑅)))
41 1red 11259 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
4226, 41, 36ltdivmuld 13125 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1)))
436mulridd 11275 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (𝑅 · 1) = 𝑅)
4443adantr 480 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅 · 1) = 𝑅)
4544breq2d 5159 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅))
4642, 45bitr2d 280 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1))
4746biimpd 229 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1))
4847adantld 490 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) < 1))
4930, 40, 483jcad 1128 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5049exp4b 430 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))))
51503impd 1347 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5225, 51sylbid 240 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5352imp 406 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5434rexri 11316 . . . . . 6 -1 ∈ ℝ*
55 1xr 11317 . . . . . 6 1 ∈ ℝ*
56 elioo2 13424 . . . . . 6 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5754, 55, 56mp2an 692 . . . . 5 ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5853, 57sylibr 234 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1))
59 ovexd 7465 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V)
60 elioore 13413 . . . . . . 7 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℝ)
6160recnd 11286 . . . . . 6 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℂ)
62 asincl 26930 . . . . . . 7 (𝑢 ∈ ℂ → (arcsin‘𝑢) ∈ ℂ)
63 id 22 . . . . . . . 8 (𝑢 ∈ ℂ → 𝑢 ∈ ℂ)
64 1cnd 11253 . . . . . . . . . 10 (𝑢 ∈ ℂ → 1 ∈ ℂ)
65 sqcl 14154 . . . . . . . . . 10 (𝑢 ∈ ℂ → (𝑢↑2) ∈ ℂ)
6664, 65subcld 11617 . . . . . . . . 9 (𝑢 ∈ ℂ → (1 − (𝑢↑2)) ∈ ℂ)
6766sqrtcld 15472 . . . . . . . 8 (𝑢 ∈ ℂ → (√‘(1 − (𝑢↑2))) ∈ ℂ)
6863, 67mulcld 11278 . . . . . . 7 (𝑢 ∈ ℂ → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
6962, 68addcld 11277 . . . . . 6 (𝑢 ∈ ℂ → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7061, 69syl 17 . . . . 5 (𝑢 ∈ (-1(,)1) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7170adantl 481 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
72 ovexd 7465 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (2 · (√‘(1 − (𝑢↑2)))) ∈ V)
73 recn 11242 . . . . . . 7 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
7473adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
75 1cnd 11253 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℂ)
762dvmptid 26009 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
77 ioossre 13444 . . . . . . 7 (-𝑅(,)𝑅) ⊆ ℝ
7877a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ⊆ ℝ)
79 eqid 2734 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8079tgioo2 24838 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
81 iooretop 24801 . . . . . . 7 (-𝑅(,)𝑅) ∈ (topGen‘ran (,))
8281a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ∈ (topGen‘ran (,)))
832, 74, 75, 76, 78, 80, 79, 82dvmptres 26015 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1))
842, 5, 13, 83, 6, 8dvmptdivc 26017 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅)))
8561, 62syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (arcsin‘𝑢) ∈ ℂ)
8685adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (arcsin‘𝑢) ∈ ℂ)
87 ovexd 7465 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 / (√‘(1 − (𝑢↑2)))) ∈ V)
88 asinf 26929 . . . . . . . . . 10 arcsin:ℂ⟶ℂ
8988a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → arcsin:ℂ⟶ℂ)
90 ioossre 13444 . . . . . . . . . . 11 (-1(,)1) ⊆ ℝ
91 ax-resscn 11209 . . . . . . . . . . 11 ℝ ⊆ ℂ
9290, 91sstri 4004 . . . . . . . . . 10 (-1(,)1) ⊆ ℂ
9392a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℂ)
9489, 93feqresmpt 6977 . . . . . . . 8 (𝑅 ∈ ℝ+ → (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))
9594oveq2d 7446 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))))
96 dvreasin 37692 . . . . . . 7 (ℝ D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2)))))
9795, 96eqtr3di 2789 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2))))))
9861, 68syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
9998adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
100 ovexd 7465 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V)
10161adantl 481 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 𝑢 ∈ ℂ)
102 1cnd 11253 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 1 ∈ ℂ)
103 recn 11242 . . . . . . . . 9 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
104103adantl 481 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 𝑢 ∈ ℂ)
105 1cnd 11253 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 1 ∈ ℂ)
1062dvmptid 26009 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 𝑢)) = (𝑢 ∈ ℝ ↦ 1))
10790a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℝ)
108 iooretop 24801 . . . . . . . . 9 (-1(,)1) ∈ (topGen‘ran (,))
109108a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ∈ (topGen‘ran (,)))
1102, 104, 105, 106, 107, 80, 79, 109dvmptres 26015 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ 𝑢)) = (𝑢 ∈ (-1(,)1) ↦ 1))
11161, 67syl 17 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
112111adantl 481 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
113 ovexd 7465 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ V)
114 1red 11259 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 1 ∈ ℝ)
11560resqcld 14161 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℝ)
116114, 115resubcld 11688 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ)
117 elioo2 13424 . . . . . . . . . . . . 13 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1)))
11854, 55, 117mp2an 692 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1))
119 id 22 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ)
120 1red 11259 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 1 ∈ ℝ)
121119, 120absltd 15464 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ (-1 < 𝑢𝑢 < 1)))
122103abscld 15471 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
123103absge0d 15479 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
124 0le1 11783 . . . . . . . . . . . . . . . . . 18 0 ≤ 1
125124a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ 1)
126122, 120, 123, 125lt2sqd 14291 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ ((abs‘𝑢)↑2) < (1↑2)))
127 absresq 15337 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
128 sq1 14230 . . . . . . . . . . . . . . . . . 18 (1↑2) = 1
129128a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (1↑2) = 1)
130127, 129breq12d 5160 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → (((abs‘𝑢)↑2) < (1↑2) ↔ (𝑢↑2) < 1))
131 resqcl 14160 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
132131, 120posdifd 11847 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1 − (𝑢↑2))))
133126, 130, 1323bitrd 305 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ 0 < (1 − (𝑢↑2))))
134121, 133bitr3d 281 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) ↔ 0 < (1 − (𝑢↑2))))
135134biimpd 229 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2))))
1361353impib 1115 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2)))
137118, 136sylbi 217 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 0 < (1 − (𝑢↑2)))
138116, 137elrpd 13071 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ+)
139138adantl 481 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 − (𝑢↑2)) ∈ ℝ+)
140 negex 11503 . . . . . . . . . 10 -(2 · 𝑢) ∈ V
141140a1i 11 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → -(2 · 𝑢) ∈ V)
142 rpcn 13042 . . . . . . . . . . 11 (𝑣 ∈ ℝ+𝑣 ∈ ℂ)
143142sqrtcld 15472 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (√‘𝑣) ∈ ℂ)
144143adantl 481 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (√‘𝑣) ∈ ℂ)
145 ovexd 7465 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V)
146 1cnd 11253 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 1 ∈ ℂ)
147103sqcld 14180 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℂ)
148146, 147subcld 11617 . . . . . . . . . . 11 (𝑢 ∈ ℝ → (1 − (𝑢↑2)) ∈ ℂ)
149148adantl 481 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (1 − (𝑢↑2)) ∈ ℂ)
150140a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → -(2 · 𝑢) ∈ V)
151 0red 11261 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 0 ∈ ℝ)
152 1cnd 11253 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → 1 ∈ ℂ)
1532, 152dvmptc 26010 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 1)) = (𝑢 ∈ ℝ ↦ 0))
154147adantl 481 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℂ)
155 ovexd 7465 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (2 · 𝑢) ∈ V)
15679cnfldtopon 24818 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
157 toponmax 22947 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
158156, 157mp1i 13 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ℂ ∈ (TopOpen‘ℂfld))
159 dfss2 3980 . . . . . . . . . . . . . . 15 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
16091, 159mpbi 230 . . . . . . . . . . . . . 14 (ℝ ∩ ℂ) = ℝ
161160a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ ∩ ℂ) = ℝ)
16265adantl 481 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (𝑢↑2) ∈ ℂ)
163 ovexd 7465 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (2 · 𝑢) ∈ V)
164 2nn 12336 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
165 dvexp 26005 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))))
166164, 165ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1))))
167 2m1e1 12389 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
168167oveq2i 7441 . . . . . . . . . . . . . . . . . 18 (𝑢↑(2 − 1)) = (𝑢↑1)
169 exp1 14104 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢)
170168, 169eqtrid 2786 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢)
171170oveq2d 7446 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℂ → (2 · (𝑢↑(2 − 1))) = (2 · 𝑢))
172171mpteq2ia 5250 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
173166, 172eqtri 2762 . . . . . . . . . . . . . 14 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
174173a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢)))
17579, 2, 158, 161, 162, 163, 174dvmptres3 26008 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢)))
1762, 105, 151, 153, 154, 155, 175dvmptsub 26019 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢))))
177 df-neg 11492 . . . . . . . . . . . 12 -(2 · 𝑢) = (0 − (2 · 𝑢))
178177mpteq2i 5252 . . . . . . . . . . 11 (𝑢 ∈ ℝ ↦ -(2 · 𝑢)) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢)))
179176, 178eqtr4di 2792 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢)))
1802, 149, 150, 179, 107, 80, 79, 109dvmptres 26015 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢)))
181 dvsqrt 26798 . . . . . . . . . 10 (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣))))
182181a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣)))))
183 fveq2 6906 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (√‘𝑣) = (√‘(1 − (𝑢↑2))))
184183oveq2d 7446 . . . . . . . . . 10 (𝑣 = (1 − (𝑢↑2)) → (2 · (√‘𝑣)) = (2 · (√‘(1 − (𝑢↑2)))))
185184oveq2d 7446 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (1 / (2 · (√‘𝑣))) = (1 / (2 · (√‘(1 − (𝑢↑2))))))
1862, 2, 139, 141, 144, 145, 180, 182, 183, 185dvmptco 26024 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))))
187 2cnd 12341 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 2 ∈ ℂ)
188187, 61mulneg2d 11714 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · -𝑢) = -(2 · 𝑢))
189188oveq1d 7445 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))))
19061negcld 11604 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -𝑢 ∈ ℂ)
191137gt0ne0d 11824 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ≠ 0)
19261, 66syl 17 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℂ)
193192adantr 480 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈ ℂ)
194 simpr 484 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (√‘(1 − (𝑢↑2))) = 0)
195193, 194sqr00d 15476 . . . . . . . . . . . . . 14 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0)
196195ex 412 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0))
197196necon3d 2958 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → ((1 − (𝑢↑2)) ≠ 0 → (√‘(1 − (𝑢↑2))) ≠ 0))
198191, 197mpd 15 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ≠ 0)
199 2ne0 12367 . . . . . . . . . . . 12 2 ≠ 0
200199a1i 11 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 2 ≠ 0)
201190, 111, 187, 198, 200divcan5d 12066 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
202187, 61mulcld 11278 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (2 · 𝑢) ∈ ℂ)
203202negcld 11604 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(2 · 𝑢) ∈ ℂ)
204187, 111mulcld 11278 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
205187, 111, 200, 198mulne0d 11912 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ≠ 0)
206203, 204, 205divrec2d 12044 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))
207189, 201, 2063eqtr3rd 2783 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
208207mpteq2ia 5250 . . . . . . . 8 (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))
209186, 208eqtrdi 2790 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))))
2102, 101, 102, 110, 112, 113, 209dvmptmul 26013 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (𝑢 · (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))))
2112, 86, 87, 97, 99, 100, 210dvmptadd 26012 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))))
212111mullidd 11276 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 · (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
213190, 111, 198divcld 12040 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
214213, 61mulcomd 11279 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21561, 190, 111, 198divassd 12075 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21661, 61mulneg2d 11714 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢))
21761sqvald 14179 . . . . . . . . . . . . . 14 (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢))
218217negeqd 11499 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢))
219216, 218eqtr4d 2777 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2))
220219oveq1d 7445 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
221214, 215, 2203eqtr2d 2780 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
222212, 221oveq12d 7448 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
22361sqcld 14180 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℂ)
224223negcld 11604 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈ ℂ)
225224, 111, 198divcld 12040 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
226111, 225addcomd 11460 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
227222, 226eqtrd 2774 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
228227oveq2d 7446 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
2291112timesd 12506 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) = ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))))
23064, 65negsubd 11623 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = (1 − (𝑢↑2)))
23166sqsqrtd 15474 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2)))
23267sqvald 14179 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
233230, 231, 2323eqtr2d 2780 . . . . . . . . . . . 12 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
23461, 233syl 17 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
235234oveq1d 7445 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))))
236 1cnd 11253 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 1 ∈ ℂ)
237236, 224, 111, 198divdird 12078 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
238111, 111, 198divcan3d 12045 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
239235, 237, 2383eqtr3rd 2783 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
240239oveq1d 7445 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))))
241111, 198reccld 12033 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (1 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
242241, 225, 111addassd 11280 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
243229, 240, 2423eqtrrd 2779 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))) = (2 · (√‘(1 − (𝑢↑2)))))
244228, 243eqtrd 2774 . . . . . 6 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = (2 · (√‘(1 − (𝑢↑2)))))
245244mpteq2ia 5250 . . . . 5 (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2)))))
246211, 245eqtrdi 2790 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2))))))
247 fveq2 6906 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅)))
248 id 22 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅))
249 oveq1 7437 . . . . . . . 8 (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2))
250249oveq2d 7446 . . . . . . 7 (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2)))
251250fveq2d 6910 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
252248, 251oveq12d 7448 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
253247, 252oveq12d 7448 . . . 4 (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) = ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
254251oveq2d 7446 . . . 4 (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1 − (𝑢↑2)))) = (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
2552, 2, 58, 59, 71, 72, 84, 246, 253, 254dvmptco 26024 . . 3 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))
2566sqcld 14180 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
2572, 18, 19, 255, 256dvmptcmul 26016 . 2 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))))
258 2cnd 12341 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ)
259258, 16mulcld 11278 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
2606, 8reccld 12033 . . . . . . 7 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
261260adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ)
262259, 261mulcomd 11279 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
263262oveq2d 7446 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
264256adantr 480 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ)
265264, 261, 259mulassd 11281 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2666sqvald 14179 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) = (𝑅 · 𝑅))
267266oveq1d 7445 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅))
268256, 6, 8divrecd 12043 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅)))
2696, 6, 8divcan3d 12045 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅 · 𝑅) / 𝑅) = 𝑅)
270267, 268, 2693eqtr3d 2782 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
271270adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
272271oveq1d 7445 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
2737, 258, 16mul12d 11467 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
27420resqcld 14161 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
275274adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ)
27620sqge0d 14173 . . . . . . . . 9 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
277276adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2))
278 1red 11259 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ)
2793adantl 481 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ)
28020adantr 480 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
281279, 280, 9redivcld 12092 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
282281resqcld 14161 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
283278, 282resubcld 11688 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
284 0red 11261 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
28526, 27absltd 15464 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
28673abscld 15471 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
287286adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
28873absge0d 15479 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
289288adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
290 rpge0 13045 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
291290adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
292287, 27, 289, 291lt2sqd 14291 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
293 absresq 15337 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
294293adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
295256adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
296295mulridd 11275 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) · 1) = (𝑅↑2))
297296eqcomd 2740 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) = ((𝑅↑2) · 1))
298294, 297breq12d 5160 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
2996adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
30074, 299, 28sqdivd 14195 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
301300breq1d 5157 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1))
30229resqcld 14161 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
303302, 41posdifd 11847 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
304 resqcl 14160 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
305304adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
306 rpgt0 13044 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → 0 < 𝑅)
307 0red 11261 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
308 0le0 12364 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
309308a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ≤ 0)
310307, 20, 309, 290lt2sqd 14291 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
311 sq0 14227 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
312311a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0↑2) = 0)
313312breq1d 5157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
314310, 313bitrd 279 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
315306, 314mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
316274, 315elrpd 13071 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
317316adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
318305, 41, 317ltdivmuld 13125 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) < 1 ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
319301, 303, 3183bitr3rd 310 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < ((𝑅↑2) · 1) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
320292, 298, 3193bitrd 305 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
321285, 320bitr3d 281 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
322321biimpd 229 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
323322exp4b 430 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2))))))
3243233impd 1347 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
32525, 324sylbid 240 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
326325imp 406 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2)))
327284, 283, 326ltled 11406 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
328275, 277, 283, 327sqrtmuld 15459 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
329264, 13, 14subdid 11716 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
330264mulridd 11275 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
3315, 7, 9sqdivd 14195 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
332331oveq2d 7446 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
3334sqcld 14180 . . . . . . . . . . . . 13 (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ)
334333adantl 481 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ)
335 sqne0 14159 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3366, 335syl 17 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3378, 336mpbird 257 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
338337adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0)
339334, 264, 338divcan2d 12042 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
340332, 339eqtrd 2774 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
341330, 340oveq12d 7448 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
342329, 341eqtrd 2774 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
343342fveq2d 6910 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
34420, 290sqrtsqd 15454 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (√‘(𝑅↑2)) = 𝑅)
345344adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅)
346345oveq1d 7445 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
347328, 343, 3463eqtr3rd 2783 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
348347oveq2d 7446 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
349272, 273, 3483eqtrd 2778 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
350263, 265, 3493eqtr2d 2780 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
351350mpteq2dva 5247 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
352257, 351eqtrd 2774 1 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  Vcvv 3477  cin 3961  wss 3962  {cpr 4632   class class class wbr 5147  cmpt 5230  ran crn 5689  cres 5690  wf 6558  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  *cxr 11291   < clt 11292  cle 11293  cmin 11489  -cneg 11490   / cdiv 11917  cn 12263  2c2 12318  +crp 13031  (,)cioo 13383  cexp 14098  csqrt 15268  abscabs 15269  TopOpenctopn 17467  topGenctg 17483  fldccnfld 21381  TopOnctopon 22931   D cdv 25912  arcsincasin 26919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-tan 16103  df-pi 16104  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916  df-log 26612  df-cxp 26613  df-asin 26922
This theorem is referenced by:  areacirc  37699
  Copyright terms: Public domain W3C validator