Metamath Proof Explorer

Theorem areacirc

Description: The area of a circle of radius R is _pi x. R ^ 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)

Ref Expression
Hypothesis areacirc.1 ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) }
Assertion areacirc ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( area ‘ 𝑆 ) = ( π · ( 𝑅 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 areacirc.1 ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) }
2 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } ⊆ ( ℝ × ℝ )
3 1 2 eqsstri ⊢ 𝑆 ⊆ ( ℝ × ℝ )
4 3 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 𝑆 ⊆ ( ℝ × ℝ ) )
5 1 areacirclem5 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑆 “ { 𝑡 } ) = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
6 resqcl ⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ↑ 2 ) ∈ ℝ )
7 6 3ad2ant1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
8 resqcl ⊢ ( 𝑡 ∈ ℝ → ( 𝑡 ↑ 2 ) ∈ ℝ )
9 8 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
10 7 9 resubcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
11 10 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
12 absresq ⊢ ( 𝑡 ∈ ℝ → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
13 12 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
14 13 breq1d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ↔ ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
15 recn ⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
16 15 abscld ⊢ ( 𝑡 ∈ ℝ → ( abs ‘ 𝑡 ) ∈ ℝ )
17 16 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ 𝑡 ) ∈ ℝ )
18 simp1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 𝑅 ∈ ℝ )
19 15 absge0d ⊢ ( 𝑡 ∈ ℝ → 0 ≤ ( abs ‘ 𝑡 ) )
20 19 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ 𝑡 ) )
21 simp2 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 0 ≤ 𝑅 )
22 17 18 20 21 le2sqd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
23 7 9 subge0d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ↔ ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
24 14 22 23 3bitr4d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
25 24 biimpa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
26 11 25 resqrtcld ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
27 26 renegcld ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
28 iccmbl ⊢ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ ∧ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol )
29 27 26 28 syl2anc ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol )
30 mblvol ⊢ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
31 29 30 syl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
32 11 25 sqrtge0d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → 0 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
33 26 26 32 32 addge0d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
34 recn ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℂ )
35 34 sqcld ⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ↑ 2 ) ∈ ℂ )
36 35 3ad2ant1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
37 15 sqcld ⊢ ( 𝑡 ∈ ℝ → ( 𝑡 ↑ 2 ) ∈ ℂ )
38 37 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℂ )
39 36 38 subcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℂ )
40 39 sqrtcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℂ )
41 40 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℂ )
42 41 41 subnegd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
43 42 breq2d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
44 26 27 subge0d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
45 43 44 bitr3d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
46 33 45 mpbid ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
47 ovolicc ⊢ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ ∧ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ ∧ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) → ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
48 27 26 46 47 syl3anc ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
49 31 48 eqtrd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
50 26 27 resubcld ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ℝ )
51 49 50 eqeltrd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ ℝ )
52 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
53 ffn ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → vol Fn dom vol )
54 elpreima ⊢ ( vol Fn dom vol → ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ◡ vol “ ℝ ) ↔ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol ∧ ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ ℝ ) ) )
55 52 53 54 mp2b ⊢ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ◡ vol “ ℝ ) ↔ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol ∧ ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ ℝ ) )
56 29 51 55 sylanbrc ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ◡ vol “ ℝ ) )
57 0mbl ⊢ ∅ ∈ dom vol
58 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
59 57 58 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
60 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
61 59 60 eqtri ⊢ ( vol ‘ ∅ ) = 0
62 0re ⊢ 0 ∈ ℝ
63 61 62 eqeltri ⊢ ( vol ‘ ∅ ) ∈ ℝ
64 elpreima ⊢ ( vol Fn dom vol → ( ∅ ∈ ( ◡ vol “ ℝ ) ↔ ( ∅ ∈ dom vol ∧ ( vol ‘ ∅ ) ∈ ℝ ) ) )
65 52 53 64 mp2b ⊢ ( ∅ ∈ ( ◡ vol “ ℝ ) ↔ ( ∅ ∈ dom vol ∧ ( vol ‘ ∅ ) ∈ ℝ ) )
66 57 63 65 mpbir2an ⊢ ∅ ∈ ( ◡ vol “ ℝ )
67 66 a1i ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ∅ ∈ ( ◡ vol “ ℝ ) )
68 56 67 ifclda ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ∈ ( ◡ vol “ ℝ ) )
69 5 68 eqeltrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑆 “ { 𝑡 } ) ∈ ( ◡ vol “ ℝ ) )
70 69 3expa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑆 “ { 𝑡 } ) ∈ ( ◡ vol “ ℝ ) )
71 70 ralrimiva ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ∀ 𝑡 ∈ ℝ ( 𝑆 “ { 𝑡 } ) ∈ ( ◡ vol “ ℝ ) )
72 5 fveq2d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) )
73 72 3expa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ℝ ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) )
74 73 mpteq2dva ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) ) = ( 𝑡 ∈ ℝ ↦ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) ) )
75 renegcl ⊢ ( 𝑅 ∈ ℝ → - 𝑅 ∈ ℝ )
76 75 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → - 𝑅 ∈ ℝ )
77 simpl ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 𝑅 ∈ ℝ )
78 iccssre ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
79 76 77 78 syl2anc ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
80 rembl ⊢ ℝ ∈ dom vol
81 80 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ℝ ∈ dom vol )
82 fvexd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) ∈ V )
83 eldif ⊢ ( 𝑡 ∈ ( ℝ ∖ ( - 𝑅 [,] 𝑅 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) )
84 3anass ⊢ ( ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
85 84 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) ) )
86 75 3ad2ant1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → - 𝑅 ∈ ℝ )
87 elicc2 ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
88 86 18 87 syl2anc ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
89 simp3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
90 89 18 absled ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
91 89 biantrurd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) ) )
92 90 91 bitrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) ) )
93 85 88 92 3bitr4rd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) )
94 93 biimpd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 → 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) )
95 94 con3d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ¬ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) → ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
96 95 3expia ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ → ( ¬ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) → ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ) )
97 96 impd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( 𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
98 83 97 syl5bi ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( ℝ ∖ ( - 𝑅 [,] 𝑅 ) ) → ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
99 98 imp ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( ℝ ∖ ( - 𝑅 [,] 𝑅 ) ) ) → ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 )
100 iffalse ⊢ ( ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) = ∅ )
101 100 fveq2d ⊢ ( ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( vol ‘ ∅ ) )
102 101 61 eqtrdi ⊢ ( ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 )
103 99 102 syl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( ℝ ∖ ( - 𝑅 [,] 𝑅 ) ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 )
104 76 77 87 syl2anc ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
105 90 biimprd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
106 105 expd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( - 𝑅 ≤ 𝑡 → ( 𝑡 ≤ 𝑅 → ( abs ‘ 𝑡 ) ≤ 𝑅 ) ) )
107 106 3expia ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ → ( - 𝑅 ≤ 𝑡 → ( 𝑡 ≤ 𝑅 → ( abs ‘ 𝑡 ) ≤ 𝑅 ) ) ) )
108 107 3impd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
109 104 108 sylbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) → ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
110 109 3impia ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( abs ‘ 𝑡 ) ≤ 𝑅 )
111 iftrue ⊢ ( ( abs ‘ 𝑡 ) ≤ 𝑅 → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) = ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
112 111 fveq2d ⊢ ( ( abs ‘ 𝑡 ) ≤ 𝑅 → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
113 110 112 syl ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
114 6 3ad2ant1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
115 75 78 mpancom ⊢ ( 𝑅 ∈ ℝ → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
116 115 sselda ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑡 ∈ ℝ )
117 116 3adant2 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑡 ∈ ℝ )
118 117 resqcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
119 114 118 resubcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
120 75 87 mpancom ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
121 120 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
122 22 90 14 3bitr3rd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ↔ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
123 23 122 bitrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ↔ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
124 123 biimprd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
125 124 expd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( - 𝑅 ≤ 𝑡 → ( 𝑡 ≤ 𝑅 → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
126 125 3expia ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ → ( - 𝑅 ≤ 𝑡 → ( 𝑡 ≤ 𝑅 → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
127 126 3impd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
128 121 127 sylbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
129 128 3impia ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
130 119 129 resqrtcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
131 130 renegcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
132 131 130 28 syl2anc ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol )
133 132 30 syl ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
134 119 recnd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℂ )
135 134 sqrtcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℂ )
136 135 135 subnegd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
137 119 129 sqrtge0d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 0 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
138 130 130 137 137 addge0d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
139 136 breq2d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
140 130 131 subge0d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
141 139 140 bitr3d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
142 138 141 mpbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
143 131 130 142 47 syl3anc ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
144 135 2timesd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
145 136 143 144 3eqtr4d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
146 113 133 145 3eqtrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
147 146 3expa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
148 147 mpteq2dva ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) ) = ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
149 areacirclem3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )
150 148 149 eqeltrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) ) ∈ 𝐿1 )
151 79 81 82 103 150 iblss2 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ ↦ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) ) ∈ 𝐿1 )
152 74 151 eqeltrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) ) ∈ 𝐿1 )
153 dmarea ⊢ ( 𝑆 ∈ dom area ↔ ( 𝑆 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑡 ∈ ℝ ( 𝑆 “ { 𝑡 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑡 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) ) ∈ 𝐿1 ) )
154 4 71 152 153 syl3anbrc ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 𝑆 ∈ dom area )
155 areaval ⊢ ( 𝑆 ∈ dom area → ( area ‘ 𝑆 ) = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) d 𝑡 )
156 154 155 syl ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( area ‘ 𝑆 ) = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) d 𝑡 )
157 elioore ⊢ ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) → 𝑡 ∈ ℝ )
158 5 3expa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑆 “ { 𝑡 } ) = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
159 157 158 sylan2 ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( 𝑆 “ { 𝑡 } ) = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
160 159 fveq2d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) )
161 160 itgeq2dv ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) d 𝑡 = ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 )
162 ioossre ⊢ ( - 𝑅 (,) 𝑅 ) ⊆ ℝ
163 162 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( - 𝑅 (,) 𝑅 ) ⊆ ℝ )
164 eldif ⊢ ( 𝑡 ∈ ( ℝ ∖ ( - 𝑅 (,) 𝑅 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) )
165 75 rexrd ⊢ ( 𝑅 ∈ ℝ → - 𝑅 ∈ ℝ* )
166 rexr ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℝ* )
167 elioo2 ⊢ ( ( - 𝑅 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
168 165 166 167 syl2anc ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
169 168 3ad2ant1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
170 89 biantrurd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) ) )
171 89 18 absltd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) < 𝑅 ↔ ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
172 3anass ⊢ ( ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
173 172 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) ) )
174 170 171 173 3bitr4rd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ↔ ( abs ‘ 𝑡 ) < 𝑅 ) )
175 169 174 bitrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ ( abs ‘ 𝑡 ) < 𝑅 ) )
176 175 notbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ¬ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ ¬ ( abs ‘ 𝑡 ) < 𝑅 ) )
177 18 17 lenltd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ≤ ( abs ‘ 𝑡 ) ↔ ¬ ( abs ‘ 𝑡 ) < 𝑅 ) )
178 176 177 bitr4d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ¬ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ 𝑅 ≤ ( abs ‘ 𝑡 ) ) )
179 5 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( 𝑆 “ { 𝑡 } ) = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
180 179 fveq2d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) )
181 17 anim1i ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( ( abs ‘ 𝑡 ) ∈ ℝ ∧ ( abs ‘ 𝑡 ) = 𝑅 ) )
182 eqle ⊢ ( ( ( abs ‘ 𝑡 ) ∈ ℝ ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( abs ‘ 𝑡 ) ≤ 𝑅 )
183 181 182 112 3syl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
184 oveq1 ⊢ ( ( abs ‘ 𝑡 ) = 𝑅 → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑅 ↑ 2 ) )
185 184 adantl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑅 ↑ 2 ) )
186 13 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
187 185 186 eqtr3d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) )
188 fvoveq1 ⊢ ( ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
189 188 negeqd ⊢ ( ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = - ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
190 189 188 oveq12d ⊢ ( ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( - ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
191 8 recnd ⊢ ( 𝑡 ∈ ℝ → ( 𝑡 ↑ 2 ) ∈ ℂ )
192 191 subidd ⊢ ( 𝑡 ∈ ℝ → ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) = 0 )
193 192 fveq2d ⊢ ( 𝑡 ∈ ℝ → ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = ( √ ‘ 0 ) )
194 193 negeqd ⊢ ( 𝑡 ∈ ℝ → - ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = - ( √ ‘ 0 ) )
195 sqrt0 ⊢ ( √ ‘ 0 ) = 0
196 195 negeqi ⊢ - ( √ ‘ 0 ) = - 0
197 neg0 ⊢ - 0 = 0
198 196 197 eqtri ⊢ - ( √ ‘ 0 ) = 0
199 194 198 eqtrdi ⊢ ( 𝑡 ∈ ℝ → - ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = 0 )
200 193 195 eqtrdi ⊢ ( 𝑡 ∈ ℝ → ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = 0 )
201 199 200 oveq12d ⊢ ( 𝑡 ∈ ℝ → ( - ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( 0 [,] 0 ) )
202 201 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( - ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑡 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( 0 [,] 0 ) )
203 190 202 sylan9eqr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( 0 [,] 0 ) )
204 203 fveq2d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( vol ‘ ( 0 [,] 0 ) ) )
205 iccmbl ⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 0 [,] 0 ) ∈ dom vol )
206 62 62 205 mp2an ⊢ ( 0 [,] 0 ) ∈ dom vol
207 mblvol ⊢ ( ( 0 [,] 0 ) ∈ dom vol → ( vol ‘ ( 0 [,] 0 ) ) = ( vol* ‘ ( 0 [,] 0 ) ) )
208 206 207 ax-mp ⊢ ( vol ‘ ( 0 [,] 0 ) ) = ( vol* ‘ ( 0 [,] 0 ) )
209 0xr ⊢ 0 ∈ ℝ*
210 iccid ⊢ ( 0 ∈ ℝ* → ( 0 [,] 0 ) = { 0 } )
211 210 fveq2d ⊢ ( 0 ∈ ℝ* → ( vol* ‘ ( 0 [,] 0 ) ) = ( vol* ‘ { 0 } ) )
212 209 211 ax-mp ⊢ ( vol* ‘ ( 0 [,] 0 ) ) = ( vol* ‘ { 0 } )
213 ovolsn ⊢ ( 0 ∈ ℝ → ( vol* ‘ { 0 } ) = 0 )
214 62 213 ax-mp ⊢ ( vol* ‘ { 0 } ) = 0
215 212 214 eqtri ⊢ ( vol* ‘ ( 0 [,] 0 ) ) = 0
216 208 215 eqtri ⊢ ( vol ‘ ( 0 [,] 0 ) ) = 0
217 204 216 eqtrdi ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑅 ↑ 2 ) = ( 𝑡 ↑ 2 ) ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = 0 )
218 187 217 syldan ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = 0 )
219 183 218 eqtrd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) = 𝑅 ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 )
220 219 ex ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) = 𝑅 → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 ) )
221 220 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( ( abs ‘ 𝑡 ) = 𝑅 → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 ) )
222 18 17 ltnled ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑡 ) ↔ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
223 222 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( 𝑅 < ( abs ‘ 𝑡 ) ↔ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
224 simpl1 ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → 𝑅 ∈ ℝ )
225 17 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( abs ‘ 𝑡 ) ∈ ℝ )
226 simpr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → 𝑅 ≤ ( abs ‘ 𝑡 ) )
227 224 225 226 leltned ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( 𝑅 < ( abs ‘ 𝑡 ) ↔ ( abs ‘ 𝑡 ) ≠ 𝑅 ) )
228 223 227 bitr3d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( abs ‘ 𝑡 ) ≠ 𝑅 ) )
229 228 102 syl6bir ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( ( abs ‘ 𝑡 ) ≠ 𝑅 → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 ) )
230 221 229 pm2.61dne ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = 0 )
231 180 230 eqtrd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 ≤ ( abs ‘ 𝑡 ) ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 )
232 231 ex ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ≤ ( abs ‘ 𝑡 ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 ) )
233 178 232 sylbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ¬ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 ) )
234 233 3expia ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ → ( ¬ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 ) ) )
235 234 impd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( 𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 ) )
236 164 235 syl5bi ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( ℝ ∖ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 ) )
237 236 imp ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( ℝ ∖ ( - 𝑅 (,) 𝑅 ) ) ) → ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) = 0 )
238 163 237 itgss ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) d 𝑡 = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) d 𝑡 )
239 negeq ⊢ ( 𝑅 = 0 → - 𝑅 = - 0 )
240 239 197 eqtrdi ⊢ ( 𝑅 = 0 → - 𝑅 = 0 )
241 id ⊢ ( 𝑅 = 0 → 𝑅 = 0 )
242 240 241 oveq12d ⊢ ( 𝑅 = 0 → ( - 𝑅 (,) 𝑅 ) = ( 0 (,) 0 ) )
243 iooid ⊢ ( 0 (,) 0 ) = ∅
244 242 243 eqtrdi ⊢ ( 𝑅 = 0 → ( - 𝑅 (,) 𝑅 ) = ∅ )
245 244 adantl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 = 0 ) → ( - 𝑅 (,) 𝑅 ) = ∅ )
246 itgeq1 ⊢ ( ( - 𝑅 (,) 𝑅 ) = ∅ → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ∫ ∅ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 )
247 245 246 syl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 = 0 ) → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ∫ ∅ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 )
248 itg0 ⊢ ∫ ∅ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = 0
249 sq0 ⊢ ( 0 ↑ 2 ) = 0
250 249 oveq2i ⊢ ( π · ( 0 ↑ 2 ) ) = ( π · 0 )
251 picn ⊢ π ∈ ℂ
252 251 mul01i ⊢ ( π · 0 ) = 0
253 250 252 eqtr2i ⊢ 0 = ( π · ( 0 ↑ 2 ) )
254 oveq1 ⊢ ( 𝑅 = 0 → ( 𝑅 ↑ 2 ) = ( 0 ↑ 2 ) )
255 254 oveq2d ⊢ ( 𝑅 = 0 → ( π · ( 𝑅 ↑ 2 ) ) = ( π · ( 0 ↑ 2 ) ) )
256 253 255 eqtr4id ⊢ ( 𝑅 = 0 → 0 = ( π · ( 𝑅 ↑ 2 ) ) )
257 256 adantl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 = 0 ) → 0 = ( π · ( 𝑅 ↑ 2 ) ) )
258 248 257 eqtrid ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 = 0 ) → ∫ ∅ ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ( π · ( 𝑅 ↑ 2 ) ) )
259 247 258 eqtrd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 = 0 ) → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ( π · ( 𝑅 ↑ 2 ) ) )
260 simp1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0 ) → 𝑅 ∈ ℝ )
261 0red ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 0 ∈ ℝ )
262 simpr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 0 ≤ 𝑅 )
263 261 77 262 leltned ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 0 < 𝑅 ↔ 𝑅 ≠ 0 ) )
264 263 biimp3ar ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0 ) → 0 < 𝑅 )
265 260 264 elrpd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0 ) → 𝑅 ∈ ℝ+ )
266 265 3expa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 ≠ 0 ) → 𝑅 ∈ ℝ+ )
267 157 16 syl ⊢ ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) → ( abs ‘ 𝑡 ) ∈ ℝ )
268 267 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( abs ‘ 𝑡 ) ∈ ℝ )
269 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
270 269 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 𝑅 ∈ ℝ )
271 269 renegcld ⊢ ( 𝑅 ∈ ℝ+ → - 𝑅 ∈ ℝ )
272 271 rexrd ⊢ ( 𝑅 ∈ ℝ+ → - 𝑅 ∈ ℝ* )
273 rpxr ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* )
274 272 273 167 syl2anc ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
275 simpr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
276 269 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → 𝑅 ∈ ℝ )
277 275 276 absltd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) < 𝑅 ↔ ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
278 277 biimprd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) → ( abs ‘ 𝑡 ) < 𝑅 ) )
279 278 exp4b ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑡 ∈ ℝ → ( - 𝑅 < 𝑡 → ( 𝑡 < 𝑅 → ( abs ‘ 𝑡 ) < 𝑅 ) ) ) )
280 279 3impd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) → ( abs ‘ 𝑡 ) < 𝑅 ) )
281 274 280 sylbid ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) → ( abs ‘ 𝑡 ) < 𝑅 ) )
282 281 imp ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( abs ‘ 𝑡 ) < 𝑅 )
283 268 270 282 ltled ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( abs ‘ 𝑡 ) ≤ 𝑅 )
284 283 112 syl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
285 269 resqcld ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ↑ 2 ) ∈ ℝ )
286 285 recnd ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ↑ 2 ) ∈ ℂ )
287 286 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
288 191 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℂ )
289 287 288 subcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℂ )
290 289 sqrtcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℂ )
291 290 290 subnegd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
292 157 291 sylan2 ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
293 285 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
294 8 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
295 293 294 resubcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
296 157 295 sylan2 ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
297 0red ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 0 ∈ ℝ )
298 16 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( abs ‘ 𝑡 ) ∈ ℝ )
299 19 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ 𝑡 ) )
300 rpge0 ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 )
301 300 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → 0 ≤ 𝑅 )
302 298 276 299 301 lt2sqd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) < 𝑅 ↔ ( ( abs ‘ 𝑡 ) ↑ 2 ) < ( 𝑅 ↑ 2 ) ) )
303 12 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
304 303 breq1d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( ( abs ‘ 𝑡 ) ↑ 2 ) < ( 𝑅 ↑ 2 ) ↔ ( 𝑡 ↑ 2 ) < ( 𝑅 ↑ 2 ) ) )
305 302 277 304 3bitr3rd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 ↑ 2 ) < ( 𝑅 ↑ 2 ) ↔ ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ) )
306 294 293 posdifd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 ↑ 2 ) < ( 𝑅 ↑ 2 ) ↔ 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
307 305 306 bitr3d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) ↔ 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
308 307 biimpd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) → 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
309 308 exp4b ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑡 ∈ ℝ → ( - 𝑅 < 𝑡 → ( 𝑡 < 𝑅 → 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
310 309 3impd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 < 𝑡 ∧ 𝑡 < 𝑅 ) → 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
311 274 310 sylbid ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) → 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
312 311 imp ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 0 < ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
313 297 296 312 ltled ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
314 296 313 resqrtcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
315 314 renegcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
316 315 314 28 syl2anc ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ dom vol )
317 316 30 syl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
318 296 313 sqrtge0d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 0 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
319 314 314 318 318 addge0d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
320 292 breq2d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
321 314 315 subge0d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
322 320 321 bitr3d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( 0 ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
323 319 322 mpbid ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
324 315 314 323 47 syl3anc ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol* ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
325 317 324 eqtrd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) − - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
326 ax-resscn ⊢ ℝ ⊆ ℂ
327 326 a1i ⊢ ( 𝑅 ∈ ℝ+ → ℝ ⊆ ℂ )
328 271 269 78 syl2anc ⊢ ( 𝑅 ∈ ℝ+ → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
329 rpcn ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℂ )
330 329 sqcld ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ↑ 2 ) ∈ ℂ )
331 330 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
332 328 sselda ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑢 ∈ ℝ )
333 332 recnd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑢 ∈ ℂ )
334 329 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑅 ∈ ℂ )
335 rpne0 ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ≠ 0 )
336 335 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑅 ≠ 0 )
337 333 334 336 divcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑢 / 𝑅 ) ∈ ℂ )
338 asincl ⊢ ( ( 𝑢 / 𝑅 ) ∈ ℂ → ( arcsin ‘ ( 𝑢 / 𝑅 ) ) ∈ ℂ )
339 337 338 syl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( arcsin ‘ ( 𝑢 / 𝑅 ) ) ∈ ℂ )
340 1cnd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → 1 ∈ ℂ )
341 337 sqcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑢 / 𝑅 ) ↑ 2 ) ∈ ℂ )
342 340 341 subcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ∈ ℂ )
343 342 sqrtcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ∈ ℂ )
344 337 343 mulcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ∈ ℂ )
345 339 344 addcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ∈ ℂ )
346 331 345 mulcld ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ∈ ℂ )
347 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
348 347 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
349 iccntr ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( - 𝑅 [,] 𝑅 ) ) = ( - 𝑅 (,) 𝑅 ) )
350 271 269 349 syl2anc ⊢ ( 𝑅 ∈ ℝ+ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( - 𝑅 [,] 𝑅 ) ) = ( - 𝑅 (,) 𝑅 ) )
351 327 328 346 348 347 350 dvmptntr ⊢ ( 𝑅 ∈ ℝ+ → ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) = ( ℝ D ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) )
352 areacirclem1 ⊢ ( 𝑅 ∈ ℝ+ → ( ℝ D ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) = ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) )
353 351 352 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) = ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) )
354 353 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) = ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) )
355 oveq1 ⊢ ( 𝑢 = 𝑡 → ( 𝑢 ↑ 2 ) = ( 𝑡 ↑ 2 ) )
356 355 oveq2d ⊢ ( 𝑢 = 𝑡 → ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
357 356 fveq2d ⊢ ( 𝑢 = 𝑡 → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) = ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
358 357 oveq2d ⊢ ( 𝑢 = 𝑡 → ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) = ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
359 358 adantl ⊢ ( ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) ∧ 𝑢 = 𝑡 ) → ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) = ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
360 simpr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) )
361 ovexd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ V )
362 354 359 360 361 fvmptd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ‘ 𝑡 ) = ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
363 157 290 sylan2 ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℂ )
364 363 2timesd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
365 362 364 eqtrd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ‘ 𝑡 ) = ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) + ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
366 292 325 365 3eqtr4rd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ‘ 𝑡 ) = ( vol ‘ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
367 284 366 eqtr4d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ) → ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) = ( ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ‘ 𝑡 ) )
368 367 itgeq2dv ⊢ ( 𝑅 ∈ ℝ+ → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ∫ ( - 𝑅 (,) 𝑅 ) ( ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ‘ 𝑡 ) d 𝑡 )
369 269 269 300 300 addge0d ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ ( 𝑅 + 𝑅 ) )
370 329 329 subnegd ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 − - 𝑅 ) = ( 𝑅 + 𝑅 ) )
371 370 breq2d ⊢ ( 𝑅 ∈ ℝ+ → ( 0 ≤ ( 𝑅 − - 𝑅 ) ↔ 0 ≤ ( 𝑅 + 𝑅 ) ) )
372 269 271 subge0d ⊢ ( 𝑅 ∈ ℝ+ → ( 0 ≤ ( 𝑅 − - 𝑅 ) ↔ - 𝑅 ≤ 𝑅 ) )
373 371 372 bitr3d ⊢ ( 𝑅 ∈ ℝ+ → ( 0 ≤ ( 𝑅 + 𝑅 ) ↔ - 𝑅 ≤ 𝑅 ) )
374 369 373 mpbid ⊢ ( 𝑅 ∈ ℝ+ → - 𝑅 ≤ 𝑅 )
375 2cn ⊢ 2 ∈ ℂ
376 162 326 sstri ⊢ ( - 𝑅 (,) 𝑅 ) ⊆ ℂ
377 ssid ⊢ ℂ ⊆ ℂ
378 375 376 377 3pm3.2i ⊢ ( 2 ∈ ℂ ∧ ( - 𝑅 (,) 𝑅 ) ⊆ ℂ ∧ ℂ ⊆ ℂ )
379 cncfmptc ⊢ ( ( 2 ∈ ℂ ∧ ( - 𝑅 (,) 𝑅 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ 2 ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) )
380 378 379 mp1i ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ 2 ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) )
381 ioossicc ⊢ ( - 𝑅 (,) 𝑅 ) ⊆ ( - 𝑅 [,] 𝑅 )
382 resmpt ⊢ ( ( - 𝑅 (,) 𝑅 ) ⊆ ( - 𝑅 [,] 𝑅 ) → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ↾ ( - 𝑅 (,) 𝑅 ) ) = ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) )
383 381 382 ax-mp ⊢ ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ↾ ( - 𝑅 (,) 𝑅 ) ) = ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) )
384 areacirclem2 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
385 269 300 384 syl2anc ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
386 rescncf ⊢ ( ( - 𝑅 (,) 𝑅 ) ⊆ ( - 𝑅 [,] 𝑅 ) → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ↾ ( - 𝑅 (,) 𝑅 ) ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) ) )
387 381 385 386 mpsyl ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ↾ ( - 𝑅 (,) 𝑅 ) ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) )
388 383 387 eqeltrrid ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) )
389 380 388 mulcncf ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) )
390 353 389 eqeltrd ⊢ ( 𝑅 ∈ ℝ+ → ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ∈ ( ( - 𝑅 (,) 𝑅 ) –cn→ ℂ ) )
391 381 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( - 𝑅 (,) 𝑅 ) ⊆ ( - 𝑅 [,] 𝑅 ) )
392 ioombl ⊢ ( - 𝑅 (,) 𝑅 ) ∈ dom vol
393 392 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( - 𝑅 (,) 𝑅 ) ∈ dom vol )
394 ovexd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ∈ V )
395 areacirclem3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )
396 391 393 394 395 iblss ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )
397 269 300 396 syl2anc ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )
398 353 397 eqeltrd ⊢ ( 𝑅 ∈ ℝ+ → ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ∈ 𝐿1 )
399 areacirclem4 ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
400 271 269 374 390 398 399 ftc2nc ⊢ ( 𝑅 ∈ ℝ+ → ∫ ( - 𝑅 (,) 𝑅 ) ( ( ℝ D ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ 𝑅 ) − ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ - 𝑅 ) ) )
401 eqidd ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) = ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) )
402 fvoveq1 ⊢ ( 𝑢 = 𝑅 → ( arcsin ‘ ( 𝑢 / 𝑅 ) ) = ( arcsin ‘ ( 𝑅 / 𝑅 ) ) )
403 oveq1 ⊢ ( 𝑢 = 𝑅 → ( 𝑢 / 𝑅 ) = ( 𝑅 / 𝑅 ) )
404 403 oveq1d ⊢ ( 𝑢 = 𝑅 → ( ( 𝑢 / 𝑅 ) ↑ 2 ) = ( ( 𝑅 / 𝑅 ) ↑ 2 ) )
405 404 oveq2d ⊢ ( 𝑢 = 𝑅 → ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) = ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) )
406 405 fveq2d ⊢ ( 𝑢 = 𝑅 → ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) = ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) )
407 403 406 oveq12d ⊢ ( 𝑢 = 𝑅 → ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) = ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) )
408 402 407 oveq12d ⊢ ( 𝑢 = 𝑅 → ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) = ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) )
409 408 oveq2d ⊢ ( 𝑢 = 𝑅 → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) = ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) )
410 409 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 = 𝑅 ) → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) = ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) )
411 ubicc2 ⊢ ( ( - 𝑅 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ - 𝑅 ≤ 𝑅 ) → 𝑅 ∈ ( - 𝑅 [,] 𝑅 ) )
412 272 273 374 411 syl3anc ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ( - 𝑅 [,] 𝑅 ) )
413 ovexd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ∈ V )
414 401 410 412 413 fvmptd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ 𝑅 ) = ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) )
415 329 335 dividd ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 / 𝑅 ) = 1 )
416 415 fveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( arcsin ‘ ( 𝑅 / 𝑅 ) ) = ( arcsin ‘ 1 ) )
417 asin1 ⊢ ( arcsin ‘ 1 ) = ( π / 2 )
418 416 417 eqtrdi ⊢ ( 𝑅 ∈ ℝ+ → ( arcsin ‘ ( 𝑅 / 𝑅 ) ) = ( π / 2 ) )
419 415 oveq1d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 / 𝑅 ) ↑ 2 ) = ( 1 ↑ 2 ) )
420 sq1 ⊢ ( 1 ↑ 2 ) = 1
421 419 420 eqtrdi ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 / 𝑅 ) ↑ 2 ) = 1 )
422 421 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) = ( 1 − 1 ) )
423 1cnd ⊢ ( 𝑅 ∈ ℝ+ → 1 ∈ ℂ )
424 423 subidd ⊢ ( 𝑅 ∈ ℝ+ → ( 1 − 1 ) = 0 )
425 422 424 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) = 0 )
426 425 fveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) = ( √ ‘ 0 ) )
427 426 195 eqtrdi ⊢ ( 𝑅 ∈ ℝ+ → ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) = 0 )
428 427 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) = ( ( 𝑅 / 𝑅 ) · 0 ) )
429 329 329 335 divcld ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 / 𝑅 ) ∈ ℂ )
430 429 mul01d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 / 𝑅 ) · 0 ) = 0 )
431 428 430 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) = 0 )
432 418 431 oveq12d ⊢ ( 𝑅 ∈ ℝ+ → ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) = ( ( π / 2 ) + 0 ) )
433 2ne0 ⊢ 2 ≠ 0
434 251 375 433 divcli ⊢ ( π / 2 ) ∈ ℂ
435 434 a1i ⊢ ( 𝑅 ∈ ℝ+ → ( π / 2 ) ∈ ℂ )
436 435 addid1d ⊢ ( 𝑅 ∈ ℝ+ → ( ( π / 2 ) + 0 ) = ( π / 2 ) )
437 432 436 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) = ( π / 2 ) )
438 437 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑅 / 𝑅 ) ) + ( ( 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) = ( ( 𝑅 ↑ 2 ) · ( π / 2 ) ) )
439 414 438 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ 𝑅 ) = ( ( 𝑅 ↑ 2 ) · ( π / 2 ) ) )
440 fvoveq1 ⊢ ( 𝑢 = - 𝑅 → ( arcsin ‘ ( 𝑢 / 𝑅 ) ) = ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) )
441 oveq1 ⊢ ( 𝑢 = - 𝑅 → ( 𝑢 / 𝑅 ) = ( - 𝑅 / 𝑅 ) )
442 441 oveq1d ⊢ ( 𝑢 = - 𝑅 → ( ( 𝑢 / 𝑅 ) ↑ 2 ) = ( ( - 𝑅 / 𝑅 ) ↑ 2 ) )
443 442 oveq2d ⊢ ( 𝑢 = - 𝑅 → ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) = ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) )
444 443 fveq2d ⊢ ( 𝑢 = - 𝑅 → ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) = ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) )
445 441 444 oveq12d ⊢ ( 𝑢 = - 𝑅 → ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) = ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) )
446 440 445 oveq12d ⊢ ( 𝑢 = - 𝑅 → ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) = ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) )
447 446 adantl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 = - 𝑅 ) → ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) = ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) )
448 447 oveq2d ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝑢 = - 𝑅 ) → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) = ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) )
449 lbicc2 ⊢ ( ( - 𝑅 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ - 𝑅 ≤ 𝑅 ) → - 𝑅 ∈ ( - 𝑅 [,] 𝑅 ) )
450 272 273 374 449 syl3anc ⊢ ( 𝑅 ∈ ℝ+ → - 𝑅 ∈ ( - 𝑅 [,] 𝑅 ) )
451 ovexd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ∈ V )
452 401 448 450 451 fvmptd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ - 𝑅 ) = ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) )
453 329 329 335 divnegd ⊢ ( 𝑅 ∈ ℝ+ → - ( 𝑅 / 𝑅 ) = ( - 𝑅 / 𝑅 ) )
454 415 negeqd ⊢ ( 𝑅 ∈ ℝ+ → - ( 𝑅 / 𝑅 ) = - 1 )
455 453 454 eqtr3d ⊢ ( 𝑅 ∈ ℝ+ → ( - 𝑅 / 𝑅 ) = - 1 )
456 455 fveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) = ( arcsin ‘ - 1 ) )
457 ax-1cn ⊢ 1 ∈ ℂ
458 asinneg ⊢ ( 1 ∈ ℂ → ( arcsin ‘ - 1 ) = - ( arcsin ‘ 1 ) )
459 457 458 ax-mp ⊢ ( arcsin ‘ - 1 ) = - ( arcsin ‘ 1 )
460 417 negeqi ⊢ - ( arcsin ‘ 1 ) = - ( π / 2 )
461 459 460 eqtri ⊢ ( arcsin ‘ - 1 ) = - ( π / 2 )
462 456 461 eqtrdi ⊢ ( 𝑅 ∈ ℝ+ → ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) = - ( π / 2 ) )
463 455 oveq1d ⊢ ( 𝑅 ∈ ℝ+ → ( ( - 𝑅 / 𝑅 ) ↑ 2 ) = ( - 1 ↑ 2 ) )
464 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
465 463 464 eqtrdi ⊢ ( 𝑅 ∈ ℝ+ → ( ( - 𝑅 / 𝑅 ) ↑ 2 ) = 1 )
466 465 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) = ( 1 − 1 ) )
467 466 424 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) = 0 )
468 467 fveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) = ( √ ‘ 0 ) )
469 468 195 eqtrdi ⊢ ( 𝑅 ∈ ℝ+ → ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) = 0 )
470 469 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) = ( ( - 𝑅 / 𝑅 ) · 0 ) )
471 271 recnd ⊢ ( 𝑅 ∈ ℝ+ → - 𝑅 ∈ ℂ )
472 471 329 335 divcld ⊢ ( 𝑅 ∈ ℝ+ → ( - 𝑅 / 𝑅 ) ∈ ℂ )
473 472 mul01d ⊢ ( 𝑅 ∈ ℝ+ → ( ( - 𝑅 / 𝑅 ) · 0 ) = 0 )
474 470 473 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) = 0 )
475 462 474 oveq12d ⊢ ( 𝑅 ∈ ℝ+ → ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) = ( - ( π / 2 ) + 0 ) )
476 434 negcli ⊢ - ( π / 2 ) ∈ ℂ
477 476 a1i ⊢ ( 𝑅 ∈ ℝ+ → - ( π / 2 ) ∈ ℂ )
478 477 addid1d ⊢ ( 𝑅 ∈ ℝ+ → ( - ( π / 2 ) + 0 ) = - ( π / 2 ) )
479 475 478 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) = - ( π / 2 ) )
480 479 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( - 𝑅 / 𝑅 ) ) + ( ( - 𝑅 / 𝑅 ) · ( √ ‘ ( 1 − ( ( - 𝑅 / 𝑅 ) ↑ 2 ) ) ) ) ) ) = ( ( 𝑅 ↑ 2 ) · - ( π / 2 ) ) )
481 452 480 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ - 𝑅 ) = ( ( 𝑅 ↑ 2 ) · - ( π / 2 ) ) )
482 439 481 oveq12d ⊢ ( 𝑅 ∈ ℝ+ → ( ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ 𝑅 ) − ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ - 𝑅 ) ) = ( ( ( 𝑅 ↑ 2 ) · ( π / 2 ) ) − ( ( 𝑅 ↑ 2 ) · - ( π / 2 ) ) ) )
483 434 434 subnegi ⊢ ( ( π / 2 ) − - ( π / 2 ) ) = ( ( π / 2 ) + ( π / 2 ) )
484 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
485 483 484 eqtri ⊢ ( ( π / 2 ) − - ( π / 2 ) ) = π
486 485 a1i ⊢ ( 𝑅 ∈ ℝ+ → ( ( π / 2 ) − - ( π / 2 ) ) = π )
487 486 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · ( ( π / 2 ) − - ( π / 2 ) ) ) = ( ( 𝑅 ↑ 2 ) · π ) )
488 330 435 477 subdid ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · ( ( π / 2 ) − - ( π / 2 ) ) ) = ( ( ( 𝑅 ↑ 2 ) · ( π / 2 ) ) − ( ( 𝑅 ↑ 2 ) · - ( π / 2 ) ) ) )
489 251 a1i ⊢ ( 𝑅 ∈ ℝ+ → π ∈ ℂ )
490 330 489 mulcomd ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝑅 ↑ 2 ) · π ) = ( π · ( 𝑅 ↑ 2 ) ) )
491 487 488 490 3eqtr3d ⊢ ( 𝑅 ∈ ℝ+ → ( ( ( 𝑅 ↑ 2 ) · ( π / 2 ) ) − ( ( 𝑅 ↑ 2 ) · - ( π / 2 ) ) ) = ( π · ( 𝑅 ↑ 2 ) ) )
492 482 491 eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ( ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ 𝑅 ) − ( ( 𝑢 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑢 / 𝑅 ) ) + ( ( 𝑢 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑢 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ‘ - 𝑅 ) ) = ( π · ( 𝑅 ↑ 2 ) ) )
493 368 400 492 3eqtrd ⊢ ( 𝑅 ∈ ℝ+ → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ( π · ( 𝑅 ↑ 2 ) ) )
494 266 493 syl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑅 ≠ 0 ) → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ( π · ( 𝑅 ↑ 2 ) ) )
495 259 494 pm2.61dane ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ∫ ( - 𝑅 (,) 𝑅 ) ( vol ‘ if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) ) d 𝑡 = ( π · ( 𝑅 ↑ 2 ) ) )
496 161 238 495 3eqtr3d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑡 } ) ) d 𝑡 = ( π · ( 𝑅 ↑ 2 ) ) )
497 156 496 eqtrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( area ‘ 𝑆 ) = ( π · ( 𝑅 ↑ 2 ) ) )