areacirclem2

Description: Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

		Ref	Expression
	Assertion	areacirclem2	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		resqcl	$⊢ R \in ℝ \to R^{2} \in ℝ$
2	1	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to R^{2} \in ℝ$
3	2	adantr	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R]) \to R^{2} \in ℝ$
4		renegcl	$⊢ R \in ℝ \to - R \in ℝ$
5		iccssre	$⊢ (- R \in ℝ \land R \in ℝ) \to [- R, R] \subseteq ℝ$
6	4 5	mpancom	$⊢ R \in ℝ \to [- R, R] \subseteq ℝ$
7	6	sselda	$⊢ (R \in ℝ \land t \in [- R, R]) \to t \in ℝ$
8	7	resqcld	$⊢ (R \in ℝ \land t \in [- R, R]) \to t^{2} \in ℝ$
9	8	adantlr	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R]) \to t^{2} \in ℝ$
10	3 9	resubcld	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R]) \to R^{2} - t^{2} \in ℝ$
11		elicc2	$⊢ (- R \in ℝ \land R \in ℝ) \to (t \in [- R, R] \leftrightarrow (t \in ℝ \land - R \leq t \land t \leq R))$
12	4 11	mpancom	$⊢ R \in ℝ \to (t \in [- R, R] \leftrightarrow (t \in ℝ \land - R \leq t \land t \leq R))$
13	12	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] \leftrightarrow (t \in ℝ \land - R \leq t \land t \leq R))$
14	1	3ad2ant1	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to R^{2} \in ℝ$
15		resqcl	$⊢ t \in ℝ \to t^{2} \in ℝ$
16	15	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to t^{2} \in ℝ$
17	14 16	subge0d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (0 \leq R^{2} - t^{2} \leftrightarrow t^{2} \leq R^{2})$
18		absresq	$⊢ t \in ℝ \to {\|t\|}^{2} = t^{2}$
19	18	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to {\|t\|}^{2} = t^{2}$
20	19	breq1d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to ({\|t\|}^{2} \leq R^{2} \leftrightarrow t^{2} \leq R^{2})$
21	17 20	bitr4d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (0 \leq R^{2} - t^{2} \leftrightarrow {\|t\|}^{2} \leq R^{2})$
22		recn	$⊢ t \in ℝ \to t \in ℂ$
23	22	abscld	$⊢ t \in ℝ \to \|t\| \in ℝ$
24	23	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to \|t\| \in ℝ$
25		simp1	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to R \in ℝ$
26	22	absge0d	$⊢ t \in ℝ \to 0 \leq \|t\|$
27	26	3ad2ant3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to 0 \leq \|t\|$
28		simp2	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to 0 \leq R$
29	24 25 27 28	le2sqd	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (\|t\| \leq R \leftrightarrow {\|t\|}^{2} \leq R^{2})$
30		simp3	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to t \in ℝ$
31	30 25	absled	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (\|t\| \leq R \leftrightarrow (- R \leq t \land t \leq R))$
32	21 29 31	3bitr2d	$⊢ (R \in ℝ \land 0 \leq R \land t \in ℝ) \to (0 \leq R^{2} - t^{2} \leftrightarrow (- R \leq t \land t \leq R))$
33	32	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})$
34	33	3expa	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in ℝ) \to ((- R \leq t \land t \leq R) \to 0 \leq R^{2} - t^{2})$
35	34	exp4b	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in ℝ \to (- R \leq t \to (t \leq R \to 0 \leq R^{2} - t^{2})))$
36	35	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})$
37	13 36	sylbid	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] \to 0 \leq R^{2} - t^{2})$
38	37	imp	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R]) \to 0 \leq R^{2} - t^{2}$
39		elrege0	$⊢ R^{2} - t^{2} \in [0, +∞) \leftrightarrow (R^{2} - t^{2} \in ℝ \land 0 \leq R^{2} - t^{2})$
40	10 38 39	sylanbrc	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R]) \to R^{2} - t^{2} \in [0, +∞)$
41		fvres	$⊢ R^{2} - t^{2} \in [0, +∞) \to ({\sqrt ↾}_{[0, +∞)}) (R^{2} - t^{2}) = \sqrt{R^{2} - t^{2}}$
42	40 41	syl	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R]) \to ({\sqrt ↾}_{[0, +∞)}) (R^{2} - t^{2}) = \sqrt{R^{2} - t^{2}}$
43	42	mpteq2dva	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ ({\sqrt ↾}_{[0, +∞)}) (R^{2} - t^{2})) = (t \in [- R, R] ⟼ \sqrt{R^{2} - t^{2}})$
44		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
45	44	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
46		ax-resscn	$⊢ ℝ \subseteq ℂ$
47	6 46	sstrdi	$⊢ R \in ℝ \to [- R, R] \subseteq ℂ$
48		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [- R, R] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] \in TopOn ([- R, R])$
49	45 47 48	sylancr	$⊢ R \in ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] \in TopOn ([- R, R])$
50	49	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] \in TopOn ([- R, R])$
51	47	resmptd	$⊢ R \in ℝ \to {(t \in ℂ ⟼ R^{2} - t^{2}) ↾}_{[- R, R]} = (t \in [- R, R] ⟼ R^{2} - t^{2})$
52	45	a1i	$⊢ R \in ℝ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
53		recn	$⊢ R \in ℝ \to R \in ℂ$
54	53	sqcld	$⊢ R \in ℝ \to R^{2} \in ℂ$
55	52 52 54	cnmptc	$⊢ R \in ℝ \to (t \in ℂ ⟼ R^{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
56	44	sqcn	$⊢ (t \in ℂ ⟼ t^{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
57	56	a1i	$⊢ R \in ℝ \to (t \in ℂ ⟼ t^{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
58	44	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
59	58	a1i	$⊢ R \in ℝ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
60	52 55 57 59	cnmpt12f	$⊢ R \in ℝ \to (t \in ℂ ⟼ R^{2} - t^{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
61	45	toponunii	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
62	61	cnrest	$⊢ ((t \in ℂ ⟼ R^{2} - t^{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld})) \land [- R, R] \subseteq ℂ) \to {(t \in ℂ ⟼ R^{2} - t^{2}) ↾}_{[- R, R]} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn TopOpen (ℂ_{fld}))$
63	60 47 62	syl2anc	$⊢ R \in ℝ \to {(t \in ℂ ⟼ R^{2} - t^{2}) ↾}_{[- R, R]} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn TopOpen (ℂ_{fld}))$
64	51 63	eqeltrrd	$⊢ R \in ℝ \to (t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn TopOpen (ℂ_{fld}))$
65	64	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn TopOpen (ℂ_{fld}))$
66	45	a1i	$⊢ (R \in ℝ \land 0 \leq R) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
67		eqid	$⊢ (t \in [- R, R] ⟼ R^{2} - t^{2}) = (t \in [- R, R] ⟼ R^{2} - t^{2})$
68	67	rnmpt	$⊢ ran (t \in [- R, R] ⟼ R^{2} - t^{2}) = \{u \| \exists t \in [- R, R] u = R^{2} - t^{2}\}$
69		simp3	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R] \land u = R^{2} - t^{2}) \to u = R^{2} - t^{2}$
70	40	3adant3	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R] \land u = R^{2} - t^{2}) \to R^{2} - t^{2} \in [0, +∞)$
71	69 70	eqeltrd	$⊢ ((R \in ℝ \land 0 \leq R) \land t \in [- R, R] \land u = R^{2} - t^{2}) \to u \in [0, +∞)$
72	71	rexlimdv3a	$⊢ (R \in ℝ \land 0 \leq R) \to (\exists t \in [- R, R] u = R^{2} - t^{2} \to u \in [0, +∞))$
73	72	abssdv	$⊢ (R \in ℝ \land 0 \leq R) \to \{u \| \exists t \in [- R, R] u = R^{2} - t^{2}\} \subseteq [0, +∞)$
74	68 73	eqsstrid	$⊢ (R \in ℝ \land 0 \leq R) \to ran (t \in [- R, R] ⟼ R^{2} - t^{2}) \subseteq [0, +∞)$
75		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
76	75 46	sstri	$⊢ [0, +∞) \subseteq ℂ$
77	76	a1i	$⊢ (R \in ℝ \land 0 \leq R) \to [0, +∞) \subseteq ℂ$
78		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (t \in [- R, R] ⟼ R^{2} - t^{2}) \subseteq [0, +∞) \land [0, +∞) \subseteq ℂ) \to ((t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn TopOpen (ℂ_{fld})) \leftrightarrow (t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞))))$
79	66 74 77 78	syl3anc	$⊢ (R \in ℝ \land 0 \leq R) \to ((t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn TopOpen (ℂ_{fld})) \leftrightarrow (t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞))))$
80	65 79	mpbid	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ R^{2} - t^{2}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)))$
81		ssid	$⊢ ℂ \subseteq ℂ$
82		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [0, +∞) \underset{cn}{⟶} ℝ \subseteq [0, +∞) \underset{cn}{⟶} ℂ$
83	46 81 82	mp2an	$⊢ [0, +∞) \underset{cn}{⟶} ℝ \subseteq [0, +∞) \underset{cn}{⟶} ℂ$
84		resqrtcn	$⊢ ({\sqrt ↾}_{[0, +∞)}) : [0, +∞) \underset{cn}{⟶} ℝ$
85	83 84	sselii	$⊢ ({\sqrt ↾}_{[0, +∞)}) : [0, +∞) \underset{cn}{⟶} ℂ$
86		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)$
87		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
88	44 86 87	cncfcn	$⊢ ([0, +∞) \subseteq ℂ \land ℂ \subseteq ℂ) \to [0, +∞) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
89	76 81 88	mp2an	$⊢ [0, +∞) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
90	85 89	eleqtri	$⊢ {\sqrt ↾}_{[0, +∞)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
91	90	a1i	$⊢ (R \in ℝ \land 0 \leq R) \to {\sqrt ↾}_{[0, +∞)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
92	50 80 91	cnmpt11f	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ ({\sqrt ↾}_{[0, +∞)}) (R^{2} - t^{2})) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
93		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] = TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]$
94	44 93 87	cncfcn	$⊢ ([- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to [- R, R] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
95	47 81 94	sylancl	$⊢ R \in ℝ \to [- R, R] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
96	95	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to [- R, R] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
97	92 96	eleqtrrd	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ ({\sqrt ↾}_{[0, +∞)}) (R^{2} - t^{2})) : [- R, R] \underset{cn}{⟶} ℂ$
98	43 97	eqeltrrd	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem areacirclem2

Proof