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 37427

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 5766	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ × ℝ)
3	1, 2	eqsstri 4013	. . . . 5 ⊢ 𝑆 ⊆ (ℝ × ℝ)
4	3	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ⊆ (ℝ × ℝ))
5	1	areacirclem5 37426	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
6		resqcl 14137	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
7	6	3ad2ant1 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
8		resqcl 14137	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
9	8	3ad2ant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
10	7, 9	resubcld 11683	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
11	10	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
12		absresq 15302	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
13	12	3ad2ant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
14	13	breq1d 5155	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
15		recn 11239	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
16	15	abscld 15436	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
17	16	3ad2ant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
18		simp1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
19	15	absge0d 15444	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
20	19	3ad2ant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
21		simp2 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
22	17, 18, 20, 21	le2sqd 14269	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
23	7, 9	subge0d 11845	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
24	14, 22, 23	3bitr4d 310	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
25	24	biimpa 475	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
26	11, 25	resqrtcld 15417	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
27	26	renegcld 11682	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
28		iccmbl 25583	. . . . . . . . . 10 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
29	27, 26, 28	syl2anc 582	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol)
30		mblvol 25547	. . . . . . . . . . . 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 15420	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
33	26, 26, 32, 32	addge0d 11831	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
34		recn 11239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
35	34	sqcld 14157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
36	35	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
37	15	sqcld 14157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
38	37	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
39	36, 38	subcld 11612	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
40	39	sqrtcld 15437	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
41	40	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
42	41, 41	subnegd 11619	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
43	42	breq2d 5157	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
44	26, 27	subge0d 11845	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
45	43, 44	bitr3d 280	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
46	33, 45	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
47		ovolicc 25540	. . . . . . . . . . . 12 ⊢ ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
48	27, 26, 46, 47	syl3anc 1368	. . . . . . . . . . 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 11683	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈ ℝ)
51	49, 50	eqeltrd 2826	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈ ℝ)
52		volf 25546	. . . . . . . . . 10 ⊢ vol:dom vol⟶(0[,]+∞)
53		ffn 6720	. . . . . . . . . 10 ⊢ (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
54		elpreima 7063	. . . . . . . . . 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 581	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (^◡vol “ ℝ))
57		0mbl 25556	. . . . . . . . . 10 ⊢ ∅ ∈ dom vol
58		mblvol 25547	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
59	57, 58	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
60		ovol0 25510	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
61	59, 60	eqtri 2754	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
62		0re 11257	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
63	61, 62	eqeltri 2822	. . . . . . . . . 10 ⊢ (vol‘∅) ∈ ℝ
64		elpreima 7063	. . . . . . . . . . 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 4558	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈ (^◡vol “ ℝ))
69	5, 68	eqeltrd 2826	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
70	69	3expa 1115	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
71	70	ralrimiva 3136	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ))
72	5	fveq2d 6897	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
73	72	3expa 1115	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
74	73	mpteq2dva 5245	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) = (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))))
75		renegcl 11564	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
76	75	adantr 479	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → -𝑅 ∈ ℝ)
77		simpl 481	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑅 ∈ ℝ)
78		iccssre 13454	. . . . . . 7 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
79	76, 77, 78	syl2anc 582	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅[,]𝑅) ⊆ ℝ)
80		rembl 25557	. . . . . . 7 ⊢ ℝ ∈ dom vol
81	80	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ℝ ∈ dom vol)
82		fvexd 6908	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈ V)
83		eldif 3956	. . . . . . . . 9 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)))
84		3anass 1092	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
85	84	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
86	75	3ad2ant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → -𝑅 ∈ ℝ)
87		elicc2 13437	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
88	86, 18, 87	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89		simp3 1135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
90	89, 18	absled 15430	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
91	89	biantrurd 531	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
92	90, 91	bitrd 278	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))))
93	85, 88, 92	3bitr4rd 311	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 𝑡 ∈ (-𝑅[,]𝑅)))
94	93	biimpd 228	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 → 𝑡 ∈ (-𝑅[,]𝑅)))
95	94	con3d 152	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅))
96	95	3expia 1118	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅)))
97	96	impd 409	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
98	83, 97	biimtrid 241	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅))
99	98	imp 405	. . . . . . 7 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → ¬ (abs‘𝑡) ≤ 𝑅)
100		iffalse 4532	. . . . . . . . 9 ⊢ (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
101	100	fveq2d 6897	. . . . . . . 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 582	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
105	90	biimprd 247	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅))
106	105	expd 414	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅)))
107	106	3expia 1118	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅))))
108	107	3impd 1345	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅))
109	104, 108	sylbid 239	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → (abs‘𝑡) ≤ 𝑅))
110	109	3impia 1114	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (abs‘𝑡) ≤ 𝑅)
111		iftrue 4529	. . . . . . . . . . . 12 ⊢ ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
112	111	fveq2d 6897	. . . . . . . . . . 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 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
115	75, 78	mpancom 686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
116	115	sselda 3978	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
117	116	3adant2 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
118	117	resqcld 14138	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
119	114, 118	resubcld 11683	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
120	75, 87	mpancom 686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
121	120	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
122	22, 90, 14	3bitr3rd 309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ (𝑅↑2) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
123	23, 122	bitrd 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
124	123	biimprd 247	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
125	124	expd 414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2)))))
126	125	3expia 1118	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
127	126	3impd 1345	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
128	121, 127	sylbid 239	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
129	128	3impia 1114	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
130	119, 129	resqrtcld 15417	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
131	130	renegcld 11682	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
132	131, 130, 28	syl2anc 582	. . . . . . . . . . 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 11283	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
135	134	sqrtcld 15437	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
136	135, 135	subnegd 11619	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
137	119, 129	sqrtge0d 15420	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
138	130, 130, 137, 137	addge0d 11831	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
139	136	breq2d 5157	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
140	130, 131	subge0d 11845	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
141	139, 140	bitr3d 280	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
142	138, 141	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
143	131, 130, 142, 47	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))))
144	135	2timesd 12501	. . . . . . . . . . 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 1115	. . . . . . . 8 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
148	147	mpteq2dva 5245	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))
149		areacirclem3 37424	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿¹)
150	148, 149	eqeltrd 2826	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
151	79, 81, 82, 103, 150	iblss2 25823	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈ 𝐿¹)
152	74, 151	eqeltrd 2826	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹)
153		dmarea 26982	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (^◡vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑡}))) ∈ 𝐿¹))
154	4, 71, 152, 153	syl3anbrc 1340	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 𝑆 ∈ dom area)
155		areaval 26989	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
156	154, 155	syl 17	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
157		elioore 13402	. . . . . 6 ⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ)
158	5	3expa 1115	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
159	157, 158	sylan2 591	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
160	159	fveq2d 6897	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
161	160	itgeq2dv 25799	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡)
162		ioossre 13433	. . . . 5 ⊢ (-𝑅(,)𝑅) ⊆ ℝ
163	162	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ ℝ)
164		eldif 3956	. . . . . 6 ⊢ (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)))
165	75	rexrd 11305	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ^*)
166		rexr 11301	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℝ^*)
167		elioo2 13413	. . . . . . . . . . . . . 14 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
168	165, 166, 167	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
169	168	3ad2ant1 1130	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
170	89	biantrurd 531	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
171	89, 18	absltd 15429	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
172		3anass 1092	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
173	172	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))))
174	170, 171, 173	3bitr4rd 311	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (abs‘𝑡) < 𝑅))
175	169, 174	bitrd 278	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (abs‘𝑡) < 𝑅))
176	175	notbid 317	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ ¬ (abs‘𝑡) < 𝑅))
177	18, 17	lenltd 11401	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) ↔ ¬ (abs‘𝑡) < 𝑅))
178	176, 177	bitr4d 281	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ 𝑅 ≤ (abs‘𝑡)))
179	5	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
180	179	fveq2d 6897	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)))
181	17	anim1i 613	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅))
182		eqle 11357	. . . . . . . . . . . . . . . 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 7423	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘𝑡) = 𝑅 → ((abs‘𝑡)↑2) = (𝑅↑2))
185	184	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑅↑2))
186	13	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑡↑2))
187	185, 186	eqtr3d 2768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2))
188		fvoveq1 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑡↑2) − (𝑡↑2))))
189	188	negeqd 11495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) = -(√‘((𝑡↑2) − (𝑡↑2))))
190	189, 188	oveq12d 7434	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))))
191	8	recnd 11283	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℂ)
192	191	subidd 11600	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0)
193	192	fveq2d 6897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (√‘((𝑡↑2) − (𝑡↑2))) = (√‘0))
194	193	negeqd 11495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → -(√‘((𝑡↑2) − (𝑡↑2))) = -(√‘0))
195		sqrt0 15241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (√‘0) = 0
196	195	negeqi 11494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -(√‘0) = -0
197		neg0 11547	. . . . . . . . . . . . . . . . . . . . . . 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 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℝ → (-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) = (0[,]0))
202	201	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . 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 6897	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (vol‘(0[,]0)))
205		iccmbl 25583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom vol)
206	62, 62, 205	mp2an 690	. . . . . . . . . . . . . . . . . . 19 ⊢ (0[,]0) ∈ dom vol
207		mblvol 25547	. . . . . . . . . . . . . . . . . . 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 11302	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℝ^*
210		iccid 13417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℝ^* → (0[,]0) = {0})
211	210	fveq2d 6897	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ^* → (vol‘(0[,]0)) = (vol‘{0}))
212	209, 211	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol‘(0[,]0)) = (vol‘{0})
213		ovolsn 25512	. . . . . . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
221	220	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
222	18, 17	ltnled 11402	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
223	222	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
224		simpl1 1188	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ∈ ℝ)
225	17	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (abs‘𝑡) ∈ ℝ)
226		simpr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ≤ (abs‘𝑡))
227	224, 225, 226	leltned 11408	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ (abs‘𝑡) ≠ 𝑅))
228	223, 227	bitr3d 280	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (¬ (abs‘𝑡) ≤ 𝑅 ↔ (abs‘𝑡) ≠ 𝑅))
229	228, 102	biimtrrdi 253	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) ≠ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0))
230	221, 229	pm2.61dne 3018	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = 0)
231	180, 230	eqtrd 2766	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = 0)
232	231	ex 411	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) → (vol‘(𝑆 “ {𝑡})) = 0))
233	178, 232	sylbid 239	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0))
234	233	3expia 1118	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0)))
235	234	impd 409	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
236	164, 235	biimtrid 241	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0))
237	236	imp 405	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅))) → (vol‘(𝑆 “ {𝑡})) = 0)
238	163, 237	itgss 25829	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡)
239		negeq 11493	. . . . . . . . . 10 ⊢ (𝑅 = 0 → -𝑅 = -0)
240	239, 197	eqtrdi 2782	. . . . . . . . 9 ⊢ (𝑅 = 0 → -𝑅 = 0)
241		id 22	. . . . . . . . 9 ⊢ (𝑅 = 0 → 𝑅 = 0)
242	240, 241	oveq12d 7434	. . . . . . . 8 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0))
243		iooid 13400	. . . . . . . 8 ⊢ (0(,)0) = ∅
244	242, 243	eqtrdi 2782	. . . . . . 7 ⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = ∅)
245	244	adantl 480	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅)
246		itgeq1 25790	. . . . . 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 25797	. . . . . 6 ⊢ ∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0
249		sq0 14204	. . . . . . . . . 10 ⊢ (0↑2) = 0
250	249	oveq2i 7427	. . . . . . . . 9 ⊢ (π · (0↑2)) = (π · 0)
251		picn 26484	. . . . . . . . . 10 ⊢ π ∈ ℂ
252	251	mul01i 11445	. . . . . . . . 9 ⊢ (π · 0) = 0
253	250, 252	eqtr2i 2755	. . . . . . . 8 ⊢ 0 = (π · (0↑2))
254		oveq1 7423	. . . . . . . . 9 ⊢ (𝑅 = 0 → (𝑅↑2) = (0↑2))
255	254	oveq2d 7432	. . . . . . . 8 ⊢ (𝑅 = 0 → (π · (𝑅↑2)) = (π · (0↑2)))
256	253, 255	eqtr4id 2785	. . . . . . 7 ⊢ (𝑅 = 0 → 0 = (π · (𝑅↑2)))
257	256	adantl 480	. . . . . 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 1133	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ)
261		0red 11258	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ∈ ℝ)
262		simpr 483	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ 𝑅)
263	261, 77, 262	leltned 11408	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0 < 𝑅 ↔ 𝑅 ≠ 0))
264	263	biimp3ar 1467	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 0 < 𝑅)
265	260, 264	elrpd 13061	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ⁺)
266	265	3expa 1115	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ⁺)
267	157, 16	syl 17	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) ∈ ℝ)
268	267	adantl 480	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ∈ ℝ)
269		rpre 13030	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
270	269	adantr 479	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ)
271	269	renegcld 11682	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
272	271	rexrd 11305	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ^*)
273		rpxr 13031	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^*)
274	272, 273, 167	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
275		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
276	269	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
277	275, 276	absltd 15429	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
278	277	biimprd 247	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
279	278	exp4b 429	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → (abs‘𝑡) < 𝑅))))
280	279	3impd 1345	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅))
281	274, 280	sylbid 239	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) < 𝑅))
282	281	imp 405	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) < 𝑅)
283	268, 270, 282	ltled 11403	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅)
284	283, 112	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))))
285	269	resqcld 14138	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
286	285	recnd 11283	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
287	286	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ)
288	191	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ)
289	287, 288	subcld 11612	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
290	289	sqrtcld 15437	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
291	290, 290	subnegd 11619	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
292	157, 291	sylan2 591	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
293	285	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
294	8	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
295	293, 294	resubcld 11683	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
296	157, 295	sylan2 591	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
297		0red 11258	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ)
298	16	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
299	19	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
300		rpge0 13035	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
301	300	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
302	298, 276, 299, 301	lt2sqd 14268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2)))
303	12	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
304	303	breq1d 5155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2)))
305	302, 277, 304	3bitr3rd 309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))
306	294, 293	posdifd 11842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) < (𝑅↑2) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
307	305, 306	bitr3d 280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < ((𝑅↑2) − (𝑡↑2))))
308	307	biimpd 228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
309	308	exp4b 429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < ((𝑅↑2) − (𝑡↑2))))))
310	309	3impd 1345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
311	274, 310	sylbid 239	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅(,)𝑅) → 0 < ((𝑅↑2) − (𝑡↑2))))
312	311	imp 405	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < ((𝑅↑2) − (𝑡↑2)))
313	297, 296, 312	ltled 11403	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
314	296, 313	resqrtcld 15417	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
315	314	renegcld 11682	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
316	315, 314, 28	syl2anc 582	. . . . . . . . . . 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 15420	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
319	314, 314, 318, 318	addge0d 11831	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))
320	292	breq2d 5157	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))))
321	314, 315	subge0d 11845	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
322	320, 321	bitr3d 280	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))) ↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
323	319, 322	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))
324	315, 314, 323, 47	syl3anc 1368	. . . . . . . . . 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 11206	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
327	326	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ℝ ⊆ ℂ)
328	271, 269, 78	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
329		rpcn 13032	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
330	329	sqcld 14157	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
331	330	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
332	328	sselda 3978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ)
333	332	recnd 11283	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ)
334	329	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
335		rpne0 13038	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
336	335	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
337	333, 334, 336	divcld 12035	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ)
338		asincl 26898	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
339	337, 338	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ)
340		1cnd 11250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
341	337	sqcld 14157	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ)
342	340, 341	subcld 11612	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ)
343	342	sqrtcld 15437	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ)
344	337, 343	mulcld 11275	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈ ℂ)
345	339, 344	addcld 11274	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈ ℂ)
346	331, 345	mulcld 11275	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈ ℂ)
347		eqid 2726	. . . . . . . . . . . . . . 15 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
348	347	tgioo2 24807	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
349		iccntr 24825	. . . . . . . . . . . . . . 15 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
350	271, 269, 349	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅))
351	327, 328, 346, 348, 347, 350	dvmptntr 25991	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))))
352		areacirclem1 37422	. . . . . . . . . . . . 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 479	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))))
355		oveq1 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2))
356	355	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2)))
357	356	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
358	357	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
359	358	adantl 480	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
360		simpr 483	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅))
361		ovexd 7451	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V)
362	354, 359, 360, 361	fvmptd 7008	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2)))))
363	157, 290	sylan2 591	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
364	363	2timesd 12501	. . . . . . . . . 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 25799	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡)
369	269, 269, 300, 300	addge0d 11831	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅 + 𝑅))
370	329, 329	subnegd 11619	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 − -𝑅) = (𝑅 + 𝑅))
371	370	breq2d 5157	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ 0 ≤ (𝑅 + 𝑅)))
372	269, 271	subge0d 11845	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 − -𝑅) ↔ -𝑅 ≤ 𝑅))
373	371, 372	bitr3d 280	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (0 ≤ (𝑅 + 𝑅) ↔ -𝑅 ≤ 𝑅))
374	369, 373	mpbid 231	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ≤ 𝑅)
375		2cn 12333	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
376	162, 326	sstri 3988	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ ℂ
377		ssid 4001	. . . . . . . . . . 11 ⊢ ℂ ⊆ ℂ
378	375, 376, 377	3pm3.2i 1336	. . . . . . . . . 10 ⊢ (2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ)
379		cncfmptc 24920	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
380	378, 379	mp1i 13	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
381		ioossicc 13458	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)
382		resmpt 6038	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))))
383	381, 382	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))
384		areacirclem2 37423	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
385	269, 300, 384	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
386		rescncf 24905	. . . . . . . . . . 11 ⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)))
387	381, 385, 386	mpsyl 68	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
388	383, 387	eqeltrrid 2831	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
389	380, 388	mulcncf 25462	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
390	353, 389	eqeltrd 2826	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ))
391	381	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅))
392		ioombl 25582	. . . . . . . . . . 11 ⊢ (-𝑅(,)𝑅) ∈ dom vol
393	392	a1i 11	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (-𝑅(,)𝑅) ∈ dom vol)
394		ovexd 7451	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V)
395		areacirclem3 37424	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
396	391, 393, 394, 395	iblss 25822	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
397	269, 300, 396	syl2anc 582	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ 𝐿¹)
398	353, 397	eqeltrd 2826	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ 𝐿¹)
399		areacirclem4 37425	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
400	271, 269, 374, 390, 398, 399	ftc2nc 37416	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)))
401		eqidd 2727	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))
402		fvoveq1 7439	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅)))
403		oveq1 7423	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅))
404	403	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2))
405	404	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2)))
406	405	fveq2d 6897	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((𝑅 / 𝑅)↑2))))
407	403, 406	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))
408	402, 407	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))
409	408	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
410	409	adantl 480	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
411		ubicc2 13490	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → 𝑅 ∈ (-𝑅[,]𝑅))
412	272, 273, 374, 411	syl3anc 1368	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ (-𝑅[,]𝑅))
413		ovexd 7451	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V)
414	401, 410, 412, 413	fvmptd 7008	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))))
415	329, 335	dividd 12033	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) = 1)
416	415	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (arcsin‘1))
417		asin1 26919	. . . . . . . . . . . . 13 ⊢ (arcsin‘1) = (π / 2)
418	416, 417	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(𝑅 / 𝑅)) = (π / 2))
419	415	oveq1d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = (1↑2))
420		sq1 14207	. . . . . . . . . . . . . . . . . . 19 ⊢ (1↑2) = 1
421	419, 420	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅)↑2) = 1)
422	421	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = (1 − 1))
423		1cnd 11250	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 1 ∈ ℂ)
424	423	subidd 11600	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − 1) = 0)
425	422, 424	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((𝑅 / 𝑅)↑2)) = 0)
426	425	fveq2d 6897	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = (√‘0))
427	426, 195	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0)
428	427	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0))
429	329, 329, 335	divcld 12035	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅 / 𝑅) ∈ ℂ)
430	429	mul01d 11454	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · 0) = 0)
431	428, 430	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))) = 0)
432	418, 431	oveq12d 7434	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) + 0))
433		2ne0 12362	. . . . . . . . . . . . . 14 ⊢ 2 ≠ 0
434	251, 375, 433	divcli 12001	. . . . . . . . . . . . 13 ⊢ (π / 2) ∈ ℂ
435	434	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (π / 2) ∈ ℂ)
436	435	addridd 11455	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) + 0) = (π / 2))
437	432, 436	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2))
438	437	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π / 2)))
439	414, 438	eqtrd 2766	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π / 2)))
440		fvoveq1 7439	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅)))
441		oveq1 7423	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅))
442	441	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2))
443	442	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2)))
444	443	fveq2d 6897	. . . . . . . . . . . . . 14 ⊢ (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 − ((-𝑅 / 𝑅)↑2))))
445	441, 444	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))
446	440, 445	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
447	446	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))))
448	447	oveq2d 7432	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
449		lbicc2 13489	. . . . . . . . . . 11 ⊢ ((-𝑅 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ -𝑅 ≤ 𝑅) → -𝑅 ∈ (-𝑅[,]𝑅))
450	272, 273, 374, 449	syl3anc 1368	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ (-𝑅[,]𝑅))
451		ovexd 7451	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) ∈ V)
452	401, 448, 450, 451	fvmptd 7008	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))))
453	329, 329, 335	divnegd 12048	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = (-𝑅 / 𝑅))
454	415	negeqd 11495	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -(𝑅 / 𝑅) = -1)
455	453, 454	eqtr3d 2768	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) = -1)
456	455	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = (arcsin‘-1))
457		ax-1cn 11207	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
458		asinneg 26911	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℂ → (arcsin‘-1) = -(arcsin‘1))
459	457, 458	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (arcsin‘-1) = -(arcsin‘1)
460	417	negeqi 11494	. . . . . . . . . . . . . 14 ⊢ -(arcsin‘1) = -(π / 2)
461	459, 460	eqtri 2754	. . . . . . . . . . . . 13 ⊢ (arcsin‘-1) = -(π / 2)
462	456, 461	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (arcsin‘(-𝑅 / 𝑅)) = -(π / 2))
463	455	oveq1d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = (-1↑2))
464		neg1sqe1 14208	. . . . . . . . . . . . . . . . . . 19 ⊢ (-1↑2) = 1
465	463, 464	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅)↑2) = 1)
466	465	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = (1 − 1))
467	466, 424	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 − ((-𝑅 / 𝑅)↑2)) = 0)
468	467	fveq2d 6897	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = (√‘0))
469	468, 195	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0)
470	469	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0))
471	271	recnd 11283	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℂ)
472	471, 329, 335	divcld 12035	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅 / 𝑅) ∈ ℂ)
473	472	mul01d 11454	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · 0) = 0)
474	470, 473	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))) = 0)
475	462, 474	oveq12d 7434	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = (-(π / 2) + 0))
476	434	negcli 11569	. . . . . . . . . . . . 13 ⊢ -(π / 2) ∈ ℂ
477	476	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → -(π / 2) ∈ ℂ)
478	477	addridd 11455	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (-(π / 2) + 0) = -(π / 2))
479	475, 478	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2))))) = -(π / 2))
480	479	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 − ((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π / 2)))
481	452, 480	eqtrd 2766	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π / 2)))
482	439, 481	oveq12d 7434	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
483	434, 434	subnegi 11580	. . . . . . . . . . 11 ⊢ ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
484		pidiv2halves 26492	. . . . . . . . . . 11 ⊢ ((π / 2) + (π / 2)) = π
485	483, 484	eqtri 2754	. . . . . . . . . 10 ⊢ ((π / 2) − -(π / 2)) = π
486	485	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((π / 2) − -(π / 2)) = π)
487	486	oveq2d 7432	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = ((𝑅↑2) · π))
488	330, 435, 477	subdid 11711	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · ((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) − ((𝑅↑2) · -(π / 2))))
489	251	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → π ∈ ℂ)
490	330, 489	mulcomd 11276	. . . . . . . 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 3019	. . 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 205 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ≠ wne 2930 ∀wral 3051 Vcvv 3462 ∖ cdif 3943 ⊆ wss 3946 ∅c0 4322 ifcif 4523 {csn 4623 class class class wbr 5145 {copab 5207 ↦ cmpt 5228 × cxp 5672 ^◡ccnv 5673 dom cdm 5674 ran crn 5675 ↾ cres 5676 “ cima 5677 Fn wfn 6541 ⟶wf 6542 ‘cfv 6546 (class class class)co 7416 ℂcc 11147 ℝcr 11148 0cc0 11149 1c1 11150 + caddc 11152 · cmul 11154 +∞cpnf 11286 ℝ^*cxr 11288 < clt 11289 ≤ cle 11290 − cmin 11485 -cneg 11486 / cdiv 11912 2c2 12313 ℝ⁺crp 13022 (,)cioo 13372 [,]cicc 13375 ↑cexp 14075 √csqrt 15233 abscabs 15234 πcpi 16063 TopOpenctopn 17431 topGenctg 17447 ℂ_fldccnfld 21339 intcnt 23009 –cn→ccncf 24884 vol*covol 25479 volcvol 25480 𝐿¹cibl 25634 ∫citg 25635 D cdv 25880 arcsincasin 26887 areacarea 26980

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5282 ax-sep 5296 ax-nul 5303 ax-pow 5361 ax-pr 5425 ax-un 7738 ax-inf2 9677 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226 ax-pre-sup 11227 ax-addf 11228

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3966 df-symdif 4241 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4906 df-int 4947 df-iun 4995 df-iin 4996 df-disj 5111 df-br 5146 df-opab 5208 df-mpt 5229 df-tr 5263 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-se 5630 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-pred 6304 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6498 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-isom 6555 df-riota 7372 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7682 df-ofr 7683 df-om 7869 df-1st 7995 df-2nd 7996 df-supp 8167 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-oadd 8492 df-omul 8493 df-er 8726 df-map 8849 df-pm 8850 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9399 df-fi 9447 df-sup 9478 df-inf 9479 df-oi 9546 df-dju 9937 df-card 9975 df-acn 9978 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11487 df-neg 11488 df-div 11913 df-nn 12259 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12519 df-z 12605 df-dec 12724 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13140 df-xadd 13141 df-xmul 13142 df-ioo 13376 df-ioc 13377 df-ico 13378 df-icc 13379 df-fz 13533 df-fzo 13676 df-fl 13806 df-mod 13884 df-seq 14016 df-exp 14076 df-fac 14286 df-bc 14315 df-hash 14343 df-shft 15067 df-cj 15099 df-re 15100 df-im 15101 df-sqrt 15235 df-abs 15236 df-limsup 15468 df-clim 15485 df-rlim 15486 df-sum 15686 df-ef 16064 df-sin 16066 df-cos 16067 df-tan 16068 df-pi 16069 df-struct 17144 df-sets 17161 df-slot 17179 df-ndx 17191 df-base 17209 df-ress 17238 df-plusg 17274 df-mulr 17275 df-starv 17276 df-sca 17277 df-vsca 17278 df-ip 17279 df-tset 17280 df-ple 17281 df-ds 17283 df-unif 17284 df-hom 17285 df-cco 17286 df-rest 17432 df-topn 17433 df-0g 17451 df-gsum 17452 df-topgen 17453 df-pt 17454 df-prds 17457 df-xrs 17512 df-qtop 17517 df-imas 17518 df-xps 17520 df-mre 17594 df-mrc 17595 df-acs 17597 df-mgm 18628 df-sgrp 18707 df-mnd 18723 df-submnd 18769 df-mulg 19058 df-cntz 19307 df-cmn 19776 df-psmet 21331 df-xmet 21332 df-met 21333 df-bl 21334 df-mopn 21335 df-fbas 21336 df-fg 21337 df-cnfld 21340 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22937 df-cld 23011 df-ntr 23012 df-cls 23013 df-nei 23090 df-lp 23128 df-perf 23129 df-cn 23219 df-cnp 23220 df-haus 23307 df-cmp 23379 df-tx 23554 df-hmeo 23747 df-fil 23838 df-fm 23930 df-flim 23931 df-flf 23932 df-xms 24314 df-ms 24315 df-tms 24316 df-cncf 24886 df-ovol 25481 df-vol 25482 df-mbf 25636 df-itg1 25637 df-itg2 25638 df-ibl 25639 df-itg 25640 df-0p 25687 df-limc 25883 df-dv 25884 df-log 26580 df-cxp 26581 df-asin 26890 df-area 26981

This theorem is referenced by: (None)

W3C validator