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 33979
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 10314 . . . 4 ℝ ∈ {ℝ, ℂ}
21a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℝ ∈ {ℝ, ℂ})
3 elioore 12450 . . . . . . . 8 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
43recnd 10355 . . . . . . 7 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ)
54adantl 474 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ)
6 rpcn 12082 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
76adantr 473 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ)
8 rpne0 12088 . . . . . . 7 (𝑅 ∈ ℝ+𝑅 ≠ 0)
98adantr 473 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0)
105, 7, 9divcld 11091 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
11 asincl 24948 . . . . 5 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
1210, 11syl 17 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ)
13 1cnd 10321 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ)
1410sqcld 13256 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
1513, 14subcld 10682 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
1615sqrtcld 14513 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
1710, 16mulcld 10347 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
1812, 17addcld 10346 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ℂ)
19 ovexd 6910 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V)
20 rpre 12078 . . . . . . . . . 10 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
2120renegcld 10747 . . . . . . . . 9 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
2221rexrd 10376 . . . . . . . 8 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ*)
23 rpxr 12081 . . . . . . . 8 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
24 elioo2 12461 . . . . . . . 8 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
2522, 23, 24syl2anc 580 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
26 simpr 478 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2720adantr 473 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
288adantr 473 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
2926, 27, 28redivcld 11143 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
3029a1d 25 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ))
316mulm1d 10772 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (-1 · 𝑅) = -𝑅)
3231adantr 473 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-1 · 𝑅) = -𝑅)
3332breq1d 4851 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -𝑅 < 𝑡))
34 neg1rr 11431 . . . . . . . . . . . . . . 15 -1 ∈ ℝ
3534a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → -1 ∈ ℝ)
36 simpl 475 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ+)
3735, 26, 36ltmuldivd 12160 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-1 · 𝑅) < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3833, 37bitr3d 273 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅)))
3938biimpd 221 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅)))
4039adantrd 486 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → -1 < (𝑡 / 𝑅)))
41 1red 10327 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
4226, 41, 36ltdivmuld 12164 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1)))
436mulid1d 10344 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (𝑅 · 1) = 𝑅)
4443adantr 473 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅 · 1) = 𝑅)
4544breq2d 4853 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅))
4642, 45bitr2d 272 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1))
4746biimpd 221 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1))
4847adantld 485 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (𝑡 / 𝑅) < 1))
4930, 40, 483jcad 1160 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5049exp4b 422 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))))
51503impd 1458 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5225, 51sylbid 232 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5352imp 396 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5434rexri 10385 . . . . . 6 -1 ∈ ℝ*
55 1re 10326 . . . . . . 7 1 ∈ ℝ
5655rexri 10385 . . . . . 6 1 ∈ ℝ*
57 elioo2 12461 . . . . . 6 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)))
5854, 56, 57mp2an 684 . . . . 5 ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))
5953, 58sylibr 226 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1))
60 ovexd 6910 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V)
61 elioore 12450 . . . . . . 7 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℝ)
6261recnd 10355 . . . . . 6 (𝑢 ∈ (-1(,)1) → 𝑢 ∈ ℂ)
63 asincl 24948 . . . . . . 7 (𝑢 ∈ ℂ → (arcsin‘𝑢) ∈ ℂ)
64 id 22 . . . . . . . 8 (𝑢 ∈ ℂ → 𝑢 ∈ ℂ)
65 1cnd 10321 . . . . . . . . . 10 (𝑢 ∈ ℂ → 1 ∈ ℂ)
66 sqcl 13175 . . . . . . . . . 10 (𝑢 ∈ ℂ → (𝑢↑2) ∈ ℂ)
6765, 66subcld 10682 . . . . . . . . 9 (𝑢 ∈ ℂ → (1 − (𝑢↑2)) ∈ ℂ)
6867sqrtcld 14513 . . . . . . . 8 (𝑢 ∈ ℂ → (√‘(1 − (𝑢↑2))) ∈ ℂ)
6964, 68mulcld 10347 . . . . . . 7 (𝑢 ∈ ℂ → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
7063, 69addcld 10346 . . . . . 6 (𝑢 ∈ ℂ → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7162, 70syl 17 . . . . 5 (𝑢 ∈ (-1(,)1) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
7271adantl 474 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) ∈ ℂ)
73 ovexd 6910 . . . 4 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (2 · (√‘(1 − (𝑢↑2)))) ∈ V)
74 recn 10312 . . . . . . 7 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
7574adantl 474 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
76 1cnd 10321 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℂ)
772dvmptid 24057 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
78 ioossre 12480 . . . . . . 7 (-𝑅(,)𝑅) ⊆ ℝ
7978a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ⊆ ℝ)
80 eqid 2797 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8180tgioo2 22930 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
82 iooretop 22893 . . . . . . 7 (-𝑅(,)𝑅) ∈ (topGen‘ran (,))
8382a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → (-𝑅(,)𝑅) ∈ (topGen‘ran (,)))
842, 75, 76, 77, 79, 81, 80, 83dvmptres 24063 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1))
852, 5, 13, 84, 6, 8dvmptdivc 24065 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅)))
8662, 63syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (arcsin‘𝑢) ∈ ℂ)
8786adantl 474 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (arcsin‘𝑢) ∈ ℂ)
88 ovexd 6910 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 / (√‘(1 − (𝑢↑2)))) ∈ V)
89 dvreasin 33977 . . . . . . 7 (ℝ D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2)))))
90 asinf 24947 . . . . . . . . . 10 arcsin:ℂ⟶ℂ
9190a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → arcsin:ℂ⟶ℂ)
92 ioossre 12480 . . . . . . . . . . 11 (-1(,)1) ⊆ ℝ
93 ax-resscn 10279 . . . . . . . . . . 11 ℝ ⊆ ℂ
9492, 93sstri 3805 . . . . . . . . . 10 (-1(,)1) ⊆ ℂ
9594a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℂ)
9691, 95feqresmpt 6473 . . . . . . . 8 (𝑅 ∈ ℝ+ → (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))
9796oveq2d 6892 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))))
9889, 97syl5reqr 2846 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑢↑2))))))
9962, 69syl 17 . . . . . . 7 (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
10099adantl 474 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (𝑢 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
101 ovexd 6910 . . . . . 6 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V)
10262adantl 474 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 𝑢 ∈ ℂ)
103 1cnd 10321 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → 1 ∈ ℂ)
104 recn 10312 . . . . . . . . 9 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
105104adantl 474 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 𝑢 ∈ ℂ)
106 1cnd 10321 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 1 ∈ ℂ)
1072dvmptid 24057 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 𝑢)) = (𝑢 ∈ ℝ ↦ 1))
10892a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ⊆ ℝ)
109 iooretop 22893 . . . . . . . . 9 (-1(,)1) ∈ (topGen‘ran (,))
110109a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (-1(,)1) ∈ (topGen‘ran (,)))
1112, 105, 106, 107, 108, 81, 80, 110dvmptres 24063 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ 𝑢)) = (𝑢 ∈ (-1(,)1) ↦ 1))
11262, 68syl 17 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
113112adantl 474 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (√‘(1 − (𝑢↑2))) ∈ ℂ)
114 ovexd 6910 . . . . . . 7 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ V)
115 1red 10327 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 1 ∈ ℝ)
11661resqcld 13287 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℝ)
117115, 116resubcld 10748 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ)
118 elioo2 12461 . . . . . . . . . . . . 13 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1)))
11954, 56, 118mp2an 684 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1))
120 id 22 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ)
121 1red 10327 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → 1 ∈ ℝ)
122120, 121absltd 14505 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ (-1 < 𝑢𝑢 < 1)))
123104abscld 14512 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
124104absge0d 14520 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
125 0le1 10841 . . . . . . . . . . . . . . . . . 18 0 ≤ 1
126125a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → 0 ≤ 1)
127123, 121, 124, 126lt2sqd 13295 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ ((abs‘𝑢)↑2) < (1↑2)))
128 absresq 14379 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
129 sq1 13208 . . . . . . . . . . . . . . . . . 18 (1↑2) = 1
130129a1i 11 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (1↑2) = 1)
131128, 130breq12d 4854 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → (((abs‘𝑢)↑2) < (1↑2) ↔ (𝑢↑2) < 1))
132 resqcl 13181 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
133132, 121posdifd 10904 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1 − (𝑢↑2))))
134127, 131, 1333bitrd 297 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℝ → ((abs‘𝑢) < 1 ↔ 0 < (1 − (𝑢↑2))))
135122, 134bitr3d 273 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) ↔ 0 < (1 − (𝑢↑2))))
136135biimpd 221 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → ((-1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2))))
1371363impib 1145 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ ∧ -1 < 𝑢𝑢 < 1) → 0 < (1 − (𝑢↑2)))
138119, 137sylbi 209 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 0 < (1 − (𝑢↑2)))
139117, 138elrpd 12110 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℝ+)
140139adantl 474 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → (1 − (𝑢↑2)) ∈ ℝ+)
141 negex 10568 . . . . . . . . . 10 -(2 · 𝑢) ∈ V
142141a1i 11 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑢 ∈ (-1(,)1)) → -(2 · 𝑢) ∈ V)
143 rpcn 12082 . . . . . . . . . . 11 (𝑣 ∈ ℝ+𝑣 ∈ ℂ)
144143sqrtcld 14513 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (√‘𝑣) ∈ ℂ)
145144adantl 474 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (√‘𝑣) ∈ ℂ)
146 ovexd 6910 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑣 ∈ ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V)
147 1cnd 10321 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 1 ∈ ℂ)
148104sqcld 13256 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℂ)
149147, 148subcld 10682 . . . . . . . . . . 11 (𝑢 ∈ ℝ → (1 − (𝑢↑2)) ∈ ℂ)
150149adantl 474 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (1 − (𝑢↑2)) ∈ ℂ)
151141a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → -(2 · 𝑢) ∈ V)
152 0red 10330 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → 0 ∈ ℝ)
153 1cnd 10321 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → 1 ∈ ℂ)
1542, 153dvmptc 24058 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ 1)) = (𝑢 ∈ ℝ ↦ 0))
155148adantl 474 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℂ)
156 ovexd 6910 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑢 ∈ ℝ) → (2 · 𝑢) ∈ V)
15780cnfldtopon 22910 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
158 toponmax 21055 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
159157, 158mp1i 13 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ℂ ∈ (TopOpen‘ℂfld))
160 df-ss 3781 . . . . . . . . . . . . . . 15 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
16193, 160mpbi 222 . . . . . . . . . . . . . 14 (ℝ ∩ ℂ) = ℝ
162161a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ ∩ ℂ) = ℝ)
16366adantl 474 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (𝑢↑2) ∈ ℂ)
164 ovexd 6910 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑢 ∈ ℂ) → (2 · 𝑢) ∈ V)
165 2nn 11382 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
166 dvexp 24053 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))))
167165, 166ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1))))
168 2m1e1 11442 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
169168oveq2i 6887 . . . . . . . . . . . . . . . . . 18 (𝑢↑(2 − 1)) = (𝑢↑1)
170 exp1 13116 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢)
171169, 170syl5eq 2843 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢)
172171oveq2d 6892 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ℂ → (2 · (𝑢↑(2 − 1))) = (2 · 𝑢))
173172mpteq2ia 4931 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 − 1)))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
174167, 173eqtri 2819 . . . . . . . . . . . . . 14 (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))
175174a1i 11 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢)))
17680, 2, 159, 162, 163, 164, 175dvmptres3 24056 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢)))
1772, 106, 152, 154, 155, 156, 176dvmptsub 24067 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢))))
178 df-neg 10557 . . . . . . . . . . . 12 -(2 · 𝑢) = (0 − (2 · 𝑢))
179178mpteq2i 4932 . . . . . . . . . . 11 (𝑢 ∈ ℝ ↦ -(2 · 𝑢)) = (𝑢 ∈ ℝ ↦ (0 − (2 · 𝑢)))
180177, 179syl6eqr 2849 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢)))
1812, 150, 151, 180, 108, 81, 80, 110dvmptres 24063 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢)))
182 dvsqrt 24823 . . . . . . . . . 10 (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣))))
183182a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (ℝ D (𝑣 ∈ ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑣)))))
184 fveq2 6409 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (√‘𝑣) = (√‘(1 − (𝑢↑2))))
185184oveq2d 6892 . . . . . . . . . 10 (𝑣 = (1 − (𝑢↑2)) → (2 · (√‘𝑣)) = (2 · (√‘(1 − (𝑢↑2)))))
186185oveq2d 6892 . . . . . . . . 9 (𝑣 = (1 − (𝑢↑2)) → (1 / (2 · (√‘𝑣))) = (1 / (2 · (√‘(1 − (𝑢↑2))))))
1872, 2, 140, 142, 145, 146, 181, 183, 184, 186dvmptco 24072 . . . . . . . 8 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))))
188 2cnd 11387 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → 2 ∈ ℂ)
189188, 62mulneg2d 10774 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · -𝑢) = -(2 · 𝑢))
190189oveq1d 6891 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))))
19162negcld 10669 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -𝑢 ∈ ℂ)
192138gt0ne0d 10882 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ≠ 0)
19362, 67syl 17 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (-1(,)1) → (1 − (𝑢↑2)) ∈ ℂ)
194193adantr 473 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈ ℂ)
195 simpr 478 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (√‘(1 − (𝑢↑2))) = 0)
196194, 195sqr00d 14517 . . . . . . . . . . . . . 14 ((𝑢 ∈ (-1(,)1) ∧ (√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0)
197196ex 402 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0))
198197necon3d 2990 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → ((1 − (𝑢↑2)) ≠ 0 → (√‘(1 − (𝑢↑2))) ≠ 0))
199192, 198mpd 15 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) ≠ 0)
200 2ne0 11420 . . . . . . . . . . . 12 2 ≠ 0
201200a1i 11 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 2 ≠ 0)
202191, 112, 188, 199, 201divcan5d 11117 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((2 · -𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
203188, 62mulcld 10347 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (2 · 𝑢) ∈ ℂ)
204203negcld 10669 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(2 · 𝑢) ∈ ℂ)
205188, 112mulcld 10347 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ∈ ℂ)
206188, 112, 201, 199mulne0d 10969 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) ≠ 0)
207204, 205, 206divrec2d 11095 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(2 · 𝑢) / (2 · (√‘(1 − (𝑢↑2))))) = ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))
208190, 202, 2073eqtr3rd 2840 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2)))))
209208mpteq2ia 4931 . . . . . . . 8 (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))
210187, 209syl6eq 2847 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))))
2112, 102, 103, 111, 113, 114, 210dvmptmul 24061 . . . . . 6 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ (𝑢 · (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))))
2122, 87, 88, 98, 100, 101, 211dvmptadd 24060 . . . . 5 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))))
213112mulid2d 10345 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (1 · (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
214191, 112, 199divcld 11091 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
215214, 62mulcomd 10348 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21662, 191, 112, 199divassd 11126 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2))))))
21762, 62mulneg2d 10774 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢))
21862sqvald 13255 . . . . . . . . . . . . . 14 (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢))
219218negeqd 10564 . . . . . . . . . . . . 13 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢))
220217, 219eqtr4d 2834 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2))
221220oveq1d 6891 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
222215, 216, 2213eqtr2d 2837 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))))
223213, 222oveq12d 6894 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
22462sqcld 13256 . . . . . . . . . . . 12 (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈ ℂ)
225224negcld 10669 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈ ℂ)
226225, 112, 199divcld 11091 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
227112, 226addcomd 10526 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
228223, 227eqtrd 2831 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2)))))
229228oveq2d 6892 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
2301122timesd 11559 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (2 · (√‘(1 − (𝑢↑2)))) = ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))))
23165, 66negsubd 10688 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = (1 − (𝑢↑2)))
23267sqsqrtd 14515 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2)))
23368sqvald 13255 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ → ((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
234231, 232, 2333eqtr2d 2837 . . . . . . . . . . . 12 (𝑢 ∈ ℂ → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
23562, 234syl 17 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → (1 + -(𝑢↑2)) = ((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))))
236235oveq1d 6891 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))))
237 1cnd 10321 . . . . . . . . . . 11 (𝑢 ∈ (-1(,)1) → 1 ∈ ℂ)
238237, 225, 112, 199divdird 11129 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → ((1 + -(𝑢↑2)) / (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
239112, 112, 199divcan3d 11096 . . . . . . . . . 10 (𝑢 ∈ (-1(,)1) → (((√‘(1 − (𝑢↑2))) · (√‘(1 − (𝑢↑2)))) / (√‘(1 − (𝑢↑2)))) = (√‘(1 − (𝑢↑2))))
240236, 238, 2393eqtr3rd 2840 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))))
241240oveq1d 6891 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → ((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))))
242112, 199reccld 11084 . . . . . . . . 9 (𝑢 ∈ (-1(,)1) → (1 / (√‘(1 − (𝑢↑2)))) ∈ ℂ)
243242, 226, 112addassd 10349 . . . . . . . 8 (𝑢 ∈ (-1(,)1) → (((1 / (√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))))
244230, 241, 2433eqtrrd 2836 . . . . . . 7 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1 − (𝑢↑2))))) = (2 · (√‘(1 − (𝑢↑2)))))
245229, 244eqtrd 2831 . . . . . 6 (𝑢 ∈ (-1(,)1) → ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢))) = (2 · (√‘(1 − (𝑢↑2)))))
246245mpteq2ia 4931 . . . . 5 (𝑢 ∈ (-1(,)1) ↦ ((1 / (√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2)))))
247212, 246syl6eq 2847 . . . 4 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2 · (√‘(1 − (𝑢↑2))))))
248 fveq2 6409 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅)))
249 id 22 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅))
250 oveq1 6883 . . . . . . . 8 (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2))
251250oveq2d 6892 . . . . . . 7 (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2)))
252251fveq2d 6413 . . . . . 6 (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
253249, 252oveq12d 6894 . . . . 5 (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
254248, 253oveq12d 6894 . . . 4 (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) = ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
255252oveq2d 6892 . . . 4 (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1 − (𝑢↑2)))) = (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
2562, 2, 59, 60, 72, 73, 85, 247, 254, 255dvmptco 24072 . . 3 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))
2576sqcld 13256 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
2582, 18, 19, 256, 257dvmptcmul 24064 . 2 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))))
259 2cnd 11387 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ)
260259, 16mulcld 10347 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
2616, 8reccld 11084 . . . . . . 7 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
262261adantr 473 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ)
263260, 262mulcomd 10348 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
264263oveq2d 6892 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
265257adantr 473 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ)
266265, 262, 260mulassd 10350 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2676sqvald 13255 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) = (𝑅 · 𝑅))
268267oveq1d 6891 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅))
269257, 6, 8divrecd 11094 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅)))
2706, 6, 8divcan3d 11096 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅 · 𝑅) / 𝑅) = 𝑅)
271268, 269, 2703eqtr3d 2839 . . . . . . 7 (𝑅 ∈ ℝ+ → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
272271adantr 473 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅)
273272oveq1d 6891 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
2747, 259, 16mul12d 10533 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
27520resqcld 13287 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
276275adantr 473 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ)
27720sqge0d 13288 . . . . . . . . 9 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
278277adantr 473 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2))
279 1red 10327 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ)
2803adantl 474 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ)
28120adantr 473 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
282280, 281, 9redivcld 11143 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
283282resqcld 13287 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
284279, 283resubcld 10748 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
285 0red 10330 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
28626, 27absltd 14505 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
28774abscld 14512 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
288287adantl 474 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
28974absge0d 14520 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
290289adantl 474 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
291 rpge0 12085 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
292291adantr 473 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
293288, 27, 290, 292lt2sqd 13295 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
294 absresq 14379 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
295294adantl 474 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
296257adantr 473 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
297296mulid1d 10344 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) · 1) = (𝑅↑2))
298297eqcomd 2803 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) = ((𝑅↑2) · 1))
299295, 298breq12d 4854 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
3006adantr 473 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
30175, 300, 28sqdivd 13271 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
302301breq1d 4851 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1))
30329resqcld 13287 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
304303, 41posdifd 10904 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) < 1 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
305 resqcl 13181 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
306305adantl 474 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
307 rpgt0 12084 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → 0 < 𝑅)
308 0red 10330 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
309 0le0 11417 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
310309a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → 0 ≤ 0)
311308, 20, 310, 291lt2sqd 13295 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
312 sq0 13205 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
313312a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0↑2) = 0)
314313breq1d 4851 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
315311, 314bitrd 271 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
316307, 315mpbid 224 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
317275, 316elrpd 12110 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
318317adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
319306, 41, 318ltdivmuld 12164 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) < 1 ↔ (𝑡↑2) < ((𝑅↑2) · 1)))
320302, 304, 3193bitr3rd 302 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < ((𝑅↑2) · 1) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
321293, 299, 3203bitrd 297 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
322286, 321bitr3d 273 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2))))
323322biimpd 221 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
324323exp4b 422 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2))))))
3253243impd 1458 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
32625, 325sylbid 232 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2))))
327326imp 396 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2)))
328285, 284, 327ltled 10473 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
329276, 278, 284, 328sqrtmuld 14500 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
330265, 13, 14subdid 10776 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
331265mulid1d 10344 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
3325, 7, 9sqdivd 13271 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
333332oveq2d 6892 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
3344sqcld 13256 . . . . . . . . . . . . 13 (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ)
335334adantl 474 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ)
336 sqne0 13180 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3376, 336syl 17 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
3388, 337mpbird 249 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
339338adantr 473 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0)
340335, 265, 339divcan2d 11093 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
341333, 340eqtrd 2831 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
342331, 341oveq12d 6894 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
343330, 342eqtrd 2831 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
344343fveq2d 6413 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
34520, 291sqrtsqd 14495 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (√‘(𝑅↑2)) = 𝑅)
346345adantr 473 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅)
347346oveq1d 6891 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
348329, 344, 3473eqtr3rd 2840 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
349348oveq2d 6892 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
350273, 274, 3493eqtrd 2835 . . . 4 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
351264, 266, 3503eqtr2d 2837 . . 3 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
352351mpteq2dva 4935 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
353258, 352eqtrd 2831 1 (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157  wne 2969  Vcvv 3383  cin 3766  wss 3767  {cpr 4368   class class class wbr 4841  cmpt 4920  ran crn 5311  cres 5312  wf 6095  cfv 6099  (class class class)co 6876  cc 10220  cr 10221  0cc0 10222  1c1 10223   + caddc 10225   · cmul 10227  *cxr 10360   < clt 10361  cle 10362  cmin 10554  -cneg 10555   / cdiv 10974  cn 11310  2c2 11364  +crp 12070  (,)cioo 12420  cexp 13110  csqrt 14310  abscabs 14311  TopOpenctopn 16393  topGenctg 16409  fldccnfld 20064  TopOnctopon 21039   D cdv 23964  arcsincasin 24937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2375  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-inf2 8786  ax-cnex 10278  ax-resscn 10279  ax-1cn 10280  ax-icn 10281  ax-addcl 10282  ax-addrcl 10283  ax-mulcl 10284  ax-mulrcl 10285  ax-mulcom 10286  ax-addass 10287  ax-mulass 10288  ax-distr 10289  ax-i2m1 10290  ax-1ne0 10291  ax-1rid 10292  ax-rnegex 10293  ax-rrecex 10294  ax-cnre 10295  ax-pre-lttri 10296  ax-pre-lttrn 10297  ax-pre-ltadd 10298  ax-pre-mulgt0 10299  ax-pre-sup 10300  ax-addf 10301  ax-mulf 10302
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-reu 3094  df-rmo 3095  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-se 5270  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-of 7129  df-om 7298  df-1st 7399  df-2nd 7400  df-supp 7531  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-1o 7797  df-2o 7798  df-oadd 7801  df-er 7980  df-map 8095  df-pm 8096  df-ixp 8147  df-en 8194  df-dom 8195  df-sdom 8196  df-fin 8197  df-fsupp 8516  df-fi 8557  df-sup 8588  df-inf 8589  df-oi 8655  df-card 9049  df-cda 9276  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367  df-sub 10556  df-neg 10557  df-div 10975  df-nn 11311  df-2 11372  df-3 11373  df-4 11374  df-5 11375  df-6 11376  df-7 11377  df-8 11378  df-9 11379  df-n0 11577  df-z 11663  df-dec 11780  df-uz 11927  df-q 12030  df-rp 12071  df-xneg 12189  df-xadd 12190  df-xmul 12191  df-ioo 12424  df-ioc 12425  df-ico 12426  df-icc 12427  df-fz 12577  df-fzo 12717  df-fl 12844  df-mod 12920  df-seq 13052  df-exp 13111  df-fac 13310  df-bc 13339  df-hash 13367  df-shft 14144  df-cj 14176  df-re 14177  df-im 14178  df-sqrt 14312  df-abs 14313  df-limsup 14539  df-clim 14556  df-rlim 14557  df-sum 14754  df-ef 15130  df-sin 15132  df-cos 15133  df-tan 15134  df-pi 15135  df-struct 16182  df-ndx 16183  df-slot 16184  df-base 16186  df-sets 16187  df-ress 16188  df-plusg 16276  df-mulr 16277  df-starv 16278  df-sca 16279  df-vsca 16280  df-ip 16281  df-tset 16282  df-ple 16283  df-ds 16285  df-unif 16286  df-hom 16287  df-cco 16288  df-rest 16394  df-topn 16395  df-0g 16413  df-gsum 16414  df-topgen 16415  df-pt 16416  df-prds 16419  df-xrs 16473  df-qtop 16478  df-imas 16479  df-xps 16481  df-mre 16557  df-mrc 16558  df-acs 16560  df-mgm 17553  df-sgrp 17595  df-mnd 17606  df-submnd 17647  df-mulg 17853  df-cntz 18058  df-cmn 18506  df-psmet 20056  df-xmet 20057  df-met 20058  df-bl 20059  df-mopn 20060  df-fbas 20061  df-fg 20062  df-cnfld 20065  df-top 21023  df-topon 21040  df-topsp 21062  df-bases 21075  df-cld 21148  df-ntr 21149  df-cls 21150  df-nei 21227  df-lp 21265  df-perf 21266  df-cn 21356  df-cnp 21357  df-haus 21444  df-cmp 21515  df-tx 21690  df-hmeo 21883  df-fil 21974  df-fm 22066  df-flim 22067  df-flf 22068  df-xms 22449  df-ms 22450  df-tms 22451  df-cncf 23005  df-limc 23967  df-dv 23968  df-log 24640  df-cxp 24641  df-asin 24940
This theorem is referenced by:  areacirc  33984
  Copyright terms: Public domain W3C validator