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 33630
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 10066 . . . 4 ℝ ∈ {ℝ, ℂ}
21a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℝ ∈ {ℝ, ℂ})
3 elioore 12243 . . . . . . . 8 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
43recnd 10106 . . . . . . 7 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ)
54adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ)
6 rpcn 11879 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
76adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ)
8 rpne0 11886 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ≠ 0)
98adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0)
105, 7, 9divcld 10839 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
11 asincl 24645 . . . . 5 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
1210, 11syl 17 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
13 1cnd 10094 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ)
1410sqcld 13046 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
1513, 14subcld 10430 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
1615sqrtcld 14220 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
1710, 16mulcld 10098 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
1812, 17addcld 10097 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ℂ)
19 ovexd 6720 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V)
20 rpre 11877 . . . . . . . . . 10 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
2120renegcld 10495 . . . . . . . . 9 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
2221rexrd 10127 . . . . . . . 8 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ*)
23 rpxr 11878 . . . . . . . 8 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
24 elioo2 12254 . . . . . . . 8 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
2522, 23, 24syl2anc 694 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
26 simpr 476 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2720adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
288adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
2926, 27, 28redivcld 10891 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
3029a1d 25 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ))
316mulm1d 10520 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (-1 · 𝑅) = -𝑅)
3231adantr 480 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-1 · 𝑅) = -𝑅)
3332breq1d 4695 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -𝑅 < 𝑡))
34 neg1rr 11163 . . . . . . . . . . . . . . 15 -1 ∈ ℝ
3534a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → -1 ∈ ℝ)
36 simpl 472 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ+)
3735, 26, 36ltmuldivd 11957 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3833, 37bitr3d 270 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3938biimpd 219 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅)))
4039adantrd 483 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → -1 < (𝑡 / 𝑅)))
41 1red 10093 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
4226, 41, 36ltdivmuld 11961 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1)))
436mulid1d 10095 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (𝑅 · 1) = 𝑅)
4443adantr 480 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅 · 1) = 𝑅)
4544breq2d 4697 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅))
4642, 45bitr2d 269 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1))
4746biimpd 219 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1))
4847adantld 482 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) < 1))
4930, 40, 483jcad 1262 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5049exp4b 631 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))))
51503impd 1303 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5225, 51sylbid 230 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5352imp 444 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5434rexri 10135 . . . . . 6 -1 ∈ ℝ*
55 1re 10077 . . . . . . 7 1 ∈ ℝ
5655rexri 10135 . . . . . 6 1 ∈ ℝ*
57 elioo2 12254 . . . . . 6 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5854, 56, 57mp2an 708 . . . . 5 ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5953, 58sylibr 224 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1))
60 ovexd 6720 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V)
61 elioore 12243 . . . . . . 7 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℝ)
6261recnd 10106 . . . . . 6 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℂ)
63 asincl 24645 . . . . . . 7 (𝑢 ∈ ℂ → (arcsin‘𝑢) ∈ ℂ)
64 id 22 . . . . . . . 8 (𝑢 ∈ ℂ → 𝑢 ∈ ℂ)
65 1cnd 10094 . . . . . . . . . 10 (𝑢 ∈ ℂ → 1 ∈ ℂ)
66 sqcl 12965 . . . . . . . . . 10 (𝑢 ∈ ℂ → (𝑢↑2) ∈ ℂ)
6765, 66subcld 10430 . . . . . . . . 9 (𝑢 ∈ ℂ → (1 − (𝑢↑2)) ∈ ℂ)
6867sqrtcld 14220 . . . . . . . 8 (𝑢 ∈ ℂ → (√‘(1 − (𝑢↑2))) ∈ ℂ)
6964, 68mulcld 10098 . . . . . . 7 (𝑢 ∈ ℂ → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
7063, 69addcld 10097 . . . . . 6 (𝑢 ∈ ℂ → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7162, 70syl 17 . . . . 5 (𝑢 ∈ (-1(,)1) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7271adantl 481 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
73 ovexd 6720 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (2 · (√‘(1 − (𝑢↑2)))) ∈ V)
74 recn 10064 . . . . . . 7 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
7574adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
76 1cnd 10094 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℂ)
772dvmptid 23765 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
78 ioossre 12273 . . . . . . 7 (-𝑅(,)𝑅) ⊆ ℝ
7978a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ⊆ ℝ)
80 eqid 2651 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8180tgioo2 22653 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
82 iooretop 22616 . . . . . . 7 (-𝑅(,)𝑅) ∈ (topGen‘ran (,))
8382a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ∈ (topGen‘ran (,)))
842, 75, 76, 77, 79, 81, 80, 83dvmptres 23771 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1))
852, 5, 13, 84, 6, 8dvmptdivc 23773 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅)))
8662, 63syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (arcsin‘𝑢) ∈ ℂ)
8786adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (arcsin‘𝑢) ∈ ℂ)
88 ovexd 6720 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 / (√‘(1 − (𝑢↑2)))) ∈ V)
89 dvreasin 33628 . . . . . . 7 (ℝ D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2)))))
90 asinf 24644 . . . . . . . . . 10 arcsin:ℂ⟶ℂ
9190a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → arcsin:ℂ⟶ℂ)
92 ioossre 12273 . . . . . . . . . . 11 (-1(,)1) ⊆ ℝ
93 ax-resscn 10031 . . . . . . . . . . 11 ℝ ⊆ ℂ
9492, 93sstri 3645 . . . . . . . . . 10 (-1(,)1) ⊆ ℂ
9594a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℂ)
9691, 95feqresmpt 6289 . . . . . . . 8 (𝑅 ∈ ℝ+ → (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))
9796oveq2d 6706 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))))
9889, 97syl5reqr 2700 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2))))))
9962, 69syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
10099adantl 481 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
101 ovexd 6720 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V)
10262adantl 481 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 𝑢 ∈ ℂ)
103 1cnd 10094 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 1 ∈ ℂ)
104 recn 10064 . . . . . . . . 9 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
105104adantl 481 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 𝑢 ∈ ℂ)
106 1cnd 10094 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 1 ∈ ℂ)
1072dvmptid 23765 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 𝑢)) = (𝑢 ∈ ℝ ↦ 1))
10892a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℝ)
109 iooretop 22616 . . . . . . . . 9 (-1(,)1) ∈ (topGen‘ran (,))
110109a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ∈ (topGen‘ran (,)))
1112, 105, 106, 107, 108, 81, 80, 110dvmptres 23771 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ 𝑢)) = (𝑢 ∈ (-1(,)1) ↦ 1))
11262, 68syl 17 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
113112adantl 481 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
114 ovexd 6720 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ V)
115 1red 10093 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 1 ∈ ℝ)
11661resqcld 13075 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℝ)
117115, 116resubcld 10496 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ)
118 elioo2 12254 . . . . . . . . . . . . 13 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1)))
11954, 56, 118mp2an 708 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1))
120 id 22 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ)
121 1red 10093 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 1 ∈ ℝ)
122120, 121absltd 14212 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ (-1 < 𝑢𝑢 < 1)))
123104abscld 14219 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
124104absge0d 14227 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
125 0le1 10589 . . . . . . . . . . . . . . . . . 18 0 ≤ 1
126125a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ 1)
127123, 121, 124, 126lt2sqd 13083 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ ((abs‘𝑢)↑2) < (1↑2)))
128 absresq 14086 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
129 sq1 12998 . . . . . . . . . . . . . . . . . 18 (1↑2) = 1
130129a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (1↑2) = 1)
131128, 130breq12d 4698 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → (((abs‘𝑢)↑2) < (1↑2) ↔ (𝑢↑2) < 1))
132 resqcl 12971 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
133132, 121posdifd 10652 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1 − (𝑢↑2))))
134127, 131, 1333bitrd 294 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ 0 < (1 − (𝑢↑2))))
135122, 134bitr3d 270 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) ↔ 0 < (1 − (𝑢↑2))))
136135biimpd 219 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2))))
1371363impib 1281 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2)))
138119, 137sylbi 207 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 0 < (1 − (𝑢↑2)))
139117, 138elrpd 11907 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ+)
140139adantl 481 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 − (𝑢↑2)) ∈ ℝ+)
141 negex 10317 . . . . . . . . . 10 -(2 · 𝑢) ∈ V
142141a1i 11 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → -(2 · 𝑢) ∈ V)
143 rpcn 11879 . . . . . . . . . . 11 (𝑣 ∈ ℝ+𝑣 ∈ ℂ)
144143sqrtcld 14220 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (√‘𝑣) ∈ ℂ)
145144adantl 481 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (√‘𝑣) ∈ ℂ)
146 ovexd 6720 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V)
147 1cnd 10094 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 1 ∈ ℂ)
148104sqcld 13046 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℂ)
149147, 148subcld 10430 . . . . . . . . . . 11 (𝑢 ∈ ℝ → (1 − (𝑢↑2)) ∈ ℂ)
150149adantl 481 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (1 − (𝑢↑2)) ∈ ℂ)
151141a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → -(2 · 𝑢) ∈ V)
152 0red 10079 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 0 ∈ ℝ)
153 1cnd 10094 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → 1 ∈ ℂ)
1542, 153dvmptc 23766 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 1)) = (𝑢 ∈ ℝ ↦ 0))
155148adantl 481 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℂ)
156 ovexd 6720 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (2 · 𝑢) ∈ V)
15780cnfldtopon 22633 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
158 toponmax 20778 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
159157, 158mp1i 13 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ℂ ∈ (TopOpen‘ℂfld))
160 df-ss 3621 . . . . . . . . . . . . . . 15 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
16193, 160mpbi 220 . . . . . . . . . . . . . 14 (ℝ ∩ ℂ) = ℝ
162161a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ ∩ ℂ) = ℝ)
16366adantl 481 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (𝑢↑2) ∈ ℂ)
164 ovexd 6720 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (2 · 𝑢) ∈ V)
165 2nn 11223 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
166 dvexp 23761 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))))
167165, 166ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1))))
168 2m1e1 11173 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
169168oveq2i 6701 . . . . . . . . . . . . . . . . . 18 (𝑢↑(2 − 1)) = (𝑢↑1)
170 exp1 12906 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢)
171169, 170syl5eq 2697 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢)
172171oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℂ → (2 · (𝑢↑(2 − 1))) = (2 · 𝑢))
173172mpteq2ia 4773 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
174167, 173eqtri 2673 . . . . . . . . . . . . . 14 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
175174a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢)))
17680, 2, 159, 162, 163, 164, 175dvmptres3 23764 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢)))
1772, 106, 152, 154, 155, 156, 176dvmptsub 23775 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢))))
178 df-neg 10307 . . . . . . . . . . . 12 -(2 · 𝑢) = (0 − (2 · 𝑢))
179178mpteq2i 4774 . . . . . . . . . . 11 (𝑢 ∈ ℝ ↦ -(2 · 𝑢)) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢)))
180177, 179syl6eqr 2703 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢)))
1812, 150, 151, 180, 108, 81, 80, 110dvmptres 23771 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢)))
182 dvsqrt 24528 . . . . . . . . . 10 (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣))))
183182a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣)))))
184 fveq2 6229 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (√‘𝑣) = (√‘(1 − (𝑢↑2))))
185184oveq2d 6706 . . . . . . . . . 10 (𝑣 = (1 − (𝑢↑2)) → (2 · (√‘𝑣)) = (2 · (√‘(1 − (𝑢↑2)))))
186185oveq2d 6706 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (1 / (2 · (√‘𝑣))) = (1 / (2 · (√‘(1 − (𝑢↑2))))))
1872, 2, 140, 142, 145, 146, 181, 183, 184, 186dvmptco 23780 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))))
188 2cnd 11131 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 2 ∈ ℂ)
189188, 62mulneg2d 10522 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · -𝑢) = -(2 · 𝑢))
190189oveq1d 6705 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))))
19162negcld 10417 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -𝑢 ∈ ℂ)
192138gt0ne0d 10630 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ≠ 0)
19362, 67syl 17 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℂ)
194193adantr 480 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈ ℂ)
195 simpr 476 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (√‘(1 − (𝑢↑2))) = 0)
196194, 195sqr00d 14224 . . . . . . . . . . . . . 14 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0)
197196ex 449 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0))
198197necon3d 2844 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → ((1 − (𝑢↑2)) ≠ 0 → (√‘(1 − (𝑢↑2))) ≠ 0))
199192, 198mpd 15 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ≠ 0)
200 2ne0 11151 . . . . . . . . . . . 12 2 ≠ 0
201200a1i 11 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 2 ≠ 0)
202191, 112, 188, 199, 201divcan5d 10865 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
203188, 62mulcld 10098 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (2 · 𝑢) ∈ ℂ)
204203negcld 10417 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(2 · 𝑢) ∈ ℂ)
205188, 112mulcld 10098 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
206188, 112, 201, 199mulne0d 10717 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ≠ 0)
207204, 205, 206divrec2d 10843 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))
208190, 202, 2073eqtr3rd 2694 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
209208mpteq2ia 4773 . . . . . . . 8 (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))
210187, 209syl6eq 2701 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))))
2112, 102, 103, 111, 113, 114, 210dvmptmul 23769 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (𝑢 · (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))))
2122, 87, 88, 98, 100, 101, 211dvmptadd 23768 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))))
213112mulid2d 10096 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 · (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
214191, 112, 199divcld 10839 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
215214, 62mulcomd 10099 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21662, 191, 112, 199divassd 10874 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21762, 62mulneg2d 10522 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢))
21862sqvald 13045 . . . . . . . . . . . . . 14 (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢))
219218negeqd 10313 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢))
220217, 219eqtr4d 2688 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2))
221220oveq1d 6705 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
222215, 216, 2213eqtr2d 2691 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
223213, 222oveq12d 6708 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
22462sqcld 13046 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℂ)
225224negcld 10417 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈ ℂ)
226225, 112, 199divcld 10839 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
227112, 226addcomd 10276 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
228223, 227eqtrd 2685 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
229228oveq2d 6706 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
2301122timesd 11313 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) = ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))))
23165, 66negsubd 10436 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = (1 − (𝑢↑2)))
23267sqsqrtd 14222 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2)))
23368sqvald 13045 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
234231, 232, 2333eqtr2d 2691 . . . . . . . . . . . 12 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
23562, 234syl 17 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
236235oveq1d 6705 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))))
237 1cnd 10094 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 1 ∈ ℂ)
238237, 225, 112, 199divdird 10877 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
239112, 112, 199divcan3d 10844 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
240236, 238, 2393eqtr3rd 2694 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
241240oveq1d 6705 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))))
242112, 199reccld 10832 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (1 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
243242, 226, 112addassd 10100 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
244230, 241, 2433eqtrrd 2690 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))) = (2 · (√‘(1 − (𝑢↑2)))))
245229, 244eqtrd 2685 . . . . . 6 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = (2 · (√‘(1 − (𝑢↑2)))))
246245mpteq2ia 4773 . . . . 5 (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2)))))
247212, 246syl6eq 2701 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2))))))
248 fveq2 6229 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅)))
249 id 22 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅))
250 oveq1 6697 . . . . . . . 8 (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2))
251250oveq2d 6706 . . . . . . 7 (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2)))
252251fveq2d 6233 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
253249, 252oveq12d 6708 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
254248, 253oveq12d 6708 . . . 4 (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) = ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
255252oveq2d 6706 . . . 4 (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1 − (𝑢↑2)))) = (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
2562, 2, 59, 60, 72, 73, 85, 247, 254, 255dvmptco 23780 . . 3 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))
2576sqcld 13046 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
2582, 18, 19, 256, 257dvmptcmul 23772 . 2 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))))
259 2cnd 11131 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ)
260259, 16mulcld 10098 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
2616, 8reccld 10832 . . . . . . 7 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
262261adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ)
263260, 262mulcomd 10099 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
264263oveq2d 6706 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
265257adantr 480 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ)
266265, 262, 260mulassd 10101 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2676sqvald 13045 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) = (𝑅 · 𝑅))
268267oveq1d 6705 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅))
269257, 6, 8divrecd 10842 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅)))
2706, 6, 8divcan3d 10844 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅 · 𝑅) / 𝑅) = 𝑅)
271268, 269, 2703eqtr3d 2693 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
272271adantr 480 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
273272oveq1d 6705 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
2747, 259, 16mul12d 10283 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
27520resqcld 13075 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
276275adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ)
27720sqge0d 13076 . . . . . . . . 9 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
278277adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2))
279 1red 10093 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ)
2803adantl 481 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ)
28120adantr 480 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
282280, 281, 9redivcld 10891 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
283282resqcld 13075 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
284279, 283resubcld 10496 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
285 0red 10079 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
28626, 27absltd 14212 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
28774abscld 14219 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
288287adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
28974absge0d 14227 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
290289adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
291 rpge0 11883 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
292291adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
293288, 27, 290, 292lt2sqd 13083 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
294 absresq 14086 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
295294adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
296257adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
297296mulid1d 10095 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) · 1) = (𝑅↑2))
298297eqcomd 2657 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) = ((𝑅↑2) · 1))
299295, 298breq12d 4698 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
3006adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
30175, 300, 28sqdivd 13061 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
302301breq1d 4695 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1))
30329resqcld 13075 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
304303, 41posdifd 10652 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
305 resqcl 12971 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
306305adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
307 rpgt0 11882 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → 0 < 𝑅)
308 0red 10079 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
309 0le0 11148 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
310309a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ≤ 0)
311308, 20, 310, 291lt2sqd 13083 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
312 sq0 12995 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
313312a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0↑2) = 0)
314313breq1d 4695 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
315311, 314bitrd 268 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
316307, 315mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
317275, 316elrpd 11907 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
318317adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
319306, 41, 318ltdivmuld 11961 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) < 1 ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
320302, 304, 3193bitr3rd 299 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < ((𝑅↑2) · 1) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
321293, 299, 3203bitrd 294 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
322286, 321bitr3d 270 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
323322biimpd 219 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
324323exp4b 631 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2))))))
3253243impd 1303 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
32625, 325sylbid 230 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
327326imp 444 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2)))
328285, 284, 327ltled 10223 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
329276, 278, 284, 328sqrtmuld 14207 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
330265, 13, 14subdid 10524 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
331265mulid1d 10095 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
3325, 7, 9sqdivd 13061 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
333332oveq2d 6706 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
3344sqcld 13046 . . . . . . . . . . . . 13 (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ)
335334adantl 481 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ)
336 sqne0 12970 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3376, 336syl 17 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3388, 337mpbird 247 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
339338adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0)
340335, 265, 339divcan2d 10841 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
341333, 340eqtrd 2685 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
342331, 341oveq12d 6708 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
343330, 342eqtrd 2685 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
344343fveq2d 6233 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
34520, 291sqrtsqd 14202 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (√‘(𝑅↑2)) = 𝑅)
346345adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅)
347346oveq1d 6705 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
348329, 344, 3473eqtr3rd 2694 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
349348oveq2d 6706 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
350273, 274, 3493eqtrd 2689 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
351264, 266, 3503eqtr2d 2691 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
352351mpteq2dva 4777 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
353258, 352eqtrd 2685 1 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  Vcvv 3231  cin 3606  wss 3607  {cpr 4212   class class class wbr 4685  cmpt 4762  ran crn 5144  cres 5145  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  *cxr 10111   < clt 10112  cle 10113  cmin 10304  -cneg 10305   / cdiv 10722  cn 11058  2c2 11108  +crp 11870  (,)cioo 12213  cexp 12900  csqrt 14017  abscabs 14018  TopOpenctopn 16129  topGenctg 16145  fldccnfld 19794  TopOnctopon 20763   D cdv 23672  arcsincasin 24634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-tan 14846  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-cxp 24349  df-asin 24637
This theorem is referenced by:  areacirc  33635
  Copyright terms: Public domain W3C validator