areacirc

Description: The area of a circle of radius R is _pi x. R ^ 2 . This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017) (Revised by Brendan Leahy, 22-Sep-2017) (Revised by Brendan Leahy, 11-Jul-2018)

		Ref	Expression
	Hypothesis	areacirc.1	$⊢ S = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\}$
	Assertion	areacirc	$⊢ (R \in ℝ \land 0 \leq R) \to area (S) = π R^{2}$

Proof

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

Metamath Proof Explorer

Theorem areacirc

Proof