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 37753

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 5703	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ × ℝ)
3	1, 2	eqsstri 3976	. . . . 5 ⊢ 𝑆 ⊆ (ℝ × ℝ)
4	3	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ⊆ (ℝ × ℝ))
5	1	areacirclem5 37752	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
6		resqcl 14026	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
7	6	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
8		resqcl 14026	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
9	8	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
10	7, 9	resubcld 11540	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
11	10	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12		absresq 15204	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
13	12	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
14	13	breq1d 5096	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
15		recn 11091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
16	15	abscld 15341	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
17	16	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
18		simp1 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
19	15	absge0d 15349	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
20	19	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
21		simp2 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
22	17, 18, 20, 21	le2sqd 14159	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
23	7, 9	subge0d 11702	. . . . . . . . . . . . . 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 15320	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
27	26	renegcld 11539	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
28		iccmbl 25489	. . . . . . . . . 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 25453	. . . . . . . . . . . 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 15323	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
33	26, 26, 32, 32	addge0d 11688	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
34		recn 11091	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
35	34	sqcld 14046	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
36	35	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
37	15	sqcld 14046	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
38	37	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
39	36, 38	subcld 11467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
40	39	sqrtcld 15342	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
41	40	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
42	41, 41	subnegd 11474	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
43	42	breq2d 5098	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
44	26, 27	subge0d 11702	. . . . . . . . . . . . . 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 25446	. . . . . . . . . . . 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 2766	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
50	26, 27	resubcld 11540	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈ ℝ)
51	49, 50	eqeltrd 2831	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)
52		volf 25452	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
53		ffn 6646	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
54		elpreima 6986	. . . . . . . . . 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 25462	. . . . . . . . . 10 ⊢ ∅ ∈ dom vol
58		mblvol 25453	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
59	57, 58	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
60		ovol0 25416	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
61	59, 60	eqtri 2754	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
62		0re 11109	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
63	61, 62	eqeltri 2827	. . . . . . . . . 10 ⊢ (vol‘∅) ∈ ℝ
64		elpreima 6986	. . . . . . . . . . 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 4506	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈ (^◡vol “ ℝ))
69	5, 68	eqeltrd 2831	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
70	69	3expa 1118	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
71	70	ralrimiva 3124	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
72	5	fveq2d 6821	. . . . . . 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 5179	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) = (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))))
75		renegcl 11419	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
76	75	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → -𝑅 ∈ ℝ)
77		simpl 482	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑅 ∈ ℝ)
78		iccssre 13324	. . . . . . 7 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
79	76, 77, 78	syl2anc 584	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅[,]𝑅) ⊆ ℝ)
80		rembl 25463	. . . . . . 7 ⊢ ℝ ∈ dom vol
81	80	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ℝ ∈ dom vol)
82		fvexd 6832	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈ V)
83		eldif 3907	. . . . . . . . 9 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)))
84		3anass 1094	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
85	84	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
86	75	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → -𝑅 ∈ ℝ)
87		elicc2 13306	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
88	86, 18, 87	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89		simp3 1138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
90	89, 18	absled 15335	. . . . . . . . . . . . . . 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 4479	. . . . . . . . 9 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
101	100	fveq2d 6821	. . . . . . . 8 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘∅))
102	101, 61	eqtrdi 2782	. . . . . . 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 4476	. . . . . . . . . . . 12 ⊢ ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
112	111	fveq2d 6821	. . . . . . . . . . 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 3929	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
117	116	3adant2 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
118	117	resqcld 14027	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
119	114, 118	resubcld 11540	. . . . . . . . . . . . . 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 15320	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
131	130	renegcld 11539	. . . . . . . . . . . 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 11135	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
135	134	sqrtcld 15342	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
136	135, 135	subnegd 11474	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
137	119, 129	sqrtge0d 15323	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
138	130, 130, 137, 137	addge0d 11688	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
139	136	breq2d 5098	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
140	130, 131	subge0d 11702	. . . . . . . . . . . . . 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 12359	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
145	136, 143, 144	3eqtr4d 2776	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
146	113, 133, 145	3eqtrd 2770	. . . . . . . . 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 5179	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
149		areacirclem3 37750	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿¹)
150	148, 149	eqeltrd 2831	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
151	79, 81, 82, 103, 150	iblss2 25729	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
152	74, 151	eqeltrd 2831	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹)
153		dmarea 26889	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹))
154	4, 71, 152, 153	syl3anbrc 1344	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ∈ dom area)
155		areaval 26896	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
156	154, 155	syl 17	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
157		elioore 13270	. . . . . 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 6821	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
161	160	itgeq2dv 25705	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
162		ioossre 13302	. . . . 5 ⊢ (-𝑅(,)𝑅) ⊆ ℝ
163	162	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ ℝ)
164		eldif 3907	. . . . . 6 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)))
165	75	rexrd 11157	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ^*)
166		rexr 11153	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℝ^*)
167		elioo2 13281	. . . . . . . . . . . . . 14 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
168	165, 166, 167	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
169	168	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
170	89	biantrurd 532	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
171	89, 18	absltd 15334	. . . . . . . . . . . . 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 11254	. . . . . . . . . 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 6821	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
181	17	anim1i 615	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅))
182		eqle 11210	. . . . . . . . . . . . . . . 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 7348	. . . . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2))
188		fvoveq1 7364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑡↑2) − (𝑡↑2))))
189	188	negeqd 11349	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) = -(√‘((𝑡↑2) − (𝑡↑2))))
190	189, 188	oveq12d 7359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))))
191	8	recnd 11135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
192	191	subidd 11455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0)
193	192	fveq2d 6821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = (√‘0))
194	193	negeqd 11349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = -(√‘0))
195		sqrt0 15143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (√‘0) = 0
196	195	negeqi 11348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -(√‘0) = -0
197		neg0 11402	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -0 = 0
198	196, 197	eqtri 2754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(√‘0) = 0
199	194, 198	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = 0)
200	193, 195	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = 0)
201	199, 200	oveq12d 7359	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
202	201	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
203	190, 202	sylan9eqr 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (0[,]0))
204	203	fveq2d 6821	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol‘(0[,]0)))
205		iccmbl 25489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom vol)
206	62, 62, 205	mp2an 692	. . . . . . . . . . . . . . . . . . 19 ⊢ (0[,]0) ∈ dom vol
207		mblvol 25453	. . . . . . . . . . . . . . . . . . 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 11154	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℝ^*
210		iccid 13285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℝ^* → (0[,]0) = {0})
211	210	fveq2d 6821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ^* → (vol‘(0[,]0)) = (vol‘{0}))
212	209, 211	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol‘(0[,]0)) = (vol‘{0})
213		ovolsn 25418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (vol*‘{0}) = 0)
214	62, 213	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol*‘{0}) = 0
215	212, 214	eqtri 2754	. . . . . . . . . . . . . . . . . 18 ⊢ (vol*‘(0[,]0)) = 0
216	208, 215	eqtri 2754	. . . . . . . . . . . . . . . . 17 ⊢ (vol‘(0[,]0)) = 0
217	204, 216	eqtrdi 2782	. . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . 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 11255	. . . . . . . . . . . . . . 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 11261	. . . . . . . . . . . . . 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 3014	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
231	180, 230	eqtrd 2766	. . . . . . . . . 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 25735	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
239		negeq 11347	. . . . . . . . . 10 ⊢ (𝑅 = 0 → -𝑅 = -0)
240	239, 197	eqtrdi 2782	. . . . . . . . 9 ⊢ (𝑅 = 0 → -𝑅 = 0)
241		id 22	. . . . . . . . 9 ⊢ (𝑅 = 0 → 𝑅 = 0)
242	240, 241	oveq12d 7359	. . . . . . . 8 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0))
243		iooid 13268	. . . . . . . 8 ⊢ (0(,)0) = ∅
244	242, 243	eqtrdi 2782	. . . . . . 7 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = ∅)
245	244	adantl 481	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅)
246		itgeq1 25696	. . . . . 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 25703	. . . . . 6 ⊢ ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0
249		sq0 14094	. . . . . . . . . 10 ⊢ (0↑2) = 0
250	249	oveq2i 7352	. . . . . . . . 9 ⊢ (π · (0↑2)) = (π · 0)
251		picn 26389	. . . . . . . . . 10 ⊢ π ∈ ℂ
252	251	mul01i 11298	. . . . . . . . 9 ⊢ (π · 0) = 0
253	250, 252	eqtr2i 2755	. . . . . . . 8 ⊢ 0 = (π · (0↑2))
254		oveq1 7348	. . . . . . . . 9 ⊢ (𝑅 = 0 → (𝑅↑2) = (0↑2))
255	254	oveq2d 7357	. . . . . . . 8 ⊢ (𝑅 = 0 → (π · (𝑅↑2)) = (π · (0↑2)))
256	253, 255	eqtr4id 2785	. . . . . . 7 ⊢ (𝑅 = 0 → 0 = (π · (𝑅↑2)))
257	256	adantl 481	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → 0 = (π · (𝑅↑2)))
258	248, 257	eqtrid 2778	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
259	247, 258	eqtrd 2766	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
260		simp1 1136	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ)
261		0red 11110	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ∈ ℝ)
262		simpr 484	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ 𝑅)
263	261, 77, 262	leltned 11261	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0 < 𝑅 ↔ 𝑅 ≠ 0))
264	263	biimp3ar 1472	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 0 < 𝑅)
265	260, 264	elrpd 12926	. . . . . 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 12894	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
270	269	adantr 480	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
271	269	renegcld 11539	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
272	271	rexrd 11157	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ^*)
273		rpxr 12895	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^*)
274	272, 273, 167	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
275		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
276	269	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
277	275, 276	absltd 15334	. . . . . . . . . . . . . . 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 11256	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅)
284	283, 112	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
285	269	resqcld 14027	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
286	285	recnd 11135	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
287	286	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
288	191	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
289	287, 288	subcld 11467	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
290	289	sqrtcld 15342	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
291	290, 290	subnegd 11474	. . . . . . . . . 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 11540	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
296	157, 295	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
297		0red 11110	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
298	16	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
299	19	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
300		rpge0 12899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
301	300	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
302	298, 276, 299, 301	lt2sqd 14158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
303	12	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
304	303	breq1d 5096	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2)))
305	302, 277, 304	3bitr3rd 310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
306	294, 293	posdifd 11699	. . . . . . . . . . . . . . . . . . . . 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 11256	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
314	296, 313	resqrtcld 15320	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
315	314	renegcld 11539	. . . . . . . . . . . 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 15323	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
319	314, 314, 318, 318	addge0d 11688	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
320	292	breq2d 5098	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
321	314, 315	subge0d 11702	. . . . . . . . . . . . 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 2766	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
326		ax-resscn 11058	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
327	326	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ℝ ⊆ ℂ)
328	271, 269, 78	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
329		rpcn 12896	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
330	329	sqcld 14046	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
331	330	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
332	328	sselda 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ)
333	332	recnd 11135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ)
334	329	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
335		rpne0 12902	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
336	335	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
337	333, 334, 336	divcld 11892	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ)
338		asincl 26805	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
339	337, 338	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
340		1cnd 11102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
341	337	sqcld 14046	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ)
342	340, 341	subcld 11467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ)
343	342	sqrtcld 15342	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ)
344	337, 343	mulcld 11127	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈ ℂ)
345	339, 344	addcld 11126	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈ ℂ)
346	331, 345	mulcld 11127	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈ ℂ)
347		tgioo4 24715	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
348		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
349		iccntr 24732	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
350	271, 269, 349	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
351	327, 328, 346, 347, 348, 350	dvmptntr 25897	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))))
352		areacirclem1 37748	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
353	351, 352	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
354	353	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
355		oveq1 7348	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2))
356	355	oveq2d 7357	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2)))
357	356	fveq2d 6821	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
358	357	oveq2d 7357	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
359	358	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
360		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅))
361		ovexd 7376	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V)
362	354, 359, 360, 361	fvmptd 6931	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
363	157, 290	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
364	363	2timesd 12359	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
365	362, 364	eqtrd 2766	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
366	292, 325, 365	3eqtr4rd 2777	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
367	284, 366	eqtr4d 2769	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡))
368	367	itgeq2dv 25705	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡)
369	269, 269, 300, 300	addge0d 11688	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅 + 𝑅))
370	329, 329	subnegd 11474	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 − -𝑅) = (𝑅 + 𝑅))
371	370	breq2d 5098	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ 0 ≤ (𝑅 + 𝑅)))
372	269, 271	subge0d 11702	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ -𝑅 ≤ 𝑅))
373	371, 372	bitr3d 281	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 + 𝑅) ↔ -𝑅 ≤ 𝑅))
374	369, 373	mpbid 232	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ≤ 𝑅)
375		2cn 12195	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
376	162, 326	sstri 3939	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ ℂ
377		ssid 3952	. . . . . . . . . . 11 ⊢ ℂ ⊆ ℂ
378	375, 376, 377	3pm3.2i 1340	. . . . . . . . . 10 ⊢ (2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ)
379		cncfmptc 24827	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
380	378, 379	mp1i 13	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
381		ioossicc 13328	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)
382		resmpt 5981	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))))
383	381, 382	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))
384		areacirclem2 37749	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
385	269, 300, 384	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
386		rescncf 24812	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)))
387	381, 385, 386	mpsyl 68	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
388	383, 387	eqeltrrid 2836	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
389	380, 388	mulcncf 25368	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
390	353, 389	eqeltrd 2831	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
391	381	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅))
392		ioombl 25488	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ∈ dom vol
393	392	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ∈ dom vol)
394		ovexd 7376	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V)
395		areacirclem3 37750	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
396	391, 393, 394, 395	iblss 25728	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
397	269, 300, 396	syl2anc 584	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
398	353, 397	eqeltrd 2831	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ 𝐿¹)
399		areacirclem4 37751	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
400	271, 269, 374, 390, 398, 399	ftc2nc 37742	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)))
401		eqidd 2732	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))
402		fvoveq1 7364	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅)))
403		oveq1 7348	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅))
404	403	oveq1d 7356	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2))
405	404	oveq2d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2)))
406	405	fveq2d 6821	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((𝑅 / 𝑅)↑2))))
407	403, 406	oveq12d 7359	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))
408	402, 407	oveq12d 7359	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))
409	408	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
410	409	adantl 481	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
411		ubicc2 13360	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → 𝑅 ∈ (-𝑅[,]𝑅))
412	272, 273, 374, 411	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ (-𝑅[,]𝑅))
413		ovexd 7376	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V)
414	401, 410, 412, 413	fvmptd 6931	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
415	329, 335	dividd 11890	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) = 1)
416	415	fveq2d 6821	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (arcsin‘1))
417		asin1 26826	. . . . . . . . . . . . 13 ⊢ (arcsin‘1) = (π / 2)
418	416, 417	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (π / 2))
419	415	oveq1d 7356	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = (1↑2))
420		sq1 14097	. . . . . . . . . . . . . . . . . . 19 ⊢ (1↑2) = 1
421	419, 420	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = 1)
422	421	oveq2d 7357	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = (1 − 1))
423		1cnd 11102	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 1 ∈ ℂ)
424	423	subidd 11455	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − 1) = 0)
425	422, 424	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = 0)
426	425	fveq2d 6821	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = (√‘0))
427	426, 195	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0)
428	427	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0))
429	329, 329, 335	divcld 11892	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) ∈ ℂ)
430	429	mul01d 11307	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · 0) = 0)
431	428, 430	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = 0)
432	418, 431	oveq12d 7359	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) + 0))
433		2ne0 12224	. . . . . . . . . . . . . 14 ⊢ 2 ≠ 0
434	251, 375, 433	divcli 11858	. . . . . . . . . . . . 13 ⊢ (π / 2) ∈ ℂ
435	434	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (π / 2) ∈ ℂ)
436	435	addridd 11308	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) + 0) = (π / 2))
437	432, 436	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2))
438	437	oveq2d 7357	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π / 2)))
439	414, 438	eqtrd 2766	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π / 2)))
440		fvoveq1 7364	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅)))
441		oveq1 7348	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅))
442	441	oveq1d 7356	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2))
443	442	oveq2d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2)))
444	443	fveq2d 6821	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((-𝑅 / 𝑅)↑2))))
445	441, 444	oveq12d 7359	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))
446	440, 445	oveq12d 7359	. . . . . . . . . . . 12 ⊢ (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
447	446	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
448	447	oveq2d 7357	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
449		lbicc2 13359	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → -𝑅 ∈ (-𝑅[,]𝑅))
450	272, 273, 374, 449	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ (-𝑅[,]𝑅))
451		ovexd 7376	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) ∈ V)
452	401, 448, 450, 451	fvmptd 6931	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
453	329, 329, 335	divnegd 11905	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = (-𝑅 / 𝑅))
454	415	negeqd 11349	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = -1)
455	453, 454	eqtr3d 2768	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) = -1)
456	455	fveq2d 6821	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = (arcsin‘-1))
457		ax-1cn 11059	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
458		asinneg 26818	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℂ → (arcsin‘-1) = -(arcsin‘1))
459	457, 458	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (arcsin‘-1) = -(arcsin‘1)
460	417	negeqi 11348	. . . . . . . . . . . . . 14 ⊢ -(arcsin‘1) = -(π / 2)
461	459, 460	eqtri 2754	. . . . . . . . . . . . 13 ⊢ (arcsin‘-1) = -(π / 2)
462	456, 461	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = -(π / 2))
463	455	oveq1d 7356	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = (-1↑2))
464		neg1sqe1 14098	. . . . . . . . . . . . . . . . . . 19 ⊢ (-1↑2) = 1
465	463, 464	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = 1)
466	465	oveq2d 7357	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = (1 − 1))
467	466, 424	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = 0)
468	467	fveq2d 6821	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = (√‘0))
469	468, 195	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0)
470	469	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0))
471	271	recnd 11135	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℂ)
472	471, 329, 335	divcld 11892	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) ∈ ℂ)
473	472	mul01d 11307	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · 0) = 0)
474	470, 473	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = 0)
475	462, 474	oveq12d 7359	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = (-(π / 2) + 0))
476	434	negcli 11424	. . . . . . . . . . . . 13 ⊢ -(π / 2) ∈ ℂ
477	476	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → -(π / 2) ∈ ℂ)
478	477	addridd 11308	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (-(π / 2) + 0) = -(π / 2))
479	475, 478	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = -(π / 2))
480	479	oveq2d 7357	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π / 2)))
481	452, 480	eqtrd 2766	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π / 2)))
482	439, 481	oveq12d 7359	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
483	434, 434	subnegi 11435	. . . . . . . . . . 11 ⊢ ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
484		pidiv2halves 26398	. . . . . . . . . . 11 ⊢ ((π / 2) + (π / 2)) = π
485	483, 484	eqtri 2754	. . . . . . . . . 10 ⊢ ((π / 2) − -(π / 2)) = π
486	485	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) − -(π / 2)) = π)
487	486	oveq2d 7357	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = ((𝑅↑2) · π))
488	330, 435, 477	subdid 11568	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
489	251	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → π ∈ ℂ)
490	330, 489	mulcomd 11128	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · π) = (π · (𝑅↑2)))
491	487, 488, 490	3eqtr3d 2774	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))) = (π · (𝑅↑2)))
492	482, 491	eqtrd 2766	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (π · (𝑅↑2)))
493	368, 400, 492	3eqtrd 2770	. . . . 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 3015	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2)))
496	161, 238, 495	3eqtr3d 2774	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡 = (π · (𝑅↑2)))
497	156, 496	eqtrd 2766	1 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 Vcvv 3436 ∖ cdif 3894 ⊆ wss 3897 ∅c0 4278 ifcif 4470 {csn 4571 class class class wbr 5086 {copab 5148 ↦ cmpt 5167 × cxp 5609 ^◡ccnv 5610 dom cdm 5611 ran crn 5612 ↾ cres 5613 “ cima 5614 Fn wfn 6471 ⟶wf 6472 ‘cfv 6476 (class class class)co 7341 ℂcc 10999 ℝcr 11000 0cc0 11001 1c1 11002 + caddc 11004 · cmul 11006 +∞cpnf 11138 ℝ^*cxr 11140 < clt 11141 ≤ cle 11142 − cmin 11339 -cneg 11340 / cdiv 11769 2c2 12175 ℝ⁺crp 12885 (,)cioo 13240 [,]cicc 13243 ↑cexp 13963 √csqrt 15135 abscabs 15136 πcpi 15968 TopOpenctopn 17320 topGenctg 17336 ℂ_fldccnfld 21286 intcnt 22927 –cn→ccncf 24791 vol*covol 25385 volcvol 25386 𝐿¹cibl 25540 ∫citg 25541 D cdv 25786 arcsincasin 26794 areacarea 26887

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 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079 ax-addf 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-symdif 4198 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-ofr 7606 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-omul 8385 df-er 8617 df-map 8747 df-pm 8748 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-fi 9290 df-sup 9321 df-inf 9322 df-oi 9391 df-dju 9789 df-card 9827 df-acn 9830 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-z 12464 df-dec 12584 df-uz 12728 df-q 12842 df-rp 12886 df-xneg 13006 df-xadd 13007 df-xmul 13008 df-ioo 13244 df-ioc 13245 df-ico 13246 df-icc 13247 df-fz 13403 df-fzo 13550 df-fl 13691 df-mod 13769 df-seq 13904 df-exp 13964 df-fac 14176 df-bc 14205 df-hash 14233 df-shft 14969 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-limsup 15373 df-clim 15390 df-rlim 15391 df-sum 15589 df-ef 15969 df-sin 15971 df-cos 15972 df-tan 15973 df-pi 15974 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-mulr 17170 df-starv 17171 df-sca 17172 df-vsca 17173 df-ip 17174 df-tset 17175 df-ple 17176 df-ds 17178 df-unif 17179 df-hom 17180 df-cco 17181 df-rest 17321 df-topn 17322 df-0g 17340 df-gsum 17341 df-topgen 17342 df-pt 17343 df-prds 17346 df-xrs 17401 df-qtop 17406 df-imas 17407 df-xps 17409 df-mre 17483 df-mrc 17484 df-acs 17486 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19224 df-cmn 19689 df-psmet 21278 df-xmet 21279 df-met 21280 df-bl 21281 df-mopn 21282 df-fbas 21283 df-fg 21284 df-cnfld 21287 df-top 22804 df-topon 22821 df-topsp 22843 df-bases 22856 df-cld 22929 df-ntr 22930 df-cls 22931 df-nei 23008 df-lp 23046 df-perf 23047 df-cn 23137 df-cnp 23138 df-haus 23225 df-cmp 23297 df-tx 23472 df-hmeo 23665 df-fil 23756 df-fm 23848 df-flim 23849 df-flf 23850 df-xms 24230 df-ms 24231 df-tms 24232 df-cncf 24793 df-ovol 25387 df-vol 25388 df-mbf 25542 df-itg1 25543 df-itg2 25544 df-ibl 25545 df-itg 25546 df-0p 25593 df-limc 25789 df-dv 25790 df-log 26487 df-cxp 26488 df-asin 26797 df-area 26888

This theorem is referenced by: (None)

W3C validator