areacirclem5

Description: Finding the cross-section of a circle. (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	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)$

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	1	imaeq1i	$⊢ S [\{t\}] = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} [\{t\}]$
3		vex	$⊢ t \in V$
4		imasng	$⊢ t \in V \to \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} [\{t\}] = \{u \| t \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} u\}$
5	3 4	ax-mp	$⊢ \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} [\{t\}] = \{u \| t \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} u\}$
6		df-br	$⊢ t \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} u \leftrightarrow ⟨t, u⟩ \in \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\}$
7		vex	$⊢ u \in V$
8		eleq1w	$⊢ x = t \to (x \in ℝ \leftrightarrow t \in ℝ)$
9	8	anbi1d	$⊢ x = t \to ((x \in ℝ \land y \in ℝ) \leftrightarrow (t \in ℝ \land y \in ℝ))$
10		oveq1	$⊢ x = t \to x^{2} = t^{2}$
11	10	oveq1d	$⊢ x = t \to x^{2} + y^{2} = t^{2} + y^{2}$
12	11	breq1d	$⊢ x = t \to (x^{2} + y^{2} \leq R^{2} \leftrightarrow t^{2} + y^{2} \leq R^{2})$
13	9 12	anbi12d	$⊢ x = t \to (((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2}) \leftrightarrow ((t \in ℝ \land y \in ℝ) \land t^{2} + y^{2} \leq R^{2}))$
14		eleq1w	$⊢ y = u \to (y \in ℝ \leftrightarrow u \in ℝ)$
15	14	anbi2d	$⊢ y = u \to ((t \in ℝ \land y \in ℝ) \leftrightarrow (t \in ℝ \land u \in ℝ))$
16		oveq1	$⊢ y = u \to y^{2} = u^{2}$
17	16	oveq2d	$⊢ y = u \to t^{2} + y^{2} = t^{2} + u^{2}$
18	17	breq1d	$⊢ y = u \to (t^{2} + y^{2} \leq R^{2} \leftrightarrow t^{2} + u^{2} \leq R^{2})$
19	15 18	anbi12d	$⊢ y = u \to (((t \in ℝ \land y \in ℝ) \land t^{2} + y^{2} \leq R^{2}) \leftrightarrow ((t \in ℝ \land u \in ℝ) \land t^{2} + u^{2} \leq R^{2}))$
20	3 7 13 19	opelopab	$⊢ ⟨t, u⟩ \in \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} \leftrightarrow ((t \in ℝ \land u \in ℝ) \land t^{2} + u^{2} \leq R^{2})$
21		anass	$⊢ ((t \in ℝ \land u \in ℝ) \land t^{2} + u^{2} \leq R^{2}) \leftrightarrow (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2}))$
22	6 20 21	3bitri	$⊢ t \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} u \leftrightarrow (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2}))$
23	22	abbii	$⊢ \{u \| t \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x^{2} + y^{2} \leq R^{2})\} u\} = \{u \| (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2}))\}$
24	2 5 23	3eqtri	$⊢ S [\{t\}] = \{u \| (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2}))\}$
25		simp3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to t \in ℝ$
26	25	biantrurd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to ((u \in ℝ \land t^{2} + u^{2} \leq R^{2}) \leftrightarrow (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2})))$
27	26	abbidv	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = \{u \| (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2}))\}$
28		resqcl	$⊢ R \in ℝ \to R^{2} \in ℝ$
29	28	3ad2ant1	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to R^{2} \in ℝ$
30		resqcl	$⊢ t \in ℝ \to t^{2} \in ℝ$
31	30	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to t^{2} \in ℝ$
32	29 31	resubcld	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to R^{2} - t^{2} \in ℝ$
33	32	adantr	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to R^{2} - t^{2} \in ℝ$
34		absresq	$⊢ t \in ℝ \to {\|t\|}^{2} = t^{2}$
35	34	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to {\|t\|}^{2} = t^{2}$
36	35	breq1d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to ({\|t\|}^{2} \leq R^{2} \leftrightarrow t^{2} \leq R^{2})$
37		recn	$⊢ t \in ℝ \to t \in ℂ$
38	37	abscld	$⊢ t \in ℝ \to \|t\| \in ℝ$
39	38	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to \|t\| \in ℝ$
40		simp1	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to R \in ℝ$
41	37	absge0d	$⊢ t \in ℝ \to 0 \leq \|t\|$
42	41	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to 0 \leq \|t\|$
43		simp2	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to 0 \leq R$
44	39 40 42 43	le2sqd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (\|t\| \leq R \leftrightarrow {\|t\|}^{2} \leq R^{2})$
45	29 31	subge0d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (0 \leq R^{2} - t^{2} \leftrightarrow t^{2} \leq R^{2})$
46	36 44 45	3bitr4d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (\|t\| \leq R \leftrightarrow 0 \leq R^{2} - t^{2})$
47	46	biimpa	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to 0 \leq R^{2} - t^{2}$
48	33 47	resqrtcld	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to \sqrt{R^{2} - t^{2}} \in ℝ$
49	48	renegcld	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to - \sqrt{R^{2} - t^{2}} \in ℝ$
50	49	rexrd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to - \sqrt{R^{2} - t^{2}} \in ℝ^{*}$
51	48	rexrd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to \sqrt{R^{2} - t^{2}} \in ℝ^{*}$
52		iccval	$⊢ (- \sqrt{R^{2} - t^{2}} \in ℝ^{} \land \sqrt{R^{2} - t^{2}} \in ℝ^{}) \to [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}] = \{u \in ℝ^{*} \| (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})\}$
53	50 51 52	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}}] = \{u \in ℝ^{*} \| (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})\}$
54		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}}]$
55	54	adantl	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|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}}]$
56		absresq	$⊢ u \in ℝ \to {\|u\|}^{2} = u^{2}$
57	32	recnd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to R^{2} - t^{2} \in ℂ$
58	57	adantr	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to R^{2} - t^{2} \in ℂ$
59	58	sqsqrtd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to {\sqrt{R^{2} - t^{2}}}^{2} = R^{2} - t^{2}$
60	56 59	breqan12rd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to ({\|u\|}^{2} \leq {\sqrt{R^{2} - t^{2}}}^{2} \leftrightarrow u^{2} \leq R^{2} - t^{2})$
61		recn	$⊢ u \in ℝ \to u \in ℂ$
62	61	abscld	$⊢ u \in ℝ \to \|u\| \in ℝ$
63	62	adantl	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to \|u\| \in ℝ$
64	48	adantr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to \sqrt{R^{2} - t^{2}} \in ℝ$
65	61	absge0d	$⊢ u \in ℝ \to 0 \leq \|u\|$
66	65	adantl	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to 0 \leq \|u\|$
67	33 47	sqrtge0d	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to 0 \leq \sqrt{R^{2} - t^{2}}$
68	67	adantr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to 0 \leq \sqrt{R^{2} - t^{2}}$
69	63 64 66 68	le2sqd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to (\|u\| \leq \sqrt{R^{2} - t^{2}} \leftrightarrow {\|u\|}^{2} \leq {\sqrt{R^{2} - t^{2}}}^{2})$
70	31	adantr	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land u \in ℝ) \to t^{2} \in ℝ$
71		resqcl	$⊢ u \in ℝ \to u^{2} \in ℝ$
72	71	adantl	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land u \in ℝ) \to u^{2} \in ℝ$
73	29	adantr	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land u \in ℝ) \to R^{2} \in ℝ$
74	70 72 73	leaddsub2d	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land u \in ℝ) \to (t^{2} + u^{2} \leq R^{2} \leftrightarrow u^{2} \leq R^{2} - t^{2})$
75	74	adantlr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to (t^{2} + u^{2} \leq R^{2} \leftrightarrow u^{2} \leq R^{2} - t^{2})$
76	60 69 75	3bitr4rd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to (t^{2} + u^{2} \leq R^{2} \leftrightarrow \|u\| \leq \sqrt{R^{2} - t^{2}})$
77		simpr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to u \in ℝ$
78	77 64	absled	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to (\|u\| \leq \sqrt{R^{2} - t^{2}} \leftrightarrow (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))$
79		rexr	$⊢ u \in ℝ \to u \in ℝ^{*}$
80	79	adantl	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to u \in ℝ^{*}$
81	80	biantrurd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to ((- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}) \leftrightarrow (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})))$
82	76 78 81	3bitrd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land u \in ℝ) \to (t^{2} + u^{2} \leq R^{2} \leftrightarrow (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})))$
83	82	pm5.32da	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to ((u \in ℝ \land t^{2} + u^{2} \leq R^{2}) \leftrightarrow (u \in ℝ \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))))$
84		simprl	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to u \in ℝ^{}$
85	48	adantr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to \sqrt{R^{2} - t^{2}} \in ℝ$
86		mnfxr	$⊢ −∞ \in ℝ^{*}$
87	86	a1i	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to −∞ \in ℝ^{}$
88	49	adantr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to - \sqrt{R^{2} - t^{2}} \in ℝ$
89	88	rexrd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to - \sqrt{R^{2} - t^{2}} \in ℝ^{}$
90	49	mnfltd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to −∞ < - \sqrt{R^{2} - t^{2}}$
91	90	adantr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to −∞ < - \sqrt{R^{2} - t^{2}}$
92		simprrl	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to - \sqrt{R^{2} - t^{2}} \leq u$
93	87 89 84 91 92	xrltletrd	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to −∞ < u$
94		simprrr	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to u \leq \sqrt{R^{2} - t^{2}}$
95		xrre	$⊢ ((u \in ℝ^{*} \land \sqrt{R^{2} - t^{2}} \in ℝ) \land (−∞ < u \land u \leq \sqrt{R^{2} - t^{2}})) \to u \in ℝ$
96	84 85 93 94 95	syl22anc	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \land (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))) \to u \in ℝ$
97	96	ex	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to ((u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})) \to u \in ℝ)$
98	97	pm4.71rd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to ((u \in ℝ^{} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})) \leftrightarrow (u \in ℝ \land (u \in ℝ^{} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))))$
99	83 98	bitr4d	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to ((u \in ℝ \land t^{2} + u^{2} \leq R^{2}) \leftrightarrow (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})))$
100	99	abbidv	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = \{u \| (u \in ℝ^{*} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))\}$
101		df-rab	$⊢ \{u \in ℝ^{} \| (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})\} = \{u \| (u \in ℝ^{} \land (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}}))\}$
102	100 101	eqtr4di	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = \{u \in ℝ^{*} \| (- \sqrt{R^{2} - t^{2}} \leq u \land u \leq \sqrt{R^{2} - t^{2}})\}$
103	53 55 102	3eqtr4rd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \|t\| \leq R) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = if (\|t\| \leq R, [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}], \emptyset)$
104	40 39	ltnled	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (R < \|t\| \leftrightarrow \neg \|t\| \leq R)$
105	104	biimprd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (\neg \|t\| \leq R \to R < \|t\|)$
106	105	imdistani	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \neg \|t\| \leq R) \to ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\|)$
107		df-rab	$⊢ \{u \in ℝ \| t^{2} + u^{2} \leq R^{2}\} = \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\}$
108	29	3ad2ant1	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to R^{2} \in ℝ$
109	31	3ad2ant1	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to t^{2} \in ℝ$
110	71	3ad2ant3	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to u^{2} \in ℝ$
111	109 110	readdcld	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to t^{2} + u^{2} \in ℝ$
112	40 39 43 42	lt2sqd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (R < \|t\| \leftrightarrow R^{2} < {\|t\|}^{2})$
113	35	breq2d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (R^{2} < {\|t\|}^{2} \leftrightarrow R^{2} < t^{2})$
114	112 113	bitrd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (R < \|t\| \leftrightarrow R^{2} < t^{2})$
115	114	biimpa	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\|) \to R^{2} < t^{2}$
116	115	3adant3	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to R^{2} < t^{2}$
117		sqge0	$⊢ u \in ℝ \to 0 \leq u^{2}$
118	117	3ad2ant3	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to 0 \leq u^{2}$
119	109 110	addge01d	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to (0 \leq u^{2} \leftrightarrow t^{2} \leq t^{2} + u^{2})$
120	118 119	mpbid	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to t^{2} \leq t^{2} + u^{2}$
121	108 109 111 116 120	ltletrd	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to R^{2} < t^{2} + u^{2}$
122	108 111	ltnled	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to (R^{2} < t^{2} + u^{2} \leftrightarrow \neg t^{2} + u^{2} \leq R^{2})$
123	121 122	mpbid	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\| \land u \in ℝ) \to \neg t^{2} + u^{2} \leq R^{2}$
124	123	3expa	$⊢ (((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\|) \land u \in ℝ) \to \neg t^{2} + u^{2} \leq R^{2}$
125	124	ralrimiva	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\|) \to \forall u \in ℝ \neg t^{2} + u^{2} \leq R^{2}$
126		rabeq0	$⊢ \{u \in ℝ \| t^{2} + u^{2} \leq R^{2}\} = \emptyset \leftrightarrow \forall u \in ℝ \neg t^{2} + u^{2} \leq R^{2}$
127	125 126	sylibr	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\|) \to \{u \in ℝ \| t^{2} + u^{2} \leq R^{2}\} = \emptyset$
128	107 127	eqtr3id	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land R < \|t\|) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = \emptyset$
129	106 128	syl	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \neg \|t\| \leq R) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = \emptyset$
130		iffalse	$⊢ \neg \|t\| \leq R \to if (\|t\| \leq R, [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}], \emptyset) = \emptyset$
131	130	adantl	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \neg \|t\| \leq R) \to if (\|t\| \leq R, [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}], \emptyset) = \emptyset$
132	129 131	eqtr4d	$⊢ ((R \in ℝ \land 0 \leq R \land t \in ℝ) \land \neg \|t\| \leq R) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = if (\|t\| \leq R, [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}], \emptyset)$
133	103 132	pm2.61dan	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to \{u \| (u \in ℝ \land t^{2} + u^{2} \leq R^{2})\} = if (\|t\| \leq R, [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}], \emptyset)$
134	27 133	eqtr3d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to \{u \| (t \in ℝ \land (u \in ℝ \land t^{2} + u^{2} \leq R^{2}))\} = if (\|t\| \leq R, [- \sqrt{R^{2} - t^{2}}, \sqrt{R^{2} - t^{2}}], \emptyset)$
135	24 134	syl5eq	$⊢ (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)$

Metamath Proof Explorer

Theorem areacirclem5

Proof