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

Theorem areacirc 37703
Description: The area of a circle of radius 𝑅 is π · 𝑅↑2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
Hypothesis
Ref Expression
areacirc.1 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}
Assertion
Ref Expression
areacirc ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))
Distinct variable group:   𝑥,𝑦,𝑅
Allowed substitution hints:   𝑆(𝑥,𝑦)

Proof of Theorem areacirc
Dummy variables 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 areacirc.1 . . . . . 6 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}
2 opabssxp 5794 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ × ℝ)
31, 2eqsstri 4044 . . . . 5 𝑆 ⊆ (ℝ × ℝ)
43a1i 11 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ⊆ (ℝ × ℝ))
51areacirclem5 37702 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
6 resqcl 14192 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
763ad2ant1 1133 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
8 resqcl 14192 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
983ad2ant3 1135 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
107, 9resubcld 11724 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
1110adantr 480 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12 absresq 15369 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
13123ad2ant3 1135 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
1413breq1d 5178 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
15 recn 11278 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
1615abscld 15503 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
17163ad2ant3 1135 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
18 simp1 1136 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
1915absge0d 15511 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
20193ad2ant3 1135 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
21 simp2 1137 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ 𝑅)
2217, 18, 20, 21le2sqd 14324 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
237, 9subge0d 11886 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
2414, 22, 233bitr4d 311 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
2524biimpa 476 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
2611, 25resqrtcld 15484 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
2726renegcld 11723 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
28 iccmbl 25641 . . . . . . . . . 10 ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
2927, 26, 28syl2anc 583 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
30 mblvol 25605 . . . . . . . . . . . 12 ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
3129, 30syl 17 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
3211, 25sqrtge0d 15487 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
3326, 26, 32, 32addge0d 11872 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
34 recn 11278 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
3534sqcld 14212 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
36353ad2ant1 1133 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
3715sqcld 14212 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
38373ad2ant3 1135 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
3936, 38subcld 11653 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
4039sqrtcld 15504 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
4140adantr 480 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
4241, 41subnegd 11660 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
4342breq2d 5180 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
4426, 27subge0d 11886 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
4543, 44bitr3d 281 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
4633, 45mpbid 232 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
47 ovolicc 25598 . . . . . . . . . . . 12 ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
4827, 26, 46, 47syl3anc 1371 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
4931, 48eqtrd 2780 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
5026, 27resubcld 11724 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈ ℝ)
5149, 50eqeltrd 2844 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)
52 volf 25604 . . . . . . . . . 10 vol:dom vol⟶(0[,]+∞)
53 ffn 6751 . . . . . . . . . 10 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
54 elpreima 7095 . . . . . . . . . 10 (vol Fn dom vol → ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (vol “ ℝ) ↔ ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol ∧ (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)))
5552, 53, 54mp2b 10 . . . . . . . . 9 ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (vol “ ℝ) ↔ ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol ∧ (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ))
5629, 51, 55sylanbrc 582 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (vol “ ℝ))
57 0mbl 25614 . . . . . . . . . 10 ∅ ∈ dom vol
58 mblvol 25605 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
5957, 58ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
60 ovol0 25568 . . . . . . . . . . . 12 (vol*‘∅) = 0
6159, 60eqtri 2768 . . . . . . . . . . 11 (vol‘∅) = 0
62 0re 11296 . . . . . . . . . . 11 0 ∈ ℝ
6361, 62eqeltri 2840 . . . . . . . . . 10 (vol‘∅) ∈ ℝ
64 elpreima 7095 . . . . . . . . . . 11 (vol Fn dom vol → (∅ ∈ (vol “ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅) ∈ ℝ)))
6552, 53, 64mp2b 10 . . . . . . . . . 10 (∅ ∈ (vol “ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅) ∈ ℝ))
6657, 63, 65mpbir2an 710 . . . . . . . . 9 ∅ ∈ (vol “ ℝ)
6766a1i 11 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ∅ ∈ (vol “ ℝ))
6856, 67ifclda 4584 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈ (vol “ ℝ))
695, 68eqeltrd 2844 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (vol “ ℝ))
70693expa 1118 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (vol “ ℝ))
7170ralrimiva 3152 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (vol “ ℝ))
725fveq2d 6928 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
73723expa 1118 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
7473mpteq2dva 5268 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) = (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))))
75 renegcl 11605 . . . . . . . 8 (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
7675adantr 480 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → -𝑅 ∈ ℝ)
77 simpl 482 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑅 ∈ ℝ)
78 iccssre 13501 . . . . . . 7 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
7976, 77, 78syl2anc 583 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅[,]𝑅) ⊆ ℝ)
80 rembl 25615 . . . . . . 7 ℝ ∈ dom vol
8180a1i 11 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ℝ ∈ dom vol)
82 fvexd 6939 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈ V)
83 eldif 3987 . . . . . . . . 9 (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)))
84 3anass 1095 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅)))
8584a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅))))
86753ad2ant1 1133 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → -𝑅 ∈ ℝ)
87 elicc2 13484 . . . . . . . . . . . . . . 15 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
8886, 18, 87syl2anc 583 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
89 simp3 1138 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
9089, 18absled 15497 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅𝑡𝑡𝑅)))
9189biantrurd 532 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅))))
9290, 91bitrd 279 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅))))
9385, 88, 923bitr4rd 312 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)))
9493biimpd 229 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)))
9594con3d 152 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅))
96953expia 1121 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅)))
9796impd 410 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
9883, 97biimtrid 242 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
9998imp 406 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → ¬ (abs‘𝑡) ≤ 𝑅)
100 iffalse 4558 . . . . . . . . 9 (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
101100fveq2d 6928 . . . . . . . 8 (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘∅))
102101, 61eqtrdi 2796 . . . . . . 7 (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
10399, 102syl 17 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
10476, 77, 87syl2anc 583 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
10590biimprd 248 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → (abs‘𝑡) ≤ 𝑅))
106105expd 415 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (-𝑅𝑡 → (𝑡𝑅 → (abs‘𝑡) ≤ 𝑅)))
1071063expia 1121 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → (abs‘𝑡) ≤ 𝑅))))
1081073impd 1348 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → (abs‘𝑡) ≤ 𝑅))
109104, 108sylbid 240 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → (abs‘𝑡) ≤ 𝑅))
1101093impia 1117 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (abs‘𝑡) ≤ 𝑅)
111 iftrue 4555 . . . . . . . . . . . 12 ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
112111fveq2d 6928 . . . . . . . . . . 11 ((abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
113110, 112syl 17 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
11463ad2ant1 1133 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
11575, 78mpancom 687 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
116115sselda 4009 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
1171163adant2 1131 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
118117resqcld 14193 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
119114, 118resubcld 11724 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12075, 87mpancom 687 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
121120adantr 480 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
12222, 90, 143bitr3rd 310 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡↑2) ≤ (𝑅↑2) ↔ (-𝑅𝑡𝑡𝑅)))
12323, 122bitrd 279 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅𝑡𝑡𝑅)))
124123biimprd 248 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
125124expd 415 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2)))))
1261253expia 1121 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
1271263impd 1348 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
128121, 127sylbid 240 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
1291283impia 1117 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
130119, 129resqrtcld 15484 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
131130renegcld 11723 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
132131, 130, 28syl2anc 583 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
133132, 30syl 17 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
134119recnd 11322 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
135134sqrtcld 15504 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
136135, 135subnegd 11660 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
137119, 129sqrtge0d 15487 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
138130, 130, 137, 137addge0d 11872 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
139136breq2d 5180 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
140130, 131subge0d 11886 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
141139, 140bitr3d 281 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
142138, 141mpbid 232 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
143131, 130, 142, 47syl3anc 1371 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
1441352timesd 12542 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
145136, 143, 1443eqtr4d 2790 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
146113, 133, 1453eqtrd 2784 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
1471463expa 1118 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
148147mpteq2dva 5268 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
149 areacirclem3 37700 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿1)
150148, 149eqeltrd 2844 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿1)
15179, 81, 82, 103, 150iblss2 25882 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿1)
15274, 151eqeltrd 2844 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿1)
153 dmarea 27039 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿1))
1544, 71, 152, 153syl3anbrc 1343 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ∈ dom area)
155 areaval 27046 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
156154, 155syl 17 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
157 elioore 13449 . . . . . 6 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
15853expa 1118 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
159157, 158sylan2 592 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
160159fveq2d 6928 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
161160itgeq2dv 25858 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
162 ioossre 13480 . . . . 5 (-𝑅(,)𝑅) ⊆ ℝ
163162a1i 11 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ ℝ)
164 eldif 3987 . . . . . 6 (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)))
16575rexrd 11344 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ → -𝑅 ∈ ℝ*)
166 rexr 11340 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ → 𝑅 ∈ ℝ*)
167 elioo2 13460 . . . . . . . . . . . . . 14 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
168165, 166, 167syl2anc 583 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
1691683ad2ant1 1133 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
17089biantrurd 532 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡𝑡 < 𝑅))))
17189, 18absltd 15496 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
172 3anass 1095 . . . . . . . . . . . . . 14 ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡𝑡 < 𝑅)))
173172a1i 11 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡𝑡 < 𝑅))))
174170, 171, 1733bitr4rd 312 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) ↔ (abs‘𝑡) < 𝑅))
175169, 174bitrd 279 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (abs‘𝑡) < 𝑅))
176175notbid 318 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ ¬ (abs‘𝑡) < 𝑅))
17718, 17lenltd 11440 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) ↔ ¬ (abs‘𝑡) < 𝑅))
178176, 177bitr4d 282 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ 𝑅 ≤ (abs‘𝑡)))
1795adantr 480 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
180179fveq2d 6928 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
18117anim1i 614 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅))
182 eqle 11396 . . . . . . . . . . . . . . . 16 (((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅) → (abs‘𝑡) ≤ 𝑅)
183181, 182, 1123syl 18 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
184 oveq1 7459 . . . . . . . . . . . . . . . . . 18 ((abs‘𝑡) = 𝑅 → ((abs‘𝑡)↑2) = (𝑅↑2))
185184adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑅↑2))
18613adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑡↑2))
187185, 186eqtr3d 2782 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2))
188 fvoveq1 7475 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑡↑2) − (𝑡↑2))))
189188negeqd 11535 . . . . . . . . . . . . . . . . . . . 20 ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) = -(√‘((𝑡↑2) − (𝑡↑2))))
190189, 188oveq12d 7470 . . . . . . . . . . . . . . . . . . 19 ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))))
1918recnd 11322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
192191subidd 11641 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0)
193192fveq2d 6928 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = (√‘0))
194193negeqd 11535 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = -(√‘0))
195 sqrt0 15308 . . . . . . . . . . . . . . . . . . . . . . . 24 (√‘0) = 0
196195negeqi 11534 . . . . . . . . . . . . . . . . . . . . . . 23 -(√‘0) = -0
197 neg0 11588 . . . . . . . . . . . . . . . . . . . . . . 23 -0 = 0
198196, 197eqtri 2768 . . . . . . . . . . . . . . . . . . . . . 22 -(√‘0) = 0
199194, 198eqtrdi 2796 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = 0)
200193, 195eqtrdi 2796 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = 0)
201199, 200oveq12d 7470 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ℝ → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
2022013ad2ant3 1135 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
203190, 202sylan9eqr 2802 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (0[,]0))
204203fveq2d 6928 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol‘(0[,]0)))
205 iccmbl 25641 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom vol)
20662, 62, 205mp2an 691 . . . . . . . . . . . . . . . . . . 19 (0[,]0) ∈ dom vol
207 mblvol 25605 . . . . . . . . . . . . . . . . . . 19 ((0[,]0) ∈ dom vol → (vol‘(0[,]0)) = (vol*‘(0[,]0)))
208206, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 (vol‘(0[,]0)) = (vol*‘(0[,]0))
209 0xr 11341 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℝ*
210 iccid 13464 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℝ* → (0[,]0) = {0})
211210fveq2d 6928 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ* → (vol*‘(0[,]0)) = (vol*‘{0}))
212209, 211ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (vol*‘(0[,]0)) = (vol*‘{0})
213 ovolsn 25570 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ → (vol*‘{0}) = 0)
21462, 213ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (vol*‘{0}) = 0
215212, 214eqtri 2768 . . . . . . . . . . . . . . . . . 18 (vol*‘(0[,]0)) = 0
216208, 215eqtri 2768 . . . . . . . . . . . . . . . . 17 (vol‘(0[,]0)) = 0
217204, 216eqtrdi 2796 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
218187, 217syldan 590 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
219183, 218eqtrd 2780 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
220219ex 412 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
221220adantr 480 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
22218, 17ltnled 11441 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
223222adantr 480 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
224 simpl1 1191 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ∈ ℝ)
22517adantr 480 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (abs‘𝑡) ∈ ℝ)
226 simpr 484 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ≤ (abs‘𝑡))
227224, 225, 226leltned 11447 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ (abs‘𝑡) ≠ 𝑅))
228223, 227bitr3d 281 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (¬ (abs‘𝑡) ≤ 𝑅 ↔ (abs‘𝑡) ≠ 𝑅))
229228, 102biimtrrdi 254 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) ≠ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
230221, 229pm2.61dne 3034 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
231180, 230eqtrd 2780 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = 0)
232231ex 412 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) → (vol‘(𝑆 “ {𝑡})) = 0))
233178, 232sylbid 240 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0))
2342333expia 1121 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0)))
235234impd 410 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
236164, 235biimtrid 242 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
237236imp 406 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅))) → (vol‘(𝑆 “ {𝑡})) = 0)
238163, 237itgss 25888 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
239 negeq 11533 . . . . . . . . . 10 (𝑅 = 0 → -𝑅 = -0)
240239, 197eqtrdi 2796 . . . . . . . . 9 (𝑅 = 0 → -𝑅 = 0)
241 id 22 . . . . . . . . 9 (𝑅 = 0 → 𝑅 = 0)
242240, 241oveq12d 7470 . . . . . . . 8 (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0))
243 iooid 13447 . . . . . . . 8 (0(,)0) = ∅
244242, 243eqtrdi 2796 . . . . . . 7 (𝑅 = 0 → (-𝑅(,)𝑅) = ∅)
245244adantl 481 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅)
246 itgeq1 25849 . . . . . 6 ((-𝑅(,)𝑅) = ∅ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
247245, 246syl 17 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
248 itg0 25856 . . . . . 6 ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0
249 sq0 14259 . . . . . . . . . 10 (0↑2) = 0
250249oveq2i 7463 . . . . . . . . 9 (π · (0↑2)) = (π · 0)
251 picn 26540 . . . . . . . . . 10 π ∈ ℂ
252251mul01i 11484 . . . . . . . . 9 (π · 0) = 0
253250, 252eqtr2i 2769 . . . . . . . 8 0 = (π · (0↑2))
254 oveq1 7459 . . . . . . . . 9 (𝑅 = 0 → (𝑅↑2) = (0↑2))
255254oveq2d 7468 . . . . . . . 8 (𝑅 = 0 → (π · (𝑅↑2)) = (π · (0↑2)))
256253, 255eqtr4id 2799 . . . . . . 7 (𝑅 = 0 → 0 = (π · (𝑅↑2)))
257256adantl 481 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → 0 = (π · (𝑅↑2)))
258248, 257eqtrid 2792 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
259247, 258eqtrd 2780 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
260 simp1 1136 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑅 ≠ 0) → 𝑅 ∈ ℝ)
261 0red 11297 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ∈ ℝ)
262 simpr 484 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ 𝑅)
263261, 77, 262leltned 11447 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0 < 𝑅𝑅 ≠ 0))
264263biimp3ar 1470 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑅 ≠ 0) → 0 < 𝑅)
265260, 264elrpd 13107 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑅 ≠ 0) → 𝑅 ∈ ℝ+)
2662653expa 1118 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ+)
267157, 16syl 17 . . . . . . . . . . 11 (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) ∈ ℝ)
268267adantl 481 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ∈ ℝ)
269 rpre 13076 . . . . . . . . . . 11 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
270269adantr 480 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
271269renegcld 11723 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
272271rexrd 11344 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ*)
273 rpxr 13077 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
274272, 273, 167syl2anc 583 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
275 simpr 484 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
276269adantr 480 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
277275, 276absltd 15496 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
278277biimprd 248 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
279278exp4b 430 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → (abs‘𝑡) < 𝑅))))
2802793impd 1348 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
281274, 280sylbid 240 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) < 𝑅))
282281imp 406 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) < 𝑅)
283268, 270, 282ltled 11442 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅)
284283, 112syl 17 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
285269resqcld 14193 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
286285recnd 11322 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
287286adantr 480 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
288191adantl 481 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
289287, 288subcld 11653 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
290289sqrtcld 15504 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
291290, 290subnegd 11660 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
292157, 291sylan2 592 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
293285adantr 480 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
2948adantl 481 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
295293, 294resubcld 11724 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
296157, 295sylan2 592 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
297 0red 11297 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
29816adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
29919adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
300 rpge0 13081 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
301300adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
302298, 276, 299, 301lt2sqd 14323 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
30312adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
304303breq1d 5178 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2)))
305302, 277, 3043bitr3rd 310 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
306294, 293posdifd 11883 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
307305, 306bitr3d 281 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
308307biimpd 229 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
309308exp4b 430 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < ((𝑅↑2) − (𝑡↑2))))))
3103093impd 1348 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
311274, 310sylbid 240 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
312311imp 406 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 < ((𝑅↑2) − (𝑡↑2)))
313297, 296, 312ltled 11442 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
314296, 313resqrtcld 15484 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
315314renegcld 11723 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
316315, 314, 28syl2anc 583 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
317316, 30syl 17 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
318296, 313sqrtge0d 15487 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
319314, 314, 318, 318addge0d 11872 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
320292breq2d 5180 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
321314, 315subge0d 11886 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
322320, 321bitr3d 281 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
323319, 322mpbid 232 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
324315, 314, 323, 47syl3anc 1371 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
325317, 324eqtrd 2780 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
326 ax-resscn 11245 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
327326a1i 11 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ℝ ⊆ ℂ)
328271, 269, 78syl2anc 583 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℝ)
329 rpcn 13078 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
330329sqcld 14212 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
331330adantr 480 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
332328sselda 4009 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ)
333332recnd 11322 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ)
334329adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
335 rpne0 13084 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+𝑅 ≠ 0)
336335adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
337333, 334, 336divcld 12076 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ)
338 asincl 26955 . . . . . . . . . . . . . . . . 17 ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
339337, 338syl 17 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
340 1cnd 11289 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
341337sqcld 14212 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ)
342340, 341subcld 11653 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ)
343342sqrtcld 15504 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ)
344337, 343mulcld 11314 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈ ℂ)
345339, 344addcld 11313 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈ ℂ)
346331, 345mulcld 11314 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈ ℂ)
347 eqid 2740 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
348347tgioo2 24865 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
349 iccntr 24883 . . . . . . . . . . . . . . 15 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
350271, 269, 349syl2anc 583 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
351327, 328, 346, 348, 347, 350dvmptntr 26050 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))))
352 areacirclem1 37698 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
353351, 352eqtrd 2780 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
354353adantr 480 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
355 oveq1 7459 . . . . . . . . . . . . . . 15 (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2))
356355oveq2d 7468 . . . . . . . . . . . . . 14 (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2)))
357356fveq2d 6928 . . . . . . . . . . . . 13 (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
358357oveq2d 7468 . . . . . . . . . . . 12 (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
359358adantl 481 . . . . . . . . . . 11 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
360 simpr 484 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅))
361 ovexd 7487 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V)
362354, 359, 360, 361fvmptd 7040 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
363157, 290sylan2 592 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
3643632timesd 12542 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
365362, 364eqtrd 2780 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
366292, 325, 3653eqtr4rd 2791 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
367284, 366eqtr4d 2783 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡))
368367itgeq2dv 25858 . . . . . 6 (𝑅 ∈ ℝ+ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡)
369269, 269, 300, 300addge0d 11872 . . . . . . . 8 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅 + 𝑅))
370329, 329subnegd 11660 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑅 − -𝑅) = (𝑅 + 𝑅))
371370breq2d 5180 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (0 ≤ (𝑅 − -𝑅) ↔ 0 ≤ (𝑅 + 𝑅)))
372269, 271subge0d 11886 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (0 ≤ (𝑅 − -𝑅) ↔ -𝑅𝑅))
373371, 372bitr3d 281 . . . . . . . 8 (𝑅 ∈ ℝ+ → (0 ≤ (𝑅 + 𝑅) ↔ -𝑅𝑅))
374369, 373mpbid 232 . . . . . . 7 (𝑅 ∈ ℝ+ → -𝑅𝑅)
375 2cn 12374 . . . . . . . . . . 11 2 ∈ ℂ
376162, 326sstri 4019 . . . . . . . . . . 11 (-𝑅(,)𝑅) ⊆ ℂ
377 ssid 4032 . . . . . . . . . . 11 ℂ ⊆ ℂ
378375, 376, 3773pm3.2i 1339 . . . . . . . . . 10 (2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ)
379 cncfmptc 24978 . . . . . . . . . 10 ((2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
380378, 379mp1i 13 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
381 ioossicc 13505 . . . . . . . . . . 11 (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)
382 resmpt 6070 . . . . . . . . . . 11 ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))))
383381, 382ax-mp 5 . . . . . . . . . 10 ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))
384 areacirclem2 37699 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
385269, 300, 384syl2anc 583 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
386 rescncf 24963 . . . . . . . . . . 11 ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)))
387381, 385, 386mpsyl 68 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
388383, 387eqeltrrid 2849 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
389380, 388mulcncf 25520 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
390353, 389eqeltrd 2844 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
391381a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅))
392 ioombl 25640 . . . . . . . . . . 11 (-𝑅(,)𝑅) ∈ dom vol
393392a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ∈ dom vol)
394 ovexd 7487 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V)
395 areacirclem3 37700 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿1)
396391, 393, 394, 395iblss 25881 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿1)
397269, 300, 396syl2anc 583 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿1)
398353, 397eqeltrd 2844 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ 𝐿1)
399 areacirclem4 37701 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
400271, 269, 374, 390, 398, 399ftc2nc 37692 . . . . . 6 (𝑅 ∈ ℝ+ → ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)))
401 eqidd 2741 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))
402 fvoveq1 7475 . . . . . . . . . . . . 13 (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅)))
403 oveq1 7459 . . . . . . . . . . . . . 14 (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅))
404403oveq1d 7467 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2))
405404oveq2d 7468 . . . . . . . . . . . . . . 15 (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2)))
406405fveq2d 6928 . . . . . . . . . . . . . 14 (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((𝑅 / 𝑅)↑2))))
407403, 406oveq12d 7470 . . . . . . . . . . . . 13 (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))
408402, 407oveq12d 7470 . . . . . . . . . . . 12 (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))
409408oveq2d 7468 . . . . . . . . . . 11 (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
410409adantl 481 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
411 ubicc2 13537 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ* ∧ -𝑅𝑅) → 𝑅 ∈ (-𝑅[,]𝑅))
412272, 273, 374, 411syl3anc 1371 . . . . . . . . . 10 (𝑅 ∈ ℝ+𝑅 ∈ (-𝑅[,]𝑅))
413 ovexd 7487 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V)
414401, 410, 412, 413fvmptd 7040 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
415329, 335dividd 12074 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (𝑅 / 𝑅) = 1)
416415fveq2d 6928 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (arcsin‘(𝑅 / 𝑅)) = (arcsin‘1))
417 asin1 26976 . . . . . . . . . . . . 13 (arcsin‘1) = (π / 2)
418416, 417eqtrdi 2796 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (arcsin‘(𝑅 / 𝑅)) = (π / 2))
419415oveq1d 7467 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅)↑2) = (1↑2))
420 sq1 14262 . . . . . . . . . . . . . . . . . . 19 (1↑2) = 1
421419, 420eqtrdi 2796 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅)↑2) = 1)
422421oveq2d 7468 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → (1 − ((𝑅 / 𝑅)↑2)) = (1 − 1))
423 1cnd 11289 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 1 ∈ ℂ)
424423subidd 11641 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → (1 − 1) = 0)
425422, 424eqtrd 2780 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 − ((𝑅 / 𝑅)↑2)) = 0)
426425fveq2d 6928 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = (√‘0))
427426, 195eqtrdi 2796 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0)
428427oveq2d 7468 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0))
429329, 329, 335divcld 12076 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (𝑅 / 𝑅) ∈ ℂ)
430429mul01d 11493 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅) · 0) = 0)
431428, 430eqtrd 2780 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = 0)
432418, 431oveq12d 7470 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) + 0))
433 2ne0 12403 . . . . . . . . . . . . . 14 2 ≠ 0
434251, 375, 433divcli 12042 . . . . . . . . . . . . 13 (π / 2) ∈ ℂ
435434a1i 11 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (π / 2) ∈ ℂ)
436435addridd 11494 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((π / 2) + 0) = (π / 2))
437432, 436eqtrd 2780 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2))
438437oveq2d 7468 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π / 2)))
439414, 438eqtrd 2780 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π / 2)))
440 fvoveq1 7475 . . . . . . . . . . . . 13 (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅)))
441 oveq1 7459 . . . . . . . . . . . . . 14 (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅))
442441oveq1d 7467 . . . . . . . . . . . . . . . 16 (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2))
443442oveq2d 7468 . . . . . . . . . . . . . . 15 (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2)))
444443fveq2d 6928 . . . . . . . . . . . . . 14 (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((-𝑅 / 𝑅)↑2))))
445441, 444oveq12d 7470 . . . . . . . . . . . . 13 (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))
446440, 445oveq12d 7470 . . . . . . . . . . . 12 (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
447446adantl 481 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
448447oveq2d 7468 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
449 lbicc2 13536 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ* ∧ -𝑅𝑅) → -𝑅 ∈ (-𝑅[,]𝑅))
450272, 273, 374, 449syl3anc 1371 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → -𝑅 ∈ (-𝑅[,]𝑅))
451 ovexd 7487 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) ∈ V)
452401, 448, 450, 451fvmptd 7040 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
453329, 329, 335divnegd 12089 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → -(𝑅 / 𝑅) = (-𝑅 / 𝑅))
454415negeqd 11535 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → -(𝑅 / 𝑅) = -1)
455453, 454eqtr3d 2782 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (-𝑅 / 𝑅) = -1)
456455fveq2d 6928 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (arcsin‘(-𝑅 / 𝑅)) = (arcsin‘-1))
457 ax-1cn 11246 . . . . . . . . . . . . . . 15 1 ∈ ℂ
458 asinneg 26968 . . . . . . . . . . . . . . 15 (1 ∈ ℂ → (arcsin‘-1) = -(arcsin‘1))
459457, 458ax-mp 5 . . . . . . . . . . . . . 14 (arcsin‘-1) = -(arcsin‘1)
460417negeqi 11534 . . . . . . . . . . . . . 14 -(arcsin‘1) = -(π / 2)
461459, 460eqtri 2768 . . . . . . . . . . . . 13 (arcsin‘-1) = -(π / 2)
462456, 461eqtrdi 2796 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (arcsin‘(-𝑅 / 𝑅)) = -(π / 2))
463455oveq1d 7467 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅)↑2) = (-1↑2))
464 neg1sqe1 14263 . . . . . . . . . . . . . . . . . . 19 (-1↑2) = 1
465463, 464eqtrdi 2796 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅)↑2) = 1)
466465oveq2d 7468 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → (1 − ((-𝑅 / 𝑅)↑2)) = (1 − 1))
467466, 424eqtrd 2780 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 − ((-𝑅 / 𝑅)↑2)) = 0)
468467fveq2d 6928 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = (√‘0))
469468, 195eqtrdi 2796 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0)
470469oveq2d 7468 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0))
471271recnd 11322 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℂ)
472471, 329, 335divcld 12076 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (-𝑅 / 𝑅) ∈ ℂ)
473472mul01d 11493 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅) · 0) = 0)
474470, 473eqtrd 2780 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = 0)
475462, 474oveq12d 7470 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = (-(π / 2) + 0))
476434negcli 11610 . . . . . . . . . . . . 13 -(π / 2) ∈ ℂ
477476a1i 11 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → -(π / 2) ∈ ℂ)
478477addridd 11494 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (-(π / 2) + 0) = -(π / 2))
479475, 478eqtrd 2780 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = -(π / 2))
480479oveq2d 7468 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π / 2)))
481452, 480eqtrd 2780 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π / 2)))
482439, 481oveq12d 7470 . . . . . . 7 (𝑅 ∈ ℝ+ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
483434, 434subnegi 11621 . . . . . . . . . . 11 ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
484 pidiv2halves 26548 . . . . . . . . . . 11 ((π / 2) + (π / 2)) = π
485483, 484eqtri 2768 . . . . . . . . . 10 ((π / 2) − -(π / 2)) = π
486485a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((π / 2) − -(π / 2)) = π)
487486oveq2d 7468 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = ((𝑅↑2) · π))
488330, 435, 477subdid 11752 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
489251a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → π ∈ ℂ)
490330, 489mulcomd 11315 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) · π) = (π · (𝑅↑2)))
491487, 488, 4903eqtr3d 2788 . . . . . . 7 (𝑅 ∈ ℝ+ → (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))) = (π · (𝑅↑2)))
492482, 491eqtrd 2780 . . . . . 6 (𝑅 ∈ ℝ+ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (π · (𝑅↑2)))
493368, 400, 4923eqtrd 2784 . . . . 5 (𝑅 ∈ ℝ+ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
494266, 493syl 17 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
495259, 494pm2.61dane 3035 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
496161, 238, 4953eqtr3d 2788 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡 = (π · (𝑅↑2)))
497156, 496eqtrd 2780 1 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wral 3067  Vcvv 3489  cdif 3974  wss 3977  c0 4353  ifcif 4549  {csn 4649   class class class wbr 5168  {copab 5230  cmpt 5251   × cxp 5700  ccnv 5701  dom cdm 5702  ran crn 5703  cres 5704  cima 5705   Fn wfn 6572  wf 6573  cfv 6577  (class class class)co 7452  cc 11186  cr 11187  0cc0 11188  1c1 11189   + caddc 11191   · cmul 11193  +∞cpnf 11325  *cxr 11327   < clt 11328  cle 11329  cmin 11525  -cneg 11526   / cdiv 11953  2c2 12354  +crp 13067  (,)cioo 13419  [,]cicc 13422  cexp 14130  csqrt 15300  abscabs 15301  πcpi 16132  TopOpenctopn 17502  topGenctg 17518  fldccnfld 21408  intcnt 23067  cnccncf 24942  vol*covol 25537  volcvol 25538  𝐿1cibl 25692  citg 25693   D cdv 25939  arcsincasin 26944  areacarea 27037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5305  ax-sep 5319  ax-nul 5326  ax-pow 5385  ax-pr 5449  ax-un 7774  ax-inf2 9714  ax-cnex 11244  ax-resscn 11245  ax-1cn 11246  ax-icn 11247  ax-addcl 11248  ax-addrcl 11249  ax-mulcl 11250  ax-mulrcl 11251  ax-mulcom 11252  ax-addass 11253  ax-mulass 11254  ax-distr 11255  ax-i2m1 11256  ax-1ne0 11257  ax-1rid 11258  ax-rnegex 11259  ax-rrecex 11260  ax-cnre 11261  ax-pre-lttri 11262  ax-pre-lttrn 11263  ax-pre-ltadd 11264  ax-pre-mulgt0 11265  ax-pre-sup 11266  ax-addf 11267
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3445  df-v 3491  df-sbc 3806  df-csb 3923  df-dif 3980  df-un 3982  df-in 3984  df-ss 3994  df-pss 3997  df-symdif 4273  df-nul 4354  df-if 4550  df-pw 4625  df-sn 4650  df-pr 4652  df-tp 4654  df-op 4656  df-uni 4934  df-int 4973  df-iun 5019  df-iin 5020  df-disj 5136  df-br 5169  df-opab 5231  df-mpt 5252  df-tr 5286  df-id 5595  df-eprel 5601  df-po 5609  df-so 5610  df-fr 5654  df-se 5655  df-we 5656  df-xp 5708  df-rel 5709  df-cnv 5710  df-co 5711  df-dm 5712  df-rn 5713  df-res 5714  df-ima 5715  df-pred 6336  df-ord 6402  df-on 6403  df-lim 6404  df-suc 6405  df-iota 6529  df-fun 6579  df-fn 6580  df-f 6581  df-f1 6582  df-fo 6583  df-f1o 6584  df-fv 6585  df-isom 6586  df-riota 7408  df-ov 7455  df-oprab 7456  df-mpo 7457  df-of 7718  df-ofr 7719  df-om 7908  df-1st 8034  df-2nd 8035  df-supp 8206  df-frecs 8326  df-wrecs 8357  df-recs 8431  df-rdg 8470  df-1o 8526  df-2o 8527  df-oadd 8530  df-omul 8531  df-er 8767  df-map 8890  df-pm 8891  df-ixp 8960  df-en 9008  df-dom 9009  df-sdom 9010  df-fin 9011  df-fsupp 9436  df-fi 9484  df-sup 9515  df-inf 9516  df-oi 9583  df-dju 9974  df-card 10012  df-acn 10015  df-pnf 11330  df-mnf 11331  df-xr 11332  df-ltxr 11333  df-le 11334  df-sub 11527  df-neg 11528  df-div 11954  df-nn 12300  df-2 12362  df-3 12363  df-4 12364  df-5 12365  df-6 12366  df-7 12367  df-8 12368  df-9 12369  df-n0 12560  df-z 12647  df-dec 12767  df-uz 12912  df-q 13024  df-rp 13068  df-xneg 13187  df-xadd 13188  df-xmul 13189  df-ioo 13423  df-ioc 13424  df-ico 13425  df-icc 13426  df-fz 13580  df-fzo 13724  df-fl 13860  df-mod 13938  df-seq 14071  df-exp 14131  df-fac 14341  df-bc 14370  df-hash 14398  df-shft 15134  df-cj 15166  df-re 15167  df-im 15168  df-sqrt 15302  df-abs 15303  df-limsup 15535  df-clim 15552  df-rlim 15553  df-sum 15753  df-ef 16133  df-sin 16135  df-cos 16136  df-tan 16137  df-pi 16138  df-struct 17215  df-sets 17232  df-slot 17250  df-ndx 17262  df-base 17280  df-ress 17309  df-plusg 17345  df-mulr 17346  df-starv 17347  df-sca 17348  df-vsca 17349  df-ip 17350  df-tset 17351  df-ple 17352  df-ds 17354  df-unif 17355  df-hom 17356  df-cco 17357  df-rest 17503  df-topn 17504  df-0g 17522  df-gsum 17523  df-topgen 17524  df-pt 17525  df-prds 17528  df-xrs 17583  df-qtop 17588  df-imas 17589  df-xps 17591  df-mre 17665  df-mrc 17666  df-acs 17668  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-submnd 18840  df-mulg 19129  df-cntz 19378  df-cmn 19845  df-psmet 21400  df-xmet 21401  df-met 21402  df-bl 21403  df-mopn 21404  df-fbas 21405  df-fg 21406  df-cnfld 21409  df-top 22942  df-topon 22959  df-topsp 22981  df-bases 22995  df-cld 23069  df-ntr 23070  df-cls 23071  df-nei 23148  df-lp 23186  df-perf 23187  df-cn 23277  df-cnp 23278  df-haus 23365  df-cmp 23437  df-tx 23612  df-hmeo 23805  df-fil 23896  df-fm 23988  df-flim 23989  df-flf 23990  df-xms 24372  df-ms 24373  df-tms 24374  df-cncf 24944  df-ovol 25539  df-vol 25540  df-mbf 25694  df-itg1 25695  df-itg2 25696  df-ibl 25697  df-itg 25698  df-0p 25745  df-limc 25942  df-dv 25943  df-log 26637  df-cxp 26638  df-asin 26947  df-area 27038
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator