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 35002

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 5643	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ × ℝ)
3	1, 2	eqsstri 4001	. . . . 5 ⊢ 𝑆 ⊆ (ℝ × ℝ)
4	3	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ⊆ (ℝ × ℝ))
5	1	areacirclem5 35001	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
6		resqcl 13491	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
7	6	3ad2ant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
8		resqcl 13491	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
9	8	3ad2ant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
10	7, 9	resubcld 11068	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
11	10	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12		absresq 14662	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
13	12	3ad2ant3 1131	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
14	13	breq1d 5076	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
15		recn 10627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
16	15	abscld 14796	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
17	16	3ad2ant3 1131	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
18		simp1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
19	15	absge0d 14804	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
20	19	3ad2ant3 1131	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
21		simp2 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
22	17, 18, 20, 21	le2sqd 13621	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
23	7, 9	subge0d 11230	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
24	14, 22, 23	3bitr4d 313	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
25	24	biimpa 479	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
26	11, 25	resqrtcld 14777	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
27	26	renegcld 11067	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
28		iccmbl 24167	. . . . . . . . . 10 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
29	27, 26, 28	syl2anc 586	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
30		mblvol 24131	. . . . . . . . . . . 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 14780	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
33	26, 26, 32, 32	addge0d 11216	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
34		recn 10627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
35	34	sqcld 13509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
36	35	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
37	15	sqcld 13509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
38	37	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
39	36, 38	subcld 10997	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
40	39	sqrtcld 14797	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
41	40	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
42	41, 41	subnegd 11004	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
43	42	breq2d 5078	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
44	26, 27	subge0d 11230	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
45	43, 44	bitr3d 283	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
46	33, 45	mpbid 234	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
47		ovolicc 24124	. . . . . . . . . . . 12 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
48	27, 26, 46, 47	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
49	31, 48	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
50	26, 27	resubcld 11068	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈ ℝ)
51	49, 50	eqeltrd 2913	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)
52		volf 24130	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
53		ffn 6514	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
54		elpreima 6828	. . . . . . . . . 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 585	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (^◡vol “ ℝ))
57		0mbl 24140	. . . . . . . . . 10 ⊢ ∅ ∈ dom vol
58		mblvol 24131	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
59	57, 58	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
60		ovol0 24094	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
61	59, 60	eqtri 2844	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
62		0re 10643	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
63	61, 62	eqeltri 2909	. . . . . . . . . 10 ⊢ (vol‘∅) ∈ ℝ
64		elpreima 6828	. . . . . . . . . . 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 709	. . . . . . . . 9 ⊢ ∅ ∈ (^◡vol “ ℝ)
67	66	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ∅ ∈ (^◡vol “ ℝ))
68	56, 67	ifclda 4501	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈ (^◡vol “ ℝ))
69	5, 68	eqeltrd 2913	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
70	69	3expa 1114	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
71	70	ralrimiva 3182	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
72	5	fveq2d 6674	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
73	72	3expa 1114	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
74	73	mpteq2dva 5161	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) = (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))))
75		renegcl 10949	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
76	75	adantr 483	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → -𝑅 ∈ ℝ)
77		simpl 485	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑅 ∈ ℝ)
78		iccssre 12819	. . . . . . 7 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
79	76, 77, 78	syl2anc 586	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅[,]𝑅) ⊆ ℝ)
80		rembl 24141	. . . . . . 7 ⊢ ℝ ∈ dom vol
81	80	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ℝ ∈ dom vol)
82		fvexd 6685	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈ V)
83		eldif 3946	. . . . . . . . 9 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)))
84		3anass 1091	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
85	84	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
86	75	3ad2ant1 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → -𝑅 ∈ ℝ)
87		elicc2 12802	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
88	86, 18, 87	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89		simp3 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
90	89, 18	absled 14790	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
91	89	biantrurd 535	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
92	90, 91	bitrd 281	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
93	85, 88, 92	3bitr4rd 314	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 𝑡 ∈ (-𝑅[,]𝑅)))
94	93	biimpd 231	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 → 𝑡 ∈ (-𝑅[,]𝑅)))
95	94	con3d 155	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅))
96	95	3expia 1117	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅)))
97	96	impd 413	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
98	83, 97	syl5bi 244	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
99	98	imp 409	. . . . . . 7 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → ¬ (abs‘𝑡) ≤ 𝑅)
100		iffalse 4476	. . . . . . . . 9 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
101	100	fveq2d 6674	. . . . . . . 8 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘∅))
102	101, 61	syl6eq 2872	. . . . . . 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 586	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
105	90	biimprd 250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅))
106	105	expd 418	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅)))
107	106	3expia 1117	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅))))
108	107	3impd 1344	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅))
109	104, 108	sylbid 242	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → (abs‘𝑡) ≤ 𝑅))
110	109	3impia 1113	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (abs‘𝑡) ≤ 𝑅)
111		iftrue 4473	. . . . . . . . . . . 12 ⊢ ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
112	111	fveq2d 6674	. . . . . . . . . . 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 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
115	75, 78	mpancom 686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
116	115	sselda 3967	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
117	116	3adant2 1127	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
118	117	resqcld 13612	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
119	114, 118	resubcld 11068	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
120	75, 87	mpancom 686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
121	120	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
122	22, 90, 14	3bitr3rd 312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ (𝑅↑2) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
123	23, 122	bitrd 281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
124	123	biimprd 250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
125	124	expd 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2)))))
126	125	3expia 1117	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
127	126	3impd 1344	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
128	121, 127	sylbid 242	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
129	128	3impia 1113	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
130	119, 129	resqrtcld 14777	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
131	130	renegcld 11067	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
132	131, 130, 28	syl2anc 586	. . . . . . . . . . 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 10669	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
135	134	sqrtcld 14797	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
136	135, 135	subnegd 11004	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
137	119, 129	sqrtge0d 14780	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
138	130, 130, 137, 137	addge0d 11216	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
139	136	breq2d 5078	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
140	130, 131	subge0d 11230	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
141	139, 140	bitr3d 283	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
142	138, 141	mpbid 234	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
143	131, 130, 142, 47	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
144	135	2timesd 11881	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
145	136, 143, 144	3eqtr4d 2866	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
146	113, 133, 145	3eqtrd 2860	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
147	146	3expa 1114	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
148	147	mpteq2dva 5161	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
149		areacirclem3 34999	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿¹)
150	148, 149	eqeltrd 2913	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
151	79, 81, 82, 103, 150	iblss2 24406	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
152	74, 151	eqeltrd 2913	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹)
153		dmarea 25535	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹))
154	4, 71, 152, 153	syl3anbrc 1339	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ∈ dom area)
155		areaval 25542	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
156	154, 155	syl 17	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
157		elioore 12769	. . . . . 6 ⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
158	5	3expa 1114	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
159	157, 158	sylan2 594	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
160	159	fveq2d 6674	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
161	160	itgeq2dv 24382	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
162		ioossre 12799	. . . . 5 ⊢ (-𝑅(,)𝑅) ⊆ ℝ
163	162	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ ℝ)
164		eldif 3946	. . . . . 6 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)))
165	75	rexrd 10691	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ^*)
166		rexr 10687	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℝ^*)
167		elioo2 12780	. . . . . . . . . . . . . 14 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
168	165, 166, 167	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
169	168	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
170	89	biantrurd 535	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
171	89, 18	absltd 14789	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
172		3anass 1091	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
173	172	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
174	170, 171, 173	3bitr4rd 314	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (abs‘𝑡) < 𝑅))
175	169, 174	bitrd 281	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (abs‘𝑡) < 𝑅))
176	175	notbid 320	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ ¬ (abs‘𝑡) < 𝑅))
177	18, 17	lenltd 10786	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) ↔ ¬ (abs‘𝑡) < 𝑅))
178	176, 177	bitr4d 284	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ 𝑅 ≤ (abs‘𝑡)))
179	5	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
180	179	fveq2d 6674	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
181	17	anim1i 616	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅))
182		eqle 10742	. . . . . . . . . . . . . . . 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 7163	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘𝑡) = 𝑅 → ((abs‘𝑡)↑2) = (𝑅↑2))
185	184	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑅↑2))
186	13	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑡↑2))
187	185, 186	eqtr3d 2858	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2))
188		fvoveq1 7179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑡↑2) − (𝑡↑2))))
189	188	negeqd 10880	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) = -(√‘((𝑡↑2) − (𝑡↑2))))
190	189, 188	oveq12d 7174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))))
191	8	recnd 10669	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
192	191	subidd 10985	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0)
193	192	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = (√‘0))
194	193	negeqd 10880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = -(√‘0))
195		sqrt0 14601	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (√‘0) = 0
196	195	negeqi 10879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -(√‘0) = -0
197		neg0 10932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -0 = 0
198	196, 197	eqtri 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(√‘0) = 0
199	194, 198	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = 0)
200	193, 195	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = 0)
201	199, 200	oveq12d 7174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
202	201	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
203	190, 202	sylan9eqr 2878	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (0[,]0))
204	203	fveq2d 6674	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol‘(0[,]0)))
205		iccmbl 24167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom vol)
206	62, 62, 205	mp2an 690	. . . . . . . . . . . . . . . . . . 19 ⊢ (0[,]0) ∈ dom vol
207		mblvol 24131	. . . . . . . . . . . . . . . . . . 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 10688	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℝ^*
210		iccid 12784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℝ^* → (0[,]0) = {0})
211	210	fveq2d 6674	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ^* → (vol‘(0[,]0)) = (vol‘{0}))
212	209, 211	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol‘(0[,]0)) = (vol‘{0})
213		ovolsn 24096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (vol*‘{0}) = 0)
214	62, 213	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol*‘{0}) = 0
215	212, 214	eqtri 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (vol*‘(0[,]0)) = 0
216	208, 215	eqtri 2844	. . . . . . . . . . . . . . . . 17 ⊢ (vol‘(0[,]0)) = 0
217	204, 216	syl6eq 2872	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
218	187, 217	syldan 593	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = 0)
219	183, 218	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
220	219	ex 415	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
221	220	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
222	18, 17	ltnled 10787	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
223	222	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
224		simpl1 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ∈ ℝ)
225	17	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (abs‘𝑡) ∈ ℝ)
226		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ≤ (abs‘𝑡))
227	224, 225, 226	leltned 10793	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ (abs‘𝑡) ≠ 𝑅))
228	223, 227	bitr3d 283	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (¬ (abs‘𝑡) ≤ 𝑅 ↔ (abs‘𝑡) ≠ 𝑅))
229	228, 102	syl6bir 256	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) ≠ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
230	221, 229	pm2.61dne 3103	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
231	180, 230	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = 0)
232	231	ex 415	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) → (vol‘(𝑆 “ {𝑡})) = 0))
233	178, 232	sylbid 242	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0))
234	233	3expia 1117	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0)))
235	234	impd 413	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
236	164, 235	syl5bi 244	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
237	236	imp 409	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅))) → (vol‘(𝑆 “ {𝑡})) = 0)
238	163, 237	itgss 24412	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
239		negeq 10878	. . . . . . . . . 10 ⊢ (𝑅 = 0 → -𝑅 = -0)
240	239, 197	syl6eq 2872	. . . . . . . . 9 ⊢ (𝑅 = 0 → -𝑅 = 0)
241		id 22	. . . . . . . . 9 ⊢ (𝑅 = 0 → 𝑅 = 0)
242	240, 241	oveq12d 7174	. . . . . . . 8 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0))
243		iooid 12767	. . . . . . . 8 ⊢ (0(,)0) = ∅
244	242, 243	syl6eq 2872	. . . . . . 7 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = ∅)
245	244	adantl 484	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅)
246		itgeq1 24373	. . . . . 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 24380	. . . . . 6 ⊢ ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0
249		oveq1 7163	. . . . . . . . 9 ⊢ (𝑅 = 0 → (𝑅↑2) = (0↑2))
250	249	oveq2d 7172	. . . . . . . 8 ⊢ (𝑅 = 0 → (π · (𝑅↑2)) = (π · (0↑2)))
251		sq0 13556	. . . . . . . . . 10 ⊢ (0↑2) = 0
252	251	oveq2i 7167	. . . . . . . . 9 ⊢ (π · (0↑2)) = (π · 0)
253		picn 25045	. . . . . . . . . 10 ⊢ π ∈ ℂ
254	253	mul01i 10830	. . . . . . . . 9 ⊢ (π · 0) = 0
255	252, 254	eqtr2i 2845	. . . . . . . 8 ⊢ 0 = (π · (0↑2))
256	250, 255	syl6reqr 2875	. . . . . . 7 ⊢ (𝑅 = 0 → 0 = (π · (𝑅↑2)))
257	256	adantl 484	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → 0 = (π · (𝑅↑2)))
258	248, 257	syl5eq 2868	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
259	247, 258	eqtrd 2856	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
260		simp1 1132	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ)
261		0red 10644	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ∈ ℝ)
262		simpr 487	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ 𝑅)
263	261, 77, 262	leltned 10793	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0 < 𝑅 ↔ 𝑅 ≠ 0))
264	263	biimp3ar 1466	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 0 < 𝑅)
265	260, 264	elrpd 12429	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ⁺)
266	265	3expa 1114	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ⁺)
267	157, 16	syl 17	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) ∈ ℝ)
268	267	adantl 484	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ∈ ℝ)
269		rpre 12398	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
270	269	adantr 483	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
271	269	renegcld 11067	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
272	271	rexrd 10691	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ^*)
273		rpxr 12399	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^*)
274	272, 273, 167	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
275		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
276	269	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
277	275, 276	absltd 14789	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
278	277	biimprd 250	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
279	278	exp4b 433	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → (abs‘𝑡) < 𝑅))))
280	279	3impd 1344	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
281	274, 280	sylbid 242	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) < 𝑅))
282	281	imp 409	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) < 𝑅)
283	268, 270, 282	ltled 10788	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅)
284	283, 112	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
285	269	resqcld 13612	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
286	285	recnd 10669	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
287	286	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
288	191	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
289	287, 288	subcld 10997	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
290	289	sqrtcld 14797	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
291	290, 290	subnegd 11004	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
292	157, 291	sylan2 594	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
293	285	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
294	8	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
295	293, 294	resubcld 11068	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
296	157, 295	sylan2 594	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
297		0red 10644	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
298	16	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
299	19	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
300		rpge0 12403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
301	300	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
302	298, 276, 299, 301	lt2sqd 13620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
303	12	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
304	303	breq1d 5076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2)))
305	302, 277, 304	3bitr3rd 312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
306	294, 293	posdifd 11227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
307	305, 306	bitr3d 283	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
308	307	biimpd 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
309	308	exp4b 433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < ((𝑅↑2) − (𝑡↑2))))))
310	309	3impd 1344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
311	274, 310	sylbid 242	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
312	311	imp 409	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < ((𝑅↑2) − (𝑡↑2)))
313	297, 296, 312	ltled 10788	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
314	296, 313	resqrtcld 14777	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
315	314	renegcld 11067	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
316	315, 314, 28	syl2anc 586	. . . . . . . . . . 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 14780	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
319	314, 314, 318, 318	addge0d 11216	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
320	292	breq2d 5078	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
321	314, 315	subge0d 11230	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
322	320, 321	bitr3d 283	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
323	319, 322	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
324	315, 314, 323, 47	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
325	317, 324	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
326		ax-resscn 10594	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
327	326	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ℝ ⊆ ℂ)
328	271, 269, 78	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
329		rpcn 12400	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
330	329	sqcld 13509	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
331	330	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
332	328	sselda 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ)
333	332	recnd 10669	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ)
334	329	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
335		rpne0 12406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
336	335	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
337	333, 334, 336	divcld 11416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ)
338		asincl 25451	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
339	337, 338	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
340		1cnd 10636	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
341	337	sqcld 13509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ)
342	340, 341	subcld 10997	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ)
343	342	sqrtcld 14797	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ)
344	337, 343	mulcld 10661	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈ ℂ)
345	339, 344	addcld 10660	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈ ℂ)
346	331, 345	mulcld 10661	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈ ℂ)
347		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
348	347	tgioo2 23411	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
349		iccntr 23429	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
350	271, 269, 349	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
351	327, 328, 346, 348, 347, 350	dvmptntr 24568	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))))
352		areacirclem1 34997	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
353	351, 352	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
354	353	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
355		oveq1 7163	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2))
356	355	oveq2d 7172	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2)))
357	356	fveq2d 6674	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
358	357	oveq2d 7172	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
359	358	adantl 484	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
360		simpr 487	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅))
361		ovexd 7191	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V)
362	354, 359, 360, 361	fvmptd 6775	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
363	157, 290	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
364	363	2timesd 11881	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
365	362, 364	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
366	292, 325, 365	3eqtr4rd 2867	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
367	284, 366	eqtr4d 2859	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡))
368	367	itgeq2dv 24382	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡)
369	269, 269, 300, 300	addge0d 11216	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅 + 𝑅))
370	329, 329	subnegd 11004	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 − -𝑅) = (𝑅 + 𝑅))
371	370	breq2d 5078	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ 0 ≤ (𝑅 + 𝑅)))
372	269, 271	subge0d 11230	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ -𝑅 ≤ 𝑅))
373	371, 372	bitr3d 283	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 + 𝑅) ↔ -𝑅 ≤ 𝑅))
374	369, 373	mpbid 234	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ≤ 𝑅)
375		2cn 11713	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
376	162, 326	sstri 3976	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ ℂ
377		ssid 3989	. . . . . . . . . . 11 ⊢ ℂ ⊆ ℂ
378	375, 376, 377	3pm3.2i 1335	. . . . . . . . . 10 ⊢ (2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ)
379		cncfmptc 23519	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
380	378, 379	mp1i 13	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
381		ioossicc 12823	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)
382		resmpt 5905	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))))
383	381, 382	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))
384		areacirclem2 34998	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
385	269, 300, 384	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
386		rescncf 23505	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)))
387	381, 385, 386	mpsyl 68	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
388	383, 387	eqeltrrid 2918	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
389	380, 388	mulcncf 24047	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
390	353, 389	eqeltrd 2913	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
391	381	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅))
392		ioombl 24166	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ∈ dom vol
393	392	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ∈ dom vol)
394		ovexd 7191	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V)
395		areacirclem3 34999	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
396	391, 393, 394, 395	iblss 24405	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
397	269, 300, 396	syl2anc 586	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
398	353, 397	eqeltrd 2913	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ 𝐿¹)
399		areacirclem4 35000	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
400	271, 269, 374, 390, 398, 399	ftc2nc 34991	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)))
401		eqidd 2822	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))
402		fvoveq1 7179	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅)))
403		oveq1 7163	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅))
404	403	oveq1d 7171	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2))
405	404	oveq2d 7172	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2)))
406	405	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((𝑅 / 𝑅)↑2))))
407	403, 406	oveq12d 7174	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))
408	402, 407	oveq12d 7174	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))
409	408	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
410	409	adantl 484	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
411		ubicc2 12854	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → 𝑅 ∈ (-𝑅[,]𝑅))
412	272, 273, 374, 411	syl3anc 1367	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ (-𝑅[,]𝑅))
413		ovexd 7191	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V)
414	401, 410, 412, 413	fvmptd 6775	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
415	329, 335	dividd 11414	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) = 1)
416	415	fveq2d 6674	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (arcsin‘1))
417		asin1 25472	. . . . . . . . . . . . 13 ⊢ (arcsin‘1) = (π / 2)
418	416, 417	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (π / 2))
419	415	oveq1d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = (1↑2))
420		sq1 13559	. . . . . . . . . . . . . . . . . . 19 ⊢ (1↑2) = 1
421	419, 420	syl6eq 2872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = 1)
422	421	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = (1 − 1))
423		1cnd 10636	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 1 ∈ ℂ)
424	423	subidd 10985	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − 1) = 0)
425	422, 424	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = 0)
426	425	fveq2d 6674	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = (√‘0))
427	426, 195	syl6eq 2872	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0)
428	427	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0))
429	329, 329, 335	divcld 11416	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) ∈ ℂ)
430	429	mul01d 10839	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · 0) = 0)
431	428, 430	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = 0)
432	418, 431	oveq12d 7174	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) + 0))
433		2ne0 11742	. . . . . . . . . . . . . 14 ⊢ 2 ≠ 0
434	253, 375, 433	divcli 11382	. . . . . . . . . . . . 13 ⊢ (π / 2) ∈ ℂ
435	434	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (π / 2) ∈ ℂ)
436	435	addid1d 10840	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) + 0) = (π / 2))
437	432, 436	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2))
438	437	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π / 2)))
439	414, 438	eqtrd 2856	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π / 2)))
440		fvoveq1 7179	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅)))
441		oveq1 7163	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅))
442	441	oveq1d 7171	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2))
443	442	oveq2d 7172	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2)))
444	443	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((-𝑅 / 𝑅)↑2))))
445	441, 444	oveq12d 7174	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))
446	440, 445	oveq12d 7174	. . . . . . . . . . . 12 ⊢ (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
447	446	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
448	447	oveq2d 7172	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
449		lbicc2 12853	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → -𝑅 ∈ (-𝑅[,]𝑅))
450	272, 273, 374, 449	syl3anc 1367	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ (-𝑅[,]𝑅))
451		ovexd 7191	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) ∈ V)
452	401, 448, 450, 451	fvmptd 6775	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
453	329, 329, 335	divnegd 11429	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = (-𝑅 / 𝑅))
454	415	negeqd 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = -1)
455	453, 454	eqtr3d 2858	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) = -1)
456	455	fveq2d 6674	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = (arcsin‘-1))
457		ax-1cn 10595	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
458		asinneg 25464	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℂ → (arcsin‘-1) = -(arcsin‘1))
459	457, 458	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (arcsin‘-1) = -(arcsin‘1)
460	417	negeqi 10879	. . . . . . . . . . . . . 14 ⊢ -(arcsin‘1) = -(π / 2)
461	459, 460	eqtri 2844	. . . . . . . . . . . . 13 ⊢ (arcsin‘-1) = -(π / 2)
462	456, 461	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = -(π / 2))
463	455	oveq1d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = (-1↑2))
464		neg1sqe1 13560	. . . . . . . . . . . . . . . . . . 19 ⊢ (-1↑2) = 1
465	463, 464	syl6eq 2872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = 1)
466	465	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = (1 − 1))
467	466, 424	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = 0)
468	467	fveq2d 6674	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = (√‘0))
469	468, 195	syl6eq 2872	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0)
470	469	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0))
471	271	recnd 10669	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℂ)
472	471, 329, 335	divcld 11416	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) ∈ ℂ)
473	472	mul01d 10839	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · 0) = 0)
474	470, 473	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = 0)
475	462, 474	oveq12d 7174	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = (-(π / 2) + 0))
476	434	negcli 10954	. . . . . . . . . . . . 13 ⊢ -(π / 2) ∈ ℂ
477	476	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → -(π / 2) ∈ ℂ)
478	477	addid1d 10840	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (-(π / 2) + 0) = -(π / 2))
479	475, 478	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = -(π / 2))
480	479	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π / 2)))
481	452, 480	eqtrd 2856	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π / 2)))
482	439, 481	oveq12d 7174	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
483	434, 434	subnegi 10965	. . . . . . . . . . 11 ⊢ ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
484		pidiv2halves 25053	. . . . . . . . . . 11 ⊢ ((π / 2) + (π / 2)) = π
485	483, 484	eqtri 2844	. . . . . . . . . 10 ⊢ ((π / 2) − -(π / 2)) = π
486	485	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) − -(π / 2)) = π)
487	486	oveq2d 7172	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = ((𝑅↑2) · π))
488	330, 435, 477	subdid 11096	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
489	253	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → π ∈ ℂ)
490	330, 489	mulcomd 10662	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · π) = (π · (𝑅↑2)))
491	487, 488, 490	3eqtr3d 2864	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))) = (π · (𝑅↑2)))
492	482, 491	eqtrd 2856	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (π · (𝑅↑2)))
493	368, 400, 492	3eqtrd 2860	. . . . 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 3104	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
496	161, 238, 495	3eqtr3d 2864	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡 = (π · (𝑅↑2)))
497	156, 496	eqtrd 2856	1 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 Vcvv 3494 ∖ cdif 3933 ⊆ wss 3936 ∅c0 4291 ifcif 4467 {csn 4567 class class class wbr 5066 {copab 5128 ↦ cmpt 5146 × cxp 5553 ^◡ccnv 5554 dom cdm 5555 ran crn 5556 ↾ cres 5557 “ cima 5558 Fn wfn 6350 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 +∞cpnf 10672 ℝ^*cxr 10674 < clt 10675 ≤ cle 10676 − cmin 10870 -cneg 10871 / cdiv 11297 2c2 11693 ℝ⁺crp 12390 (,)cioo 12739 [,]cicc 12742 ↑cexp 13430 √csqrt 14592 abscabs 14593 πcpi 15420 TopOpenctopn 16695 topGenctg 16711 ℂ_fldccnfld 20545 intcnt 21625 –cn→ccncf 23484 vol*covol 24063 volcvol 24064 𝐿¹cibl 24218 ∫citg 24219 D cdv 24461 arcsincasin 25440 areacarea 25533

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-symdif 4219 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-disj 5032 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-ofr 7410 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-omul 8107 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-dju 9330 df-card 9368 df-acn 9371 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-shft 14426 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-limsup 14828 df-clim 14845 df-rlim 14846 df-sum 15043 df-ef 15421 df-sin 15423 df-cos 15424 df-tan 15425 df-pi 15426 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-mulg 18225 df-cntz 18447 df-cmn 18908 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-cmp 21995 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-ovol 24065 df-vol 24066 df-mbf 24220 df-itg1 24221 df-itg2 24222 df-ibl 24223 df-itg 24224 df-0p 24271 df-limc 24464 df-dv 24465 df-log 25140 df-cxp 25141 df-asin 25443 df-area 25534

This theorem is referenced by: (None)

W3C validator