areacirc - Mathbox for Brendan Leahy

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

Theorem areacirc 37695

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.

Step	Hyp	Ref	Expression
1		areacirc.1	. . . . . 6 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}
2		opabssxp 5715	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ × ℝ)
3	1, 2	eqsstri 3984	. . . . 5 ⊢ 𝑆 ⊆ (ℝ × ℝ)
4	3	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ⊆ (ℝ × ℝ))
5	1	areacirclem5 37694	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
6		resqcl 14049	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
7	6	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
8		resqcl 14049	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
9	8	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
10	7, 9	resubcld 11566	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
11	10	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12		absresq 15227	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
13	12	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
14	13	breq1d 5105	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
15		recn 11118	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
16	15	abscld 15364	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
17	16	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
18		simp1 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
19	15	absge0d 15372	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
20	19	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
21		simp2 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
22	17, 18, 20, 21	le2sqd 14182	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
23	7, 9	subge0d 11728	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
24	14, 22, 23	3bitr4d 311	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
25	24	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
26	11, 25	resqrtcld 15343	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
27	26	renegcld 11565	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
28		iccmbl 25483	. . . . . . . . . 10 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
29	27, 26, 28	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
30		mblvol 25447	. . . . . . . . . . . 12 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
32	11, 25	sqrtge0d 15346	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
33	26, 26, 32, 32	addge0d 11714	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
34		recn 11118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
35	34	sqcld 14069	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
36	35	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
37	15	sqcld 14069	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
38	37	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
39	36, 38	subcld 11493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
40	39	sqrtcld 15365	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
41	40	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
42	41, 41	subnegd 11500	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
43	42	breq2d 5107	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
44	26, 27	subge0d 11728	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
45	43, 44	bitr3d 281	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
46	33, 45	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
47		ovolicc 25440	. . . . . . . . . . . 12 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
48	27, 26, 46, 47	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
49	31, 48	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
50	26, 27	resubcld 11566	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈ ℝ)
51	49, 50	eqeltrd 2828	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)
52		volf 25446	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
53		ffn 6656	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
54		elpreima 6996	. . . . . . . . . 10 ⊢ (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 10	. . . . . . . . 9 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (^◡vol “ ℝ) ↔ ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol ∧ (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ))
56	29, 51, 55	sylanbrc 583	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (^◡vol “ ℝ))
57		0mbl 25456	. . . . . . . . . 10 ⊢ ∅ ∈ dom vol
58		mblvol 25447	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
59	57, 58	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
60		ovol0 25410	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
61	59, 60	eqtri 2752	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
62		0re 11136	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
63	61, 62	eqeltri 2824	. . . . . . . . . 10 ⊢ (vol‘∅) ∈ ℝ
64		elpreima 6996	. . . . . . . . . . 11 ⊢ (vol Fn dom vol → (∅ ∈ (^◡vol “ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅) ∈ ℝ)))
65	52, 53, 64	mp2b 10	. . . . . . . . . 10 ⊢ (∅ ∈ (^◡vol “ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅) ∈ ℝ))
66	57, 63, 65	mpbir2an 711	. . . . . . . . 9 ⊢ ∅ ∈ (^◡vol “ ℝ)
67	66	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ∅ ∈ (^◡vol “ ℝ))
68	56, 67	ifclda 4514	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈ (^◡vol “ ℝ))
69	5, 68	eqeltrd 2828	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
70	69	3expa 1118	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
71	70	ralrimiva 3121	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
72	5	fveq2d 6830	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
73	72	3expa 1118	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
74	73	mpteq2dva 5188	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) = (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))))
75		renegcl 11445	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
76	75	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → -𝑅 ∈ ℝ)
77		simpl 482	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑅 ∈ ℝ)
78		iccssre 13350	. . . . . . 7 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
79	76, 77, 78	syl2anc 584	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅[,]𝑅) ⊆ ℝ)
80		rembl 25457	. . . . . . 7 ⊢ ℝ ∈ dom vol
81	80	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ℝ ∈ dom vol)
82		fvexd 6841	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈ V)
83		eldif 3915	. . . . . . . . 9 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)))
84		3anass 1094	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
85	84	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
86	75	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → -𝑅 ∈ ℝ)
87		elicc2 13332	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
88	86, 18, 87	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89		simp3 1138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
90	89, 18	absled 15358	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
91	89	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
92	90, 91	bitrd 279	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
93	85, 88, 92	3bitr4rd 312	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 𝑡 ∈ (-𝑅[,]𝑅)))
94	93	biimpd 229	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 → 𝑡 ∈ (-𝑅[,]𝑅)))
95	94	con3d 152	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅))
96	95	3expia 1121	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅)))
97	96	impd 410	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
98	83, 97	biimtrid 242	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
99	98	imp 406	. . . . . . 7 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → ¬ (abs‘𝑡) ≤ 𝑅)
100		iffalse 4487	. . . . . . . . 9 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
101	100	fveq2d 6830	. . . . . . . 8 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘∅))
102	101, 61	eqtrdi 2780	. . . . . . 7 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
103	99, 102	syl 17	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
104	76, 77, 87	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
105	90	biimprd 248	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅))
106	105	expd 415	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅)))
107	106	3expia 1121	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅))))
108	107	3impd 1349	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅))
109	104, 108	sylbid 240	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → (abs‘𝑡) ≤ 𝑅))
110	109	3impia 1117	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (abs‘𝑡) ≤ 𝑅)
111		iftrue 4484	. . . . . . . . . . . 12 ⊢ ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
112	111	fveq2d 6830	. . . . . . . . . . 11 ⊢ ((abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
113	110, 112	syl 17	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
114	6	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
115	75, 78	mpancom 688	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
116	115	sselda 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
117	116	3adant2 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
118	117	resqcld 14050	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
119	114, 118	resubcld 11566	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
120	75, 87	mpancom 688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
121	120	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
122	22, 90, 14	3bitr3rd 310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ (𝑅↑2) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
123	23, 122	bitrd 279	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
124	123	biimprd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
125	124	expd 415	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2)))))
126	125	3expia 1121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
127	126	3impd 1349	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
128	121, 127	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
129	128	3impia 1117	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
130	119, 129	resqrtcld 15343	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
131	130	renegcld 11565	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
132	131, 130, 28	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
133	132, 30	syl 17	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
134	119	recnd 11162	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
135	134	sqrtcld 15365	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
136	135, 135	subnegd 11500	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
137	119, 129	sqrtge0d 15346	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
138	130, 130, 137, 137	addge0d 11714	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
139	136	breq2d 5107	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
140	130, 131	subge0d 11728	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
141	139, 140	bitr3d 281	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
142	138, 141	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
143	131, 130, 142, 47	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
144	135	2timesd 12385	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
145	136, 143, 144	3eqtr4d 2774	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
146	113, 133, 145	3eqtrd 2768	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
147	146	3expa 1118	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
148	147	mpteq2dva 5188	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
149		areacirclem3 37692	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿¹)
150	148, 149	eqeltrd 2828	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
151	79, 81, 82, 103, 150	iblss2 25723	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
152	74, 151	eqeltrd 2828	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹)
153		dmarea 26883	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹))
154	4, 71, 152, 153	syl3anbrc 1344	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ∈ dom area)
155		areaval 26890	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
156	154, 155	syl 17	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
157		elioore 13296	. . . . . 6 ⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
158	5	3expa 1118	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
159	157, 158	sylan2 593	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
160	159	fveq2d 6830	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
161	160	itgeq2dv 25699	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
162		ioossre 13328	. . . . 5 ⊢ (-𝑅(,)𝑅) ⊆ ℝ
163	162	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ ℝ)
164		eldif 3915	. . . . . 6 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)))
165	75	rexrd 11184	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ^*)
166		rexr 11180	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℝ^*)
167		elioo2 13307	. . . . . . . . . . . . . 14 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
168	165, 166, 167	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
169	168	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
170	89	biantrurd 532	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
171	89, 18	absltd 15357	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
172		3anass 1094	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
173	172	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
174	170, 171, 173	3bitr4rd 312	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (abs‘𝑡) < 𝑅))
175	169, 174	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (abs‘𝑡) < 𝑅))
176	175	notbid 318	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ ¬ (abs‘𝑡) < 𝑅))
177	18, 17	lenltd 11280	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) ↔ ¬ (abs‘𝑡) < 𝑅))
178	176, 177	bitr4d 282	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ 𝑅 ≤ (abs‘𝑡)))
179	5	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
180	179	fveq2d 6830	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
181	17	anim1i 615	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅))
182		eqle 11236	. . . . . . . . . . . . . . . 16 ⊢ (((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅) → (abs‘𝑡) ≤ 𝑅)
183	181, 182, 112	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
184		oveq1 7360	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘𝑡) = 𝑅 → ((abs‘𝑡)↑2) = (𝑅↑2))
185	184	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑅↑2))
186	13	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑡↑2))
187	185, 186	eqtr3d 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2))
188		fvoveq1 7376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑡↑2) − (𝑡↑2))))
189	188	negeqd 11375	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) = -(√‘((𝑡↑2) − (𝑡↑2))))
190	189, 188	oveq12d 7371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))))
191	8	recnd 11162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
192	191	subidd 11481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0)
193	192	fveq2d 6830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = (√‘0))
194	193	negeqd 11375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = -(√‘0))
195		sqrt0 15166	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (√‘0) = 0
196	195	negeqi 11374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -(√‘0) = -0
197		neg0 11428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -0 = 0
198	196, 197	eqtri 2752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(√‘0) = 0
199	194, 198	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = 0)
200	193, 195	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = 0)
201	199, 200	oveq12d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
202	201	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
203	190, 202	sylan9eqr 2786	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (0[,]0))
204	203	fveq2d 6830	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol‘(0[,]0)))
205		iccmbl 25483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom vol)
206	62, 62, 205	mp2an 692	. . . . . . . . . . . . . . . . . . 19 ⊢ (0[,]0) ∈ dom vol
207		mblvol 25447	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0[,]0) ∈ dom vol → (vol‘(0[,]0)) = (vol*‘(0[,]0)))
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (vol‘(0[,]0)) = (vol*‘(0[,]0))
209		0xr 11181	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℝ^*
210		iccid 13311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℝ^* → (0[,]0) = {0})
211	210	fveq2d 6830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ^* → (vol‘(0[,]0)) = (vol‘{0}))
212	209, 211	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol‘(0[,]0)) = (vol‘{0})
213		ovolsn 25412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (vol*‘{0}) = 0)
214	62, 213	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol*‘{0}) = 0
215	212, 214	eqtri 2752	. . . . . . . . . . . . . . . . . 18 ⊢ (vol*‘(0[,]0)) = 0
216	208, 215	eqtri 2752	. . . . . . . . . . . . . . . . 17 ⊢ (vol‘(0[,]0)) = 0
217	204, 216	eqtrdi 2780	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
218	187, 217	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
219	183, 218	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
220	219	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
221	220	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
222	18, 17	ltnled 11281	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
223	222	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
224		simpl1 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ∈ ℝ)
225	17	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (abs‘𝑡) ∈ ℝ)
226		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ≤ (abs‘𝑡))
227	224, 225, 226	leltned 11287	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ (abs‘𝑡) ≠ 𝑅))
228	223, 227	bitr3d 281	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (¬ (abs‘𝑡) ≤ 𝑅 ↔ (abs‘𝑡) ≠ 𝑅))
229	228, 102	biimtrrdi 254	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) ≠ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
230	221, 229	pm2.61dne 3011	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
231	180, 230	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = 0)
232	231	ex 412	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) → (vol‘(𝑆 “ {𝑡})) = 0))
233	178, 232	sylbid 240	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0))
234	233	3expia 1121	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0)))
235	234	impd 410	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
236	164, 235	biimtrid 242	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
237	236	imp 406	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅))) → (vol‘(𝑆 “ {𝑡})) = 0)
238	163, 237	itgss 25729	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
239		negeq 11373	. . . . . . . . . 10 ⊢ (𝑅 = 0 → -𝑅 = -0)
240	239, 197	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑅 = 0 → -𝑅 = 0)
241		id 22	. . . . . . . . 9 ⊢ (𝑅 = 0 → 𝑅 = 0)
242	240, 241	oveq12d 7371	. . . . . . . 8 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0))
243		iooid 13294	. . . . . . . 8 ⊢ (0(,)0) = ∅
244	242, 243	eqtrdi 2780	. . . . . . 7 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = ∅)
245	244	adantl 481	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅)
246		itgeq1 25690	. . . . . 6 ⊢ ((-𝑅(,)𝑅) = ∅ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
247	245, 246	syl 17	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
248		itg0 25697	. . . . . 6 ⊢ ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0
249		sq0 14117	. . . . . . . . . 10 ⊢ (0↑2) = 0
250	249	oveq2i 7364	. . . . . . . . 9 ⊢ (π · (0↑2)) = (π · 0)
251		picn 26383	. . . . . . . . . 10 ⊢ π ∈ ℂ
252	251	mul01i 11324	. . . . . . . . 9 ⊢ (π · 0) = 0
253	250, 252	eqtr2i 2753	. . . . . . . 8 ⊢ 0 = (π · (0↑2))
254		oveq1 7360	. . . . . . . . 9 ⊢ (𝑅 = 0 → (𝑅↑2) = (0↑2))
255	254	oveq2d 7369	. . . . . . . 8 ⊢ (𝑅 = 0 → (π · (𝑅↑2)) = (π · (0↑2)))
256	253, 255	eqtr4id 2783	. . . . . . 7 ⊢ (𝑅 = 0 → 0 = (π · (𝑅↑2)))
257	256	adantl 481	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → 0 = (π · (𝑅↑2)))
258	248, 257	eqtrid 2776	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
259	247, 258	eqtrd 2764	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
260		simp1 1136	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ)
261		0red 11137	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ∈ ℝ)
262		simpr 484	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ 𝑅)
263	261, 77, 262	leltned 11287	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0 < 𝑅 ↔ 𝑅 ≠ 0))
264	263	biimp3ar 1472	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 0 < 𝑅)
265	260, 264	elrpd 12952	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ⁺)
266	265	3expa 1118	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ⁺)
267	157, 16	syl 17	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) ∈ ℝ)
268	267	adantl 481	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ∈ ℝ)
269		rpre 12920	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
270	269	adantr 480	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
271	269	renegcld 11565	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
272	271	rexrd 11184	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ^*)
273		rpxr 12921	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^*)
274	272, 273, 167	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
275		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
276	269	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
277	275, 276	absltd 15357	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
278	277	biimprd 248	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
279	278	exp4b 430	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → (abs‘𝑡) < 𝑅))))
280	279	3impd 1349	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
281	274, 280	sylbid 240	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) < 𝑅))
282	281	imp 406	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) < 𝑅)
283	268, 270, 282	ltled 11282	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅)
284	283, 112	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
285	269	resqcld 14050	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
286	285	recnd 11162	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
287	286	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
288	191	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
289	287, 288	subcld 11493	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
290	289	sqrtcld 15365	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
291	290, 290	subnegd 11500	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
292	157, 291	sylan2 593	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
293	285	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
294	8	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
295	293, 294	resubcld 11566	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
296	157, 295	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
297		0red 11137	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
298	16	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
299	19	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
300		rpge0 12925	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
301	300	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
302	298, 276, 299, 301	lt2sqd 14181	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
303	12	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
304	303	breq1d 5105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2)))
305	302, 277, 304	3bitr3rd 310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
306	294, 293	posdifd 11725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
307	305, 306	bitr3d 281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
308	307	biimpd 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
309	308	exp4b 430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < ((𝑅↑2) − (𝑡↑2))))))
310	309	3impd 1349	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
311	274, 310	sylbid 240	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
312	311	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < ((𝑅↑2) − (𝑡↑2)))
313	297, 296, 312	ltled 11282	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
314	296, 313	resqrtcld 15343	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
315	314	renegcld 11565	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
316	315, 314, 28	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
317	316, 30	syl 17	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
318	296, 313	sqrtge0d 15346	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
319	314, 314, 318, 318	addge0d 11714	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
320	292	breq2d 5107	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
321	314, 315	subge0d 11728	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
322	320, 321	bitr3d 281	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
323	319, 322	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
324	315, 314, 323, 47	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
325	317, 324	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
326		ax-resscn 11085	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
327	326	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ℝ ⊆ ℂ)
328	271, 269, 78	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
329		rpcn 12922	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
330	329	sqcld 14069	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
331	330	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
332	328	sselda 3937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ)
333	332	recnd 11162	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ)
334	329	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
335		rpne0 12928	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
336	335	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
337	333, 334, 336	divcld 11918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ)
338		asincl 26799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
339	337, 338	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
340		1cnd 11129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
341	337	sqcld 14069	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ)
342	340, 341	subcld 11493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ)
343	342	sqrtcld 15365	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ)
344	337, 343	mulcld 11154	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈ ℂ)
345	339, 344	addcld 11153	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈ ℂ)
346	331, 345	mulcld 11154	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈ ℂ)
347		tgioo4 24709	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
348		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
349		iccntr 24726	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
350	271, 269, 349	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
351	327, 328, 346, 347, 348, 350	dvmptntr 25891	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))))
352		areacirclem1 37690	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
353	351, 352	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
354	353	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
355		oveq1 7360	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2))
356	355	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2)))
357	356	fveq2d 6830	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
358	357	oveq2d 7369	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
359	358	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
360		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅))
361		ovexd 7388	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V)
362	354, 359, 360, 361	fvmptd 6941	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
363	157, 290	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
364	363	2timesd 12385	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
365	362, 364	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
366	292, 325, 365	3eqtr4rd 2775	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
367	284, 366	eqtr4d 2767	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡))
368	367	itgeq2dv 25699	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡)
369	269, 269, 300, 300	addge0d 11714	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅 + 𝑅))
370	329, 329	subnegd 11500	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 − -𝑅) = (𝑅 + 𝑅))
371	370	breq2d 5107	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ 0 ≤ (𝑅 + 𝑅)))
372	269, 271	subge0d 11728	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ -𝑅 ≤ 𝑅))
373	371, 372	bitr3d 281	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 + 𝑅) ↔ -𝑅 ≤ 𝑅))
374	369, 373	mpbid 232	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ≤ 𝑅)
375		2cn 12221	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
376	162, 326	sstri 3947	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ ℂ
377		ssid 3960	. . . . . . . . . . 11 ⊢ ℂ ⊆ ℂ
378	375, 376, 377	3pm3.2i 1340	. . . . . . . . . 10 ⊢ (2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ)
379		cncfmptc 24821	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
380	378, 379	mp1i 13	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
381		ioossicc 13354	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)
382		resmpt 5992	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))))
383	381, 382	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))
384		areacirclem2 37691	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
385	269, 300, 384	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
386		rescncf 24806	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)))
387	381, 385, 386	mpsyl 68	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
388	383, 387	eqeltrrid 2833	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
389	380, 388	mulcncf 25362	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
390	353, 389	eqeltrd 2828	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
391	381	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅))
392		ioombl 25482	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ∈ dom vol
393	392	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ∈ dom vol)
394		ovexd 7388	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V)
395		areacirclem3 37692	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
396	391, 393, 394, 395	iblss 25722	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
397	269, 300, 396	syl2anc 584	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
398	353, 397	eqeltrd 2828	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ 𝐿¹)
399		areacirclem4 37693	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
400	271, 269, 374, 390, 398, 399	ftc2nc 37684	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)))
401		eqidd 2730	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))
402		fvoveq1 7376	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅)))
403		oveq1 7360	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅))
404	403	oveq1d 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2))
405	404	oveq2d 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2)))
406	405	fveq2d 6830	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((𝑅 / 𝑅)↑2))))
407	403, 406	oveq12d 7371	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))
408	402, 407	oveq12d 7371	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))
409	408	oveq2d 7369	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
410	409	adantl 481	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
411		ubicc2 13386	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → 𝑅 ∈ (-𝑅[,]𝑅))
412	272, 273, 374, 411	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ (-𝑅[,]𝑅))
413		ovexd 7388	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V)
414	401, 410, 412, 413	fvmptd 6941	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
415	329, 335	dividd 11916	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) = 1)
416	415	fveq2d 6830	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (arcsin‘1))
417		asin1 26820	. . . . . . . . . . . . 13 ⊢ (arcsin‘1) = (π / 2)
418	416, 417	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (π / 2))
419	415	oveq1d 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = (1↑2))
420		sq1 14120	. . . . . . . . . . . . . . . . . . 19 ⊢ (1↑2) = 1
421	419, 420	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = 1)
422	421	oveq2d 7369	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = (1 − 1))
423		1cnd 11129	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 1 ∈ ℂ)
424	423	subidd 11481	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − 1) = 0)
425	422, 424	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = 0)
426	425	fveq2d 6830	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = (√‘0))
427	426, 195	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0)
428	427	oveq2d 7369	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0))
429	329, 329, 335	divcld 11918	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) ∈ ℂ)
430	429	mul01d 11333	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · 0) = 0)
431	428, 430	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = 0)
432	418, 431	oveq12d 7371	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) + 0))
433		2ne0 12250	. . . . . . . . . . . . . 14 ⊢ 2 ≠ 0
434	251, 375, 433	divcli 11884	. . . . . . . . . . . . 13 ⊢ (π / 2) ∈ ℂ
435	434	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (π / 2) ∈ ℂ)
436	435	addridd 11334	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) + 0) = (π / 2))
437	432, 436	eqtrd 2764	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2))
438	437	oveq2d 7369	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π / 2)))
439	414, 438	eqtrd 2764	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π / 2)))
440		fvoveq1 7376	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅)))
441		oveq1 7360	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅))
442	441	oveq1d 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2))
443	442	oveq2d 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2)))
444	443	fveq2d 6830	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((-𝑅 / 𝑅)↑2))))
445	441, 444	oveq12d 7371	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))
446	440, 445	oveq12d 7371	. . . . . . . . . . . 12 ⊢ (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
447	446	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
448	447	oveq2d 7369	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
449		lbicc2 13385	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → -𝑅 ∈ (-𝑅[,]𝑅))
450	272, 273, 374, 449	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ (-𝑅[,]𝑅))
451		ovexd 7388	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) ∈ V)
452	401, 448, 450, 451	fvmptd 6941	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
453	329, 329, 335	divnegd 11931	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = (-𝑅 / 𝑅))
454	415	negeqd 11375	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = -1)
455	453, 454	eqtr3d 2766	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) = -1)
456	455	fveq2d 6830	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = (arcsin‘-1))
457		ax-1cn 11086	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
458		asinneg 26812	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℂ → (arcsin‘-1) = -(arcsin‘1))
459	457, 458	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (arcsin‘-1) = -(arcsin‘1)
460	417	negeqi 11374	. . . . . . . . . . . . . 14 ⊢ -(arcsin‘1) = -(π / 2)
461	459, 460	eqtri 2752	. . . . . . . . . . . . 13 ⊢ (arcsin‘-1) = -(π / 2)
462	456, 461	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = -(π / 2))
463	455	oveq1d 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = (-1↑2))
464		neg1sqe1 14121	. . . . . . . . . . . . . . . . . . 19 ⊢ (-1↑2) = 1
465	463, 464	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = 1)
466	465	oveq2d 7369	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = (1 − 1))
467	466, 424	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = 0)
468	467	fveq2d 6830	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = (√‘0))
469	468, 195	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0)
470	469	oveq2d 7369	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0))
471	271	recnd 11162	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℂ)
472	471, 329, 335	divcld 11918	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) ∈ ℂ)
473	472	mul01d 11333	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · 0) = 0)
474	470, 473	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = 0)
475	462, 474	oveq12d 7371	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = (-(π / 2) + 0))
476	434	negcli 11450	. . . . . . . . . . . . 13 ⊢ -(π / 2) ∈ ℂ
477	476	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → -(π / 2) ∈ ℂ)
478	477	addridd 11334	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (-(π / 2) + 0) = -(π / 2))
479	475, 478	eqtrd 2764	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = -(π / 2))
480	479	oveq2d 7369	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π / 2)))
481	452, 480	eqtrd 2764	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π / 2)))
482	439, 481	oveq12d 7371	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
483	434, 434	subnegi 11461	. . . . . . . . . . 11 ⊢ ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
484		pidiv2halves 26392	. . . . . . . . . . 11 ⊢ ((π / 2) + (π / 2)) = π
485	483, 484	eqtri 2752	. . . . . . . . . 10 ⊢ ((π / 2) − -(π / 2)) = π
486	485	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) − -(π / 2)) = π)
487	486	oveq2d 7369	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = ((𝑅↑2) · π))
488	330, 435, 477	subdid 11594	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
489	251	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → π ∈ ℂ)
490	330, 489	mulcomd 11155	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · π) = (π · (𝑅↑2)))
491	487, 488, 490	3eqtr3d 2772	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))) = (π · (𝑅↑2)))
492	482, 491	eqtrd 2764	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (π · (𝑅↑2)))
493	368, 400, 492	3eqtrd 2768	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
494	266, 493	syl 17	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
495	259, 494	pm2.61dane 3012	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
496	161, 238, 495	3eqtr3d 2772	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡 = (π · (𝑅↑2)))
497	156, 496	eqtrd 2764	1 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 Vcvv 3438 ∖ cdif 3902 ⊆ wss 3905 ∅c0 4286 ifcif 4478 {csn 4579 class class class wbr 5095 {copab 5157 ↦ cmpt 5176 × cxp 5621 ^◡ccnv 5622 dom cdm 5623 ran crn 5624 ↾ cres 5625 “ cima 5626 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 +∞cpnf 11165 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11365 -cneg 11366 / cdiv 11795 2c2 12201 ℝ⁺crp 12911 (,)cioo 13266 [,]cicc 13269 ↑cexp 13986 √csqrt 15158 abscabs 15159 πcpi 15991 TopOpenctopn 17343 topGenctg 17359 ℂ_fldccnfld 21279 intcnt 22920 –cn→ccncf 24785 vol*covol 25379 volcvol 25380 𝐿¹cibl 25534 ∫citg 25535 D cdv 25780 arcsincasin 26788 areacarea 26881

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-symdif 4206 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-disj 5063 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-ofr 7618 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-omul 8400 df-er 8632 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-dju 9816 df-card 9854 df-acn 9857 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-q 12868 df-rp 12912 df-xneg 13032 df-xadd 13033 df-xmul 13034 df-ioo 13270 df-ioc 13271 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-fac 14199 df-bc 14228 df-hash 14256 df-shft 14992 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-limsup 15396 df-clim 15413 df-rlim 15414 df-sum 15612 df-ef 15992 df-sin 15994 df-cos 15995 df-tan 15996 df-pi 15997 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-xrs 17424 df-qtop 17429 df-imas 17430 df-xps 17432 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-submnd 18676 df-mulg 18965 df-cntz 19214 df-cmn 19679 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-fbas 21276 df-fg 21277 df-cnfld 21280 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-cld 22922 df-ntr 22923 df-cls 22924 df-nei 23001 df-lp 23039 df-perf 23040 df-cn 23130 df-cnp 23131 df-haus 23218 df-cmp 23290 df-tx 23465 df-hmeo 23658 df-fil 23749 df-fm 23841 df-flim 23842 df-flf 23843 df-xms 24224 df-ms 24225 df-tms 24226 df-cncf 24787 df-ovol 25381 df-vol 25382 df-mbf 25536 df-itg1 25537 df-itg2 25538 df-ibl 25539 df-itg 25540 df-0p 25587 df-limc 25783 df-dv 25784 df-log 26481 df-cxp 26482 df-asin 26791 df-area 26882

This theorem is referenced by: (None)

W3C validator