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 34465
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 5489 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ × ℝ)
31, 2eqsstri 3884 . . . . 5 𝑆 ⊆ (ℝ × ℝ)
43a1i 11 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ⊆ (ℝ × ℝ))
51areacirclem5 34464 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
6 resqcl 13303 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
763ad2ant1 1114 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
8 resqcl 13303 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
983ad2ant3 1116 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
107, 9resubcld 10867 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
1110adantr 473 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12 absresq 14521 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
13123ad2ant3 1116 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
1413breq1d 4935 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
15 recn 10423 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
1615abscld 14655 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
17163ad2ant3 1116 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
18 simp1 1117 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
1915absge0d 14663 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
20193ad2ant3 1116 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
21 simp2 1118 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ 𝑅)
2217, 18, 20, 21le2sqd 13433 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
237, 9subge0d 11029 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
2414, 22, 233bitr4d 303 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
2524biimpa 469 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
2611, 25resqrtcld 14636 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
2726renegcld 10866 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
28 iccmbl 23885 . . . . . . . . . 10 ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
2927, 26, 28syl2anc 576 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
30 mblvol 23849 . . . . . . . . . . . 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 14639 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
3326, 26, 32, 32addge0d 11015 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
34 recn 10423 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
3534sqcld 13321 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
36353ad2ant1 1114 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
3715sqcld 13321 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
38373ad2ant3 1116 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
3936, 38subcld 10796 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
4039sqrtcld 14656 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
4140adantr 473 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
4241, 41subnegd 10803 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
4342breq2d 4937 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
4426, 27subge0d 11029 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
4543, 44bitr3d 273 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
4633, 45mpbid 224 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
47 ovolicc 23842 . . . . . . . . . . . 12 ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
4827, 26, 46, 47syl3anc 1352 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
4931, 48eqtrd 2807 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
5026, 27resubcld 10867 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈ ℝ)
5149, 50eqeltrd 2859 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)
52 volf 23848 . . . . . . . . . 10 vol:dom vol⟶(0[,]+∞)
53 ffn 6341 . . . . . . . . . 10 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
54 elpreima 6651 . . . . . . . . . 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 575 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (vol “ ℝ))
57 0mbl 23858 . . . . . . . . . 10 ∅ ∈ dom vol
58 mblvol 23849 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
5957, 58ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
60 ovol0 23812 . . . . . . . . . . . 12 (vol*‘∅) = 0
6159, 60eqtri 2795 . . . . . . . . . . 11 (vol‘∅) = 0
62 0re 10439 . . . . . . . . . . 11 0 ∈ ℝ
6361, 62eqeltri 2855 . . . . . . . . . 10 (vol‘∅) ∈ ℝ
64 elpreima 6651 . . . . . . . . . . 11 (vol Fn dom vol → (∅ ∈ (vol “ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅) ∈ ℝ)))
6552, 53, 64mp2b 10 . . . . . . . . . 10 (∅ ∈ (vol “ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅) ∈ ℝ))
6657, 63, 65mpbir2an 699 . . . . . . . . 9 ∅ ∈ (vol “ ℝ)
6766a1i 11 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ∅ ∈ (vol “ ℝ))
6856, 67ifclda 4378 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈ (vol “ ℝ))
695, 68eqeltrd 2859 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (vol “ ℝ))
70693expa 1099 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (vol “ ℝ))
7170ralrimiva 3125 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (vol “ ℝ))
725fveq2d 6500 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
73723expa 1099 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
7473mpteq2dva 5018 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) = (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))))
75 renegcl 10748 . . . . . . . 8 (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
7675adantr 473 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → -𝑅 ∈ ℝ)
77 simpl 475 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑅 ∈ ℝ)
78 iccssre 12632 . . . . . . 7 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
7976, 77, 78syl2anc 576 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅[,]𝑅) ⊆ ℝ)
80 rembl 23859 . . . . . . 7 ℝ ∈ dom vol
8180a1i 11 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ℝ ∈ dom vol)
82 fvexd 6511 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈ V)
83 eldif 3832 . . . . . . . . 9 (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)))
84 3anass 1077 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅)))
8584a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅))))
86753ad2ant1 1114 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → -𝑅 ∈ ℝ)
87 elicc2 12615 . . . . . . . . . . . . . . 15 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
8886, 18, 87syl2anc 576 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
89 simp3 1119 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
9089, 18absled 14649 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅𝑡𝑡𝑅)))
9189biantrurd 525 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅))))
9290, 91bitrd 271 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (𝑡 ∈ ℝ ∧ (-𝑅𝑡𝑡𝑅))))
9385, 88, 923bitr4rd 304 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)))
9493biimpd 221 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)))
9594con3d 150 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅))
96953expia 1102 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅)))
9796impd 402 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
9883, 97syl5bi 234 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
9998imp 398 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → ¬ (abs‘𝑡) ≤ 𝑅)
100 iffalse 4353 . . . . . . . . 9 (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
101100fveq2d 6500 . . . . . . . 8 (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘∅))
102101, 61syl6eq 2823 . . . . . . 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 576 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
10590biimprd 240 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → (abs‘𝑡) ≤ 𝑅))
106105expd 408 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (-𝑅𝑡 → (𝑡𝑅 → (abs‘𝑡) ≤ 𝑅)))
1071063expia 1102 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → (abs‘𝑡) ≤ 𝑅))))
1081073impd 1329 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → (abs‘𝑡) ≤ 𝑅))
109104, 108sylbid 232 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → (abs‘𝑡) ≤ 𝑅))
1101093impia 1098 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (abs‘𝑡) ≤ 𝑅)
111 iftrue 4350 . . . . . . . . . . . 12 ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
112111fveq2d 6500 . . . . . . . . . . 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 1114 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
11575, 78mpancom 676 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
116115sselda 3851 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
1171163adant2 1112 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
118117resqcld 13424 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
119114, 118resubcld 10867 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12075, 87mpancom 676 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
121120adantr 473 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
12222, 90, 143bitr3rd 302 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡↑2) ≤ (𝑅↑2) ↔ (-𝑅𝑡𝑡𝑅)))
12323, 122bitrd 271 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅𝑡𝑡𝑅)))
124123biimprd 240 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
125124expd 408 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2)))))
1261253expia 1102 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
1271263impd 1329 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
128121, 127sylbid 232 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
1291283impia 1098 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
130119, 129resqrtcld 14636 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
131130renegcld 10866 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
132131, 130, 28syl2anc 576 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
133132, 30syl 17 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
134119recnd 10466 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
135134sqrtcld 14656 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
136135, 135subnegd 10803 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
137119, 129sqrtge0d 14639 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
138130, 130, 137, 137addge0d 11015 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
139136breq2d 4937 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
140130, 131subge0d 11029 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
141139, 140bitr3d 273 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
142138, 141mpbid 224 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
143131, 130, 142, 47syl3anc 1352 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
1441352timesd 11688 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
145136, 143, 1443eqtr4d 2817 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
146113, 133, 1453eqtrd 2811 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
1471463expa 1099 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
148147mpteq2dva 5018 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
149 areacirclem3 34462 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿1)
150148, 149eqeltrd 2859 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿1)
15179, 81, 82, 103, 150iblss2 24124 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿1)
15274, 151eqeltrd 2859 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿1)
153 dmarea 25252 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿1))
1544, 71, 152, 153syl3anbrc 1324 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ∈ dom area)
155 areaval 25259 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
156154, 155syl 17 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
157 elioore 12582 . . . . . 6 (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
15853expa 1099 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
159157, 158sylan2 584 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
160159fveq2d 6500 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
161160itgeq2dv 24100 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
162 ioossre 12612 . . . . 5 (-𝑅(,)𝑅) ⊆ ℝ
163162a1i 11 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ ℝ)
164 eldif 3832 . . . . . 6 (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)))
16575rexrd 10488 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ → -𝑅 ∈ ℝ*)
166 rexr 10484 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ → 𝑅 ∈ ℝ*)
167 elioo2 12593 . . . . . . . . . . . . . 14 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
168165, 166, 167syl2anc 576 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
1691683ad2ant1 1114 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
17089biantrurd 525 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡𝑡 < 𝑅))))
17189, 18absltd 14648 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
172 3anass 1077 . . . . . . . . . . . . . 14 ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡𝑡 < 𝑅)))
173172a1i 11 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡𝑡 < 𝑅))))
174170, 171, 1733bitr4rd 304 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) ↔ (abs‘𝑡) < 𝑅))
175169, 174bitrd 271 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (abs‘𝑡) < 𝑅))
176175notbid 310 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ ¬ (abs‘𝑡) < 𝑅))
17718, 17lenltd 10584 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) ↔ ¬ (abs‘𝑡) < 𝑅))
178176, 177bitr4d 274 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ 𝑅 ≤ (abs‘𝑡)))
1795adantr 473 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
180179fveq2d 6500 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
18117anim1i 606 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅))
182 eqle 10540 . . . . . . . . . . . . . . . 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 6981 . . . . . . . . . . . . . . . . . 18 ((abs‘𝑡) = 𝑅 → ((abs‘𝑡)↑2) = (𝑅↑2))
185184adantl 474 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑅↑2))
18613adantr 473 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑡↑2))
187185, 186eqtr3d 2809 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2))
188 fvoveq1 6997 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑡↑2) − (𝑡↑2))))
189188negeqd 10678 . . . . . . . . . . . . . . . . . . . 20 ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) = -(√‘((𝑡↑2) − (𝑡↑2))))
190189, 188oveq12d 6992 . . . . . . . . . . . . . . . . . . 19 ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))))
1918recnd 10466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
192191subidd 10784 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0)
193192fveq2d 6500 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = (√‘0))
194193negeqd 10678 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = -(√‘0))
195 sqrt0 14460 . . . . . . . . . . . . . . . . . . . . . . . 24 (√‘0) = 0
196195negeqi 10677 . . . . . . . . . . . . . . . . . . . . . . 23 -(√‘0) = -0
197 neg0 10731 . . . . . . . . . . . . . . . . . . . . . . 23 -0 = 0
198196, 197eqtri 2795 . . . . . . . . . . . . . . . . . . . . . 22 -(√‘0) = 0
199194, 198syl6eq 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = 0)
200193, 195syl6eq 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = 0)
201199, 200oveq12d 6992 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ℝ → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
2022013ad2ant3 1116 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
203190, 202sylan9eqr 2829 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (0[,]0))
204203fveq2d 6500 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol‘(0[,]0)))
205 iccmbl 23885 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom vol)
20662, 62, 205mp2an 680 . . . . . . . . . . . . . . . . . . 19 (0[,]0) ∈ dom vol
207 mblvol 23849 . . . . . . . . . . . . . . . . . . 19 ((0[,]0) ∈ dom vol → (vol‘(0[,]0)) = (vol*‘(0[,]0)))
208206, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 (vol‘(0[,]0)) = (vol*‘(0[,]0))
209 0xr 10485 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℝ*
210 iccid 12597 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℝ* → (0[,]0) = {0})
211210fveq2d 6500 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ* → (vol*‘(0[,]0)) = (vol*‘{0}))
212209, 211ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (vol*‘(0[,]0)) = (vol*‘{0})
213 ovolsn 23814 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ → (vol*‘{0}) = 0)
21462, 213ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (vol*‘{0}) = 0
215212, 214eqtri 2795 . . . . . . . . . . . . . . . . . 18 (vol*‘(0[,]0)) = 0
216208, 215eqtri 2795 . . . . . . . . . . . . . . . . 17 (vol‘(0[,]0)) = 0
217204, 216syl6eq 2823 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
218187, 217syldan 583 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
219183, 218eqtrd 2807 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
220219ex 405 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
221220adantr 473 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
22218, 17ltnled 10585 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
223222adantr 473 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
224 simpl1 1172 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ∈ ℝ)
22517adantr 473 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (abs‘𝑡) ∈ ℝ)
226 simpr 477 . . . . . . . . . . . . . . 15 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ≤ (abs‘𝑡))
227224, 225, 226leltned 10591 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ (abs‘𝑡) ≠ 𝑅))
228223, 227bitr3d 273 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (¬ (abs‘𝑡) ≤ 𝑅 ↔ (abs‘𝑡) ≠ 𝑅))
229228, 102syl6bir 246 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) ≠ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
230221, 229pm2.61dne 3047 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
231180, 230eqtrd 2807 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = 0)
232231ex 405 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) → (vol‘(𝑆 “ {𝑡})) = 0))
233178, 232sylbid 232 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0))
2342333expia 1102 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0)))
235234impd 402 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
236164, 235syl5bi 234 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
237236imp 398 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅))) → (vol‘(𝑆 “ {𝑡})) = 0)
238163, 237itgss 24130 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
239 negeq 10676 . . . . . . . . . 10 (𝑅 = 0 → -𝑅 = -0)
240239, 197syl6eq 2823 . . . . . . . . 9 (𝑅 = 0 → -𝑅 = 0)
241 id 22 . . . . . . . . 9 (𝑅 = 0 → 𝑅 = 0)
242240, 241oveq12d 6992 . . . . . . . 8 (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0))
243 iooid 12580 . . . . . . . 8 (0(,)0) = ∅
244242, 243syl6eq 2823 . . . . . . 7 (𝑅 = 0 → (-𝑅(,)𝑅) = ∅)
245244adantl 474 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅)
246 itgeq1 24091 . . . . . 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 24098 . . . . . 6 ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0
249 oveq1 6981 . . . . . . . . 9 (𝑅 = 0 → (𝑅↑2) = (0↑2))
250249oveq2d 6990 . . . . . . . 8 (𝑅 = 0 → (π · (𝑅↑2)) = (π · (0↑2)))
251 sq0 13368 . . . . . . . . . 10 (0↑2) = 0
252251oveq2i 6985 . . . . . . . . 9 (π · (0↑2)) = (π · 0)
253 picn 24763 . . . . . . . . . 10 π ∈ ℂ
254253mul01i 10628 . . . . . . . . 9 (π · 0) = 0
255252, 254eqtr2i 2796 . . . . . . . 8 0 = (π · (0↑2))
256250, 255syl6reqr 2826 . . . . . . 7 (𝑅 = 0 → 0 = (π · (𝑅↑2)))
257256adantl 474 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → 0 = (π · (𝑅↑2)))
258248, 257syl5eq 2819 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
259247, 258eqtrd 2807 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
260 simp1 1117 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑅 ≠ 0) → 𝑅 ∈ ℝ)
261 0red 10441 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ∈ ℝ)
262 simpr 477 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ 𝑅)
263261, 77, 262leltned 10591 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0 < 𝑅𝑅 ≠ 0))
264263biimp3ar 1450 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑅 ≠ 0) → 0 < 𝑅)
265260, 264elrpd 12243 . . . . . 6 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑅 ≠ 0) → 𝑅 ∈ ℝ+)
2662653expa 1099 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ+)
267157, 16syl 17 . . . . . . . . . . 11 (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) ∈ ℝ)
268267adantl 474 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ∈ ℝ)
269 rpre 12210 . . . . . . . . . . 11 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
270269adantr 473 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
271269renegcld 10866 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
272271rexrd 10488 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ*)
273 rpxr 12213 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
274272, 273, 167syl2anc 576 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅)))
275 simpr 477 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
276269adantr 473 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
277275, 276absltd 14648 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
278277biimprd 240 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
279278exp4b 423 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → (abs‘𝑡) < 𝑅))))
2802793impd 1329 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
281274, 280sylbid 232 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) < 𝑅))
282281imp 398 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) < 𝑅)
283268, 270, 282ltled 10586 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅)
284283, 112syl 17 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
285269resqcld 13424 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
286285recnd 10466 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
287286adantr 473 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
288191adantl 474 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
289287, 288subcld 10796 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
290289sqrtcld 14656 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
291290, 290subnegd 10803 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
292157, 291sylan2 584 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
293285adantr 473 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
2948adantl 474 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
295293, 294resubcld 10867 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
296157, 295sylan2 584 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
297 0red 10441 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
29816adantl 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
29919adantl 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
300 rpge0 12217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
301300adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
302298, 276, 299, 301lt2sqd 13432 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
30312adantl 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
304303breq1d 4935 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2)))
305302, 277, 3043bitr3rd 302 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ (-𝑅 < 𝑡𝑡 < 𝑅)))
306294, 293posdifd 11026 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
307305, 306bitr3d 273 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
308307biimpd 221 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅 < 𝑡𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
309308exp4b 423 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < ((𝑅↑2) − (𝑡↑2))))))
3103093impd 1329 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
311274, 310sylbid 232 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
312311imp 398 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 < ((𝑅↑2) − (𝑡↑2)))
313297, 296, 312ltled 10586 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
314296, 313resqrtcld 14636 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
315314renegcld 10866 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
316315, 314, 28syl2anc 576 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
317316, 30syl 17 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
318296, 313sqrtge0d 14639 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
319314, 314, 318, 318addge0d 11015 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
320292breq2d 4937 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
321314, 315subge0d 11029 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
322320, 321bitr3d 273 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
323319, 322mpbid 224 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
324315, 314, 323, 47syl3anc 1352 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
325317, 324eqtrd 2807 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
326 ax-resscn 10390 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
327326a1i 11 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ℝ ⊆ ℂ)
328271, 269, 78syl2anc 576 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℝ)
329 rpcn 12214 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
330329sqcld 13321 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
331330adantr 473 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
332328sselda 3851 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ)
333332recnd 10466 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ)
334329adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
335 rpne0 12220 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+𝑅 ≠ 0)
336335adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
337333, 334, 336divcld 11215 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ)
338 asincl 25167 . . . . . . . . . . . . . . . . 17 ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
339337, 338syl 17 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
340 1cnd 10432 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
341337sqcld 13321 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ)
342340, 341subcld 10796 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ)
343342sqrtcld 14656 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ)
344337, 343mulcld 10458 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈ ℂ)
345339, 344addcld 10457 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈ ℂ)
346331, 345mulcld 10458 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈ ℂ)
347 eqid 2771 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
348347tgioo2 23129 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
349 iccntr 23147 . . . . . . . . . . . . . . 15 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
350271, 269, 349syl2anc 576 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
351327, 328, 346, 348, 347, 350dvmptntr 24286 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))))
352 areacirclem1 34460 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
353351, 352eqtrd 2807 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
354353adantr 473 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
355 oveq1 6981 . . . . . . . . . . . . . . 15 (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2))
356355oveq2d 6990 . . . . . . . . . . . . . 14 (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2)))
357356fveq2d 6500 . . . . . . . . . . . . 13 (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
358357oveq2d 6990 . . . . . . . . . . . 12 (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
359358adantl 474 . . . . . . . . . . 11 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
360 simpr 477 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅))
361 ovexd 7008 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V)
362354, 359, 360, 361fvmptd 6599 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
363157, 290sylan2 584 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
3643632timesd 11688 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
365362, 364eqtrd 2807 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
366292, 325, 3653eqtr4rd 2818 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
367284, 366eqtr4d 2810 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡))
368367itgeq2dv 24100 . . . . . 6 (𝑅 ∈ ℝ+ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡)
369269, 269, 300, 300addge0d 11015 . . . . . . . 8 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅 + 𝑅))
370329, 329subnegd 10803 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑅 − -𝑅) = (𝑅 + 𝑅))
371370breq2d 4937 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (0 ≤ (𝑅 − -𝑅) ↔ 0 ≤ (𝑅 + 𝑅)))
372269, 271subge0d 11029 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (0 ≤ (𝑅 − -𝑅) ↔ -𝑅𝑅))
373371, 372bitr3d 273 . . . . . . . 8 (𝑅 ∈ ℝ+ → (0 ≤ (𝑅 + 𝑅) ↔ -𝑅𝑅))
374369, 373mpbid 224 . . . . . . 7 (𝑅 ∈ ℝ+ → -𝑅𝑅)
375 2cn 11513 . . . . . . . . . . 11 2 ∈ ℂ
376162, 326sstri 3860 . . . . . . . . . . 11 (-𝑅(,)𝑅) ⊆ ℂ
377 ssid 3872 . . . . . . . . . . 11 ℂ ⊆ ℂ
378375, 376, 3773pm3.2i 1320 . . . . . . . . . 10 (2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ)
379 cncfmptc 23237 . . . . . . . . . 10 ((2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
380378, 379mp1i 13 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
381 ioossicc 12636 . . . . . . . . . . 11 (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)
382 resmpt 5747 . . . . . . . . . . 11 ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))))
383381, 382ax-mp 5 . . . . . . . . . 10 ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))
384 areacirclem2 34461 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
385269, 300, 384syl2anc 576 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
386 rescncf 23223 . . . . . . . . . . 11 ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)))
387381, 385, 386mpsyl 68 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
388383, 387syl5eqelr 2864 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
389380, 388mulcncf 23765 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
390353, 389eqeltrd 2859 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
391381a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅))
392 ioombl 23884 . . . . . . . . . . 11 (-𝑅(,)𝑅) ∈ dom vol
393392a1i 11 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ∈ dom vol)
394 ovexd 7008 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V)
395 areacirclem3 34462 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿1)
396391, 393, 394, 395iblss 24123 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿1)
397269, 300, 396syl2anc 576 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿1)
398353, 397eqeltrd 2859 . . . . . . 7 (𝑅 ∈ ℝ+ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ 𝐿1)
399 areacirclem4 34463 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
400271, 269, 374, 390, 398, 399ftc2nc 34454 . . . . . 6 (𝑅 ∈ ℝ+ → ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)))
401 eqidd 2772 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))
402 fvoveq1 6997 . . . . . . . . . . . . 13 (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅)))
403 oveq1 6981 . . . . . . . . . . . . . 14 (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅))
404403oveq1d 6989 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2))
405404oveq2d 6990 . . . . . . . . . . . . . . 15 (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2)))
406405fveq2d 6500 . . . . . . . . . . . . . 14 (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((𝑅 / 𝑅)↑2))))
407403, 406oveq12d 6992 . . . . . . . . . . . . 13 (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))
408402, 407oveq12d 6992 . . . . . . . . . . . 12 (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))
409408oveq2d 6990 . . . . . . . . . . 11 (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
410409adantl 474 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
411 ubicc2 12667 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ* ∧ -𝑅𝑅) → 𝑅 ∈ (-𝑅[,]𝑅))
412272, 273, 374, 411syl3anc 1352 . . . . . . . . . 10 (𝑅 ∈ ℝ+𝑅 ∈ (-𝑅[,]𝑅))
413 ovexd 7008 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V)
414401, 410, 412, 413fvmptd 6599 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
415329, 335dividd 11213 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (𝑅 / 𝑅) = 1)
416415fveq2d 6500 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (arcsin‘(𝑅 / 𝑅)) = (arcsin‘1))
417 asin1 25188 . . . . . . . . . . . . 13 (arcsin‘1) = (π / 2)
418416, 417syl6eq 2823 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (arcsin‘(𝑅 / 𝑅)) = (π / 2))
419415oveq1d 6989 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅)↑2) = (1↑2))
420 sq1 13371 . . . . . . . . . . . . . . . . . . 19 (1↑2) = 1
421419, 420syl6eq 2823 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅)↑2) = 1)
422421oveq2d 6990 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → (1 − ((𝑅 / 𝑅)↑2)) = (1 − 1))
423 1cnd 10432 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 1 ∈ ℂ)
424423subidd 10784 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → (1 − 1) = 0)
425422, 424eqtrd 2807 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 − ((𝑅 / 𝑅)↑2)) = 0)
426425fveq2d 6500 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = (√‘0))
427426, 195syl6eq 2823 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0)
428427oveq2d 6990 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0))
429329, 329, 335divcld 11215 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (𝑅 / 𝑅) ∈ ℂ)
430429mul01d 10637 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅) · 0) = 0)
431428, 430eqtrd 2807 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = 0)
432418, 431oveq12d 6992 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) + 0))
433 2ne0 11549 . . . . . . . . . . . . . 14 2 ≠ 0
434253, 375, 433divcli 11181 . . . . . . . . . . . . 13 (π / 2) ∈ ℂ
435434a1i 11 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (π / 2) ∈ ℂ)
436435addid1d 10638 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((π / 2) + 0) = (π / 2))
437432, 436eqtrd 2807 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2))
438437oveq2d 6990 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π / 2)))
439414, 438eqtrd 2807 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π / 2)))
440 fvoveq1 6997 . . . . . . . . . . . . 13 (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅)))
441 oveq1 6981 . . . . . . . . . . . . . 14 (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅))
442441oveq1d 6989 . . . . . . . . . . . . . . . 16 (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2))
443442oveq2d 6990 . . . . . . . . . . . . . . 15 (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2)))
444443fveq2d 6500 . . . . . . . . . . . . . 14 (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((-𝑅 / 𝑅)↑2))))
445441, 444oveq12d 6992 . . . . . . . . . . . . 13 (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))
446440, 445oveq12d 6992 . . . . . . . . . . . 12 (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
447446adantl 474 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
448447oveq2d 6990 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
449 lbicc2 12666 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ*𝑅 ∈ ℝ* ∧ -𝑅𝑅) → -𝑅 ∈ (-𝑅[,]𝑅))
450272, 273, 374, 449syl3anc 1352 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → -𝑅 ∈ (-𝑅[,]𝑅))
451 ovexd 7008 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) ∈ V)
452401, 448, 450, 451fvmptd 6599 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
453329, 329, 335divnegd 11228 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → -(𝑅 / 𝑅) = (-𝑅 / 𝑅))
454415negeqd 10678 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → -(𝑅 / 𝑅) = -1)
455453, 454eqtr3d 2809 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (-𝑅 / 𝑅) = -1)
456455fveq2d 6500 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (arcsin‘(-𝑅 / 𝑅)) = (arcsin‘-1))
457 ax-1cn 10391 . . . . . . . . . . . . . . 15 1 ∈ ℂ
458 asinneg 25180 . . . . . . . . . . . . . . 15 (1 ∈ ℂ → (arcsin‘-1) = -(arcsin‘1))
459457, 458ax-mp 5 . . . . . . . . . . . . . 14 (arcsin‘-1) = -(arcsin‘1)
460417negeqi 10677 . . . . . . . . . . . . . 14 -(arcsin‘1) = -(π / 2)
461459, 460eqtri 2795 . . . . . . . . . . . . 13 (arcsin‘-1) = -(π / 2)
462456, 461syl6eq 2823 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (arcsin‘(-𝑅 / 𝑅)) = -(π / 2))
463455oveq1d 6989 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅)↑2) = (-1↑2))
464 neg1sqe1 13372 . . . . . . . . . . . . . . . . . . 19 (-1↑2) = 1
465463, 464syl6eq 2823 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅)↑2) = 1)
466465oveq2d 6990 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ ℝ+ → (1 − ((-𝑅 / 𝑅)↑2)) = (1 − 1))
467466, 424eqtrd 2807 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 − ((-𝑅 / 𝑅)↑2)) = 0)
468467fveq2d 6500 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = (√‘0))
469468, 195syl6eq 2823 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0)
470469oveq2d 6990 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0))
471271recnd 10466 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℂ)
472471, 329, 335divcld 11215 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (-𝑅 / 𝑅) ∈ ℂ)
473472mul01d 10637 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅) · 0) = 0)
474470, 473eqtrd 2807 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = 0)
475462, 474oveq12d 6992 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = (-(π / 2) + 0))
476434negcli 10753 . . . . . . . . . . . . 13 -(π / 2) ∈ ℂ
477476a1i 11 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → -(π / 2) ∈ ℂ)
478477addid1d 10638 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (-(π / 2) + 0) = -(π / 2))
479475, 478eqtrd 2807 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = -(π / 2))
480479oveq2d 6990 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π / 2)))
481452, 480eqtrd 2807 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π / 2)))
482439, 481oveq12d 6992 . . . . . . 7 (𝑅 ∈ ℝ+ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
483434, 434subnegi 10764 . . . . . . . . . . 11 ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
484 pidiv2halves 24771 . . . . . . . . . . 11 ((π / 2) + (π / 2)) = π
485483, 484eqtri 2795 . . . . . . . . . 10 ((π / 2) − -(π / 2)) = π
486485a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((π / 2) − -(π / 2)) = π)
487486oveq2d 6990 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = ((𝑅↑2) · π))
488330, 435, 477subdid 10895 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
489253a1i 11 . . . . . . . . 9 (𝑅 ∈ ℝ+ → π ∈ ℂ)
490330, 489mulcomd 10459 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((𝑅↑2) · π) = (π · (𝑅↑2)))
491487, 488, 4903eqtr3d 2815 . . . . . . 7 (𝑅 ∈ ℝ+ → (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))) = (π · (𝑅↑2)))
492482, 491eqtrd 2807 . . . . . 6 (𝑅 ∈ ℝ+ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (π · (𝑅↑2)))
493368, 400, 4923eqtrd 2811 . . . . 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 3048 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
496161, 238, 4953eqtr3d 2815 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡 = (π · (𝑅↑2)))
497156, 496eqtrd 2807 1 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  wne 2960  wral 3081  Vcvv 3408  cdif 3819  wss 3822  c0 4172  ifcif 4344  {csn 4435   class class class wbr 4925  {copab 4987  cmpt 5004   × cxp 5401  ccnv 5402  dom cdm 5403  ran crn 5404  cres 5405  cima 5406   Fn wfn 6180  wf 6181  cfv 6185  (class class class)co 6974  cc 10331  cr 10332  0cc0 10333  1c1 10334   + caddc 10336   · cmul 10338  +∞cpnf 10469  *cxr 10471   < clt 10472  cle 10473  cmin 10668  -cneg 10669   / cdiv 11096  2c2 11493  +crp 12202  (,)cioo 12552  [,]cicc 12555  cexp 13242  csqrt 14451  abscabs 14452  πcpi 15278  TopOpenctopn 16549  topGenctg 16565  fldccnfld 20262  intcnt 21344  cnccncf 23202  vol*covol 23781  volcvol 23782  𝐿1cibl 23936  citg 23937   D cdv 24179  arcsincasin 25156  areacarea 25250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-inf2 8896  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410  ax-pre-sup 10411  ax-addf 10412  ax-mulf 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-nel 3067  df-ral 3086  df-rex 3087  df-reu 3088  df-rmo 3089  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-symdif 4100  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-iin 4791  df-disj 4894  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-se 5363  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-isom 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-of 7225  df-ofr 7226  df-om 7395  df-1st 7499  df-2nd 7500  df-supp 7632  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-2o 7904  df-oadd 7907  df-omul 7908  df-er 8087  df-map 8206  df-pm 8207  df-ixp 8258  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-fsupp 8627  df-fi 8668  df-sup 8699  df-inf 8700  df-oi 8767  df-dju 9122  df-card 9160  df-acn 9163  df-cda 9386  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-div 11097  df-nn 11438  df-2 11501  df-3 11502  df-4 11503  df-5 11504  df-6 11505  df-7 11506  df-8 11507  df-9 11508  df-n0 11706  df-z 11792  df-dec 11910  df-uz 12057  df-q 12161  df-rp 12203  df-xneg 12322  df-xadd 12323  df-xmul 12324  df-ioo 12556  df-ioc 12557  df-ico 12558  df-icc 12559  df-fz 12707  df-fzo 12848  df-fl 12975  df-mod 13051  df-seq 13183  df-exp 13243  df-fac 13447  df-bc 13476  df-hash 13504  df-shft 14285  df-cj 14317  df-re 14318  df-im 14319  df-sqrt 14453  df-abs 14454  df-limsup 14687  df-clim 14704  df-rlim 14705  df-sum 14902  df-ef 15279  df-sin 15281  df-cos 15282  df-tan 15283  df-pi 15284  df-struct 16339  df-ndx 16340  df-slot 16341  df-base 16343  df-sets 16344  df-ress 16345  df-plusg 16432  df-mulr 16433  df-starv 16434  df-sca 16435  df-vsca 16436  df-ip 16437  df-tset 16438  df-ple 16439  df-ds 16441  df-unif 16442  df-hom 16443  df-cco 16444  df-rest 16550  df-topn 16551  df-0g 16569  df-gsum 16570  df-topgen 16571  df-pt 16572  df-prds 16575  df-xrs 16629  df-qtop 16634  df-imas 16635  df-xps 16637  df-mre 16727  df-mrc 16728  df-acs 16730  df-mgm 17722  df-sgrp 17764  df-mnd 17775  df-submnd 17816  df-mulg 18024  df-cntz 18230  df-cmn 18680  df-psmet 20254  df-xmet 20255  df-met 20256  df-bl 20257  df-mopn 20258  df-fbas 20259  df-fg 20260  df-cnfld 20263  df-top 21221  df-topon 21238  df-topsp 21260  df-bases 21273  df-cld 21346  df-ntr 21347  df-cls 21348  df-nei 21425  df-lp 21463  df-perf 21464  df-cn 21554  df-cnp 21555  df-haus 21642  df-cmp 21714  df-tx 21889  df-hmeo 22082  df-fil 22173  df-fm 22265  df-flim 22266  df-flf 22267  df-xms 22648  df-ms 22649  df-tms 22650  df-cncf 23204  df-ovol 23783  df-vol 23784  df-mbf 23938  df-itg1 23939  df-itg2 23940  df-ibl 23941  df-itg 23942  df-0p 23989  df-limc 24182  df-dv 24183  df-log 24856  df-cxp 24857  df-asin 25159  df-area 25251
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator