areacirclem4

Description: Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

		Ref	Expression
	Assertion	areacirclem4	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ R^{2} (arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}})) : [- R, R] \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ R \in ℝ^{+} \to R \in ℂ$
2	1	sqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℂ$
3		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
4	3	renegcld	$⊢ R \in ℝ^{+} \to - R \in ℝ$
5		iccssre	$⊢ (- R \in ℝ \land R \in ℝ) \to [- R, R] \subseteq ℝ$
6	4 3 5	syl2anc	$⊢ R \in ℝ^{+} \to [- R, R] \subseteq ℝ$
7		ax-resscn	$⊢ ℝ \subseteq ℂ$
8	6 7	sstrdi	$⊢ R \in ℝ^{+} \to [- R, R] \subseteq ℂ$
9		ssid	$⊢ ℂ \subseteq ℂ$
10	9	a1i	$⊢ R \in ℝ^{+} \to ℂ \subseteq ℂ$
11		cncfmptc	$⊢ (R^{2} \in ℂ \land [- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ R^{2}) : [- R, R] \underset{cn}{⟶} ℂ$
12	2 8 10 11	syl3anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ R^{2}) : [- R, R] \underset{cn}{⟶} ℂ$
13		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
14	13	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
15	14	a1i	$⊢ R \in ℝ^{+} \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
16	8	sselda	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to t \in ℂ$
17	1	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R \in ℂ$
18		rpne0	$⊢ R \in ℝ^{+} \to R \neq 0$
19	18	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R \neq 0$
20	16 17 19	divcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{t}{R} \in ℂ$
21		asinval	$⊢ \frac{t}{R} \in ℂ \to arcsin (\frac{t}{R}) = (- i) \log (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})$
22	20 21	syl	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to arcsin (\frac{t}{R}) = (- i) \log (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})$
23		ax-icn	$⊢ i \in ℂ$
24	23	a1i	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i \in ℂ$
25	24 20	mulcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{t}{R}) \in ℂ$
26		1cnd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 1 \in ℂ$
27	20	sqcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to {(\frac{t}{R})}^{2} \in ℂ$
28	26 27	subcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 1 - {(\frac{t}{R})}^{2} \in ℂ$
29	28	sqrtcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
30	25 29	addcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
31		0lt1	$⊢ 0 < 1$
32		simp3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to t = 0$
33	32	oveq1d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to \frac{t}{R} = \frac{0}{R}$
34	1 18	div0d	$⊢ R \in ℝ^{+} \to \frac{0}{R} = 0$
35	34	3ad2ant1	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to \frac{0}{R} = 0$
36	33 35	eqtrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to \frac{t}{R} = 0$
37	36	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to i (\frac{t}{R}) = i \cdot 0$
38		it0e0	$⊢ i \cdot 0 = 0$
39	37 38	eqtrdi	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to i (\frac{t}{R}) = 0$
40	36	oveq1d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to {(\frac{t}{R})}^{2} = 0^{2}$
41	40	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to 1 - {(\frac{t}{R})}^{2} = 1 - 0^{2}$
42	41	fveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to \sqrt{1 - {(\frac{t}{R})}^{2}} = \sqrt{1 - 0^{2}}$
43		sq0	$⊢ 0^{2} = 0$
44	43	oveq2i	$⊢ 1 - 0^{2} = 1 - 0$
45		1m0e1	$⊢ 1 - 0 = 1$
46	44 45	eqtri	$⊢ 1 - 0^{2} = 1$
47	46	fveq2i	$⊢ \sqrt{1 - 0^{2}} = \sqrt{1}$
48		sqrt1	$⊢ \sqrt{1} = 1$
49	47 48	eqtri	$⊢ \sqrt{1 - 0^{2}} = 1$
50	42 49	eqtrdi	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to \sqrt{1 - {(\frac{t}{R})}^{2}} = 1$
51	39 50	oveq12d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} = 0 + 1$
52		0p1e1	$⊢ 0 + 1 = 1$
53	51 52	eqtrdi	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} = 1$
54	53	breq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to (0 < i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leftrightarrow 0 < 1)$
55		0red	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to 0 \in ℝ$
56		1red	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to 1 \in ℝ$
57	53 56	eqeltrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
58	55 57	ltnled	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to (0 < i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leftrightarrow \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
59	54 58	bitr3d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to (0 < 1 \leftrightarrow \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
60	31 59	mpbii	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t = 0) \to \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0$
61	60	3expa	$⊢ ((R \in ℝ^{+} \land t \in [- R, R]) \land t = 0) \to \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0$
62	61	olcd	$⊢ ((R \in ℝ^{+} \land t \in [- R, R]) \land t = 0) \to (\neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \lor \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
63		inelr	$⊢ \neg i \in ℝ$
64	25 29	pncand	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}} = i (\frac{t}{R})$
65	64	3adant3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}} = i (\frac{t}{R})$
66	65	oveq1d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}}) (\frac{R}{t}) = i (\frac{t}{R}) (\frac{R}{t})$
67	23	a1i	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to i \in ℂ$
68	20	3adant3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to \frac{t}{R} \in ℂ$
69	1	3ad2ant1	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to R \in ℂ$
70	16	3adant3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to t \in ℂ$
71		simp3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to t \neq 0$
72	69 70 71	divcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to \frac{R}{t} \in ℂ$
73	67 68 72	mulassd	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to i (\frac{t}{R}) (\frac{R}{t}) = i (\frac{t}{R}) (\frac{R}{t})$
74	66 73	eqtrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}}) (\frac{R}{t}) = i (\frac{t}{R}) (\frac{R}{t})$
75	18	3ad2ant1	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to R \neq 0$
76	70 69 71 75	divcan6d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to (\frac{t}{R}) (\frac{R}{t}) = 1$
77	76	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to i (\frac{t}{R}) (\frac{R}{t}) = i \cdot 1$
78	67	mulridd	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to i \cdot 1 = i$
79	74 77 78	3eqtrrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to i = (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}}) (\frac{R}{t})$
80	79	adantr	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to i = (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}}) (\frac{R}{t})$
81		simpr	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
82		1red	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 1 \in ℝ$
83	6	sselda	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to t \in ℝ$
84	3	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R \in ℝ$
85	83 84 19	redivcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{t}{R} \in ℝ$
86	85	resqcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to {(\frac{t}{R})}^{2} \in ℝ$
87	82 86	resubcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 1 - {(\frac{t}{R})}^{2} \in ℝ$
88		elicc2	$⊢ (- R \in ℝ \land R \in ℝ) \to (t \in [- R, R] \leftrightarrow (t \in ℝ \land - R \leq t \land t \leq R))$
89	4 3 88	syl2anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] \leftrightarrow (t \in ℝ \land - R \leq t \land t \leq R))$
90		1red	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 1 \in ℝ$
91		simpr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to t \in ℝ$
92	3	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \in ℝ$
93	18	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \neq 0$
94	91 92 93	redivcld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to \frac{t}{R} \in ℝ$
95	94	resqcld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to {(\frac{t}{R})}^{2} \in ℝ$
96	90 95	subge0d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (0 \leq 1 - {(\frac{t}{R})}^{2} \leftrightarrow {(\frac{t}{R})}^{2} \leq 1)$
97		recn	$⊢ t \in ℝ \to t \in ℂ$
98	97	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to t \in ℂ$
99	1	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \in ℂ$
100	98 99 93	sqdivd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to {(\frac{t}{R})}^{2} = \frac{t^{2}}{R^{2}}$
101	100	breq1d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ({(\frac{t}{R})}^{2} \leq 1 \leftrightarrow \frac{t^{2}}{R^{2}} \leq 1)$
102		resqcl	$⊢ t \in ℝ \to t^{2} \in ℝ$
103	102	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to t^{2} \in ℝ$
104	3	resqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℝ$
105		rpgt0	$⊢ R \in ℝ^{+} \to 0 < R$
106		0red	$⊢ R \in ℝ^{+} \to 0 \in ℝ$
107		0le0	$⊢ 0 \leq 0$
108	107	a1i	$⊢ R \in ℝ^{+} \to 0 \leq 0$
109		rpge0	$⊢ R \in ℝ^{+} \to 0 \leq R$
110	106 3 108 109	lt2sqd	$⊢ R \in ℝ^{+} \to (0 < R \leftrightarrow 0^{2} < R^{2})$
111	43	a1i	$⊢ R \in ℝ^{+} \to 0^{2} = 0$
112	111	breq1d	$⊢ R \in ℝ^{+} \to (0^{2} < R^{2} \leftrightarrow 0 < R^{2})$
113	110 112	bitrd	$⊢ R \in ℝ^{+} \to (0 < R \leftrightarrow 0 < R^{2})$
114	105 113	mpbid	$⊢ R \in ℝ^{+} \to 0 < R^{2}$
115	104 114	elrpd	$⊢ R \in ℝ^{+} \to R^{2} \in ℝ^{+}$
116	115	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R^{2} \in ℝ^{+}$
117	103 90 116	ledivmuld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\frac{t^{2}}{R^{2}} \leq 1 \leftrightarrow t^{2} \leq R^{2} \cdot 1)$
118		absresq	$⊢ t \in ℝ \to {\|t\|}^{2} = t^{2}$
119	118	eqcomd	$⊢ t \in ℝ \to t^{2} = {\|t\|}^{2}$
120	2	mulridd	$⊢ R \in ℝ^{+} \to R^{2} \cdot 1 = R^{2}$
121	119 120	breqan12rd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (t^{2} \leq R^{2} \cdot 1 \leftrightarrow {\|t\|}^{2} \leq R^{2})$
122	97	abscld	$⊢ t \in ℝ \to \|t\| \in ℝ$
123	122	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to \|t\| \in ℝ$
124	97	absge0d	$⊢ t \in ℝ \to 0 \leq \|t\|$
125	124	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 0 \leq \|t\|$
126	109	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 0 \leq R$
127	123 92 125 126	le2sqd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\|t\| \leq R \leftrightarrow {\|t\|}^{2} \leq R^{2})$
128	91 92	absled	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\|t\| \leq R \leftrightarrow (- R \leq t \land t \leq R))$
129	121 127 128	3bitr2d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (t^{2} \leq R^{2} \cdot 1 \leftrightarrow (- R \leq t \land t \leq R))$
130	117 129	bitrd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\frac{t^{2}}{R^{2}} \leq 1 \leftrightarrow (- R \leq t \land t \leq R))$
131	96 101 130	3bitrrd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R \leq t \land t \leq R) \leftrightarrow 0 \leq 1 - {(\frac{t}{R})}^{2})$
132	131	biimpd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R \leq t \land t \leq R) \to 0 \leq 1 - {(\frac{t}{R})}^{2})$
133	132	exp4b	$⊢ R \in ℝ^{+} \to (t \in ℝ \to (- R \leq t \to (t \leq R \to 0 \leq 1 - {(\frac{t}{R})}^{2})))$
134	133	3impd	$⊢ R \in ℝ^{+} \to ((t \in ℝ \land - R \leq t \land t \leq R) \to 0 \leq 1 - {(\frac{t}{R})}^{2})$
135	89 134	sylbid	$⊢ R \in ℝ^{+} \to (t \in [- R, R] \to 0 \leq 1 - {(\frac{t}{R})}^{2})$
136	135	imp	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 0 \leq 1 - {(\frac{t}{R})}^{2}$
137	87 136	resqrtcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
138	137	3adant3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
139	138	adantr	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
140	81 139	resubcld	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
141	3	3ad2ant1	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to R \in ℝ$
142	83	3adant3	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to t \in ℝ$
143	141 142 71	redivcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to \frac{R}{t} \in ℝ$
144	143	adantr	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to \frac{R}{t} \in ℝ$
145	140 144	remulcld	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} - \sqrt{1 - {(\frac{t}{R})}^{2}}) (\frac{R}{t}) \in ℝ$
146	80 145	eqeltrd	$⊢ ((R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ) \to i \in ℝ$
147	146	ex	$⊢ (R \in ℝ^{+} \land t \in [- R, R] \land t \neq 0) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \to i \in ℝ)$
148	147	3expa	$⊢ ((R \in ℝ^{+} \land t \in [- R, R]) \land t \neq 0) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \to i \in ℝ)$
149	63 148	mtoi	$⊢ ((R \in ℝ^{+} \land t \in [- R, R]) \land t \neq 0) \to \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ$
150	149	orcd	$⊢ ((R \in ℝ^{+} \land t \in [- R, R]) \land t \neq 0) \to (\neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \lor \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
151	62 150	pm2.61dane	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \lor \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
152		ianor	$⊢ \neg (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0) \leftrightarrow (\neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \lor \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
153	151 152	sylibr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \neg (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
154		mnfxr	$⊢ −∞ \in ℝ^{*}$
155		0re	$⊢ 0 \in ℝ$
156		elioc2	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in (−∞, 0] \leftrightarrow (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land −∞ < i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0))$
157	154 155 156	mp2an	$⊢ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in (−∞, 0] \leftrightarrow (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land −∞ < i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
158		3simpb	$⊢ (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land −∞ < i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0) \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
159	157 158	sylbi	$⊢ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in (−∞, 0] \to (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℝ \land i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \leq 0)$
160	153 159	nsyl	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \neg i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in (−∞, 0]$
161	30 160	eldifd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in (ℂ ∖ (−∞, 0])$
162		fvres	$⊢ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}} \in (ℂ ∖ (−∞, 0]) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) = \log (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})$
163	161 162	syl	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) = \log (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})$
164	163	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (- i) ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) = (- i) \log (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})$
165	22 164	eqtr4d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to arcsin (\frac{t}{R}) = (- i) ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})$
166	165	mpteq2dva	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ arcsin (\frac{t}{R})) = (t \in [- R, R] ⟼ (- i) ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}))$
167		negicn	$⊢ - i \in ℂ$
168	167	a1i	$⊢ R \in ℝ^{+} \to - i \in ℂ$
169		cncfmptc	$⊢ (- i \in ℂ \land [- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ - i) : [- R, R] \underset{cn}{⟶} ℂ$
170	168 8 10 169	syl3anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ - i) : [- R, R] \underset{cn}{⟶} ℂ$
171	13	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
172	171	a1i	$⊢ R \in ℝ^{+} \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
173		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [- R, R] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] \in TopOn ([- R, R])$
174	172 8 173	syl2anc	$⊢ R \in ℝ^{+} \to TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] \in TopOn ([- R, R])$
175	161	fmpttd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] ⟶ ℂ ∖ (−∞, 0]$
176		difssd	$⊢ R \in ℝ^{+} \to ℂ ∖ (−∞, 0] \subseteq ℂ$
177	16 17 19	divrec2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{t}{R} = (\frac{1}{R}) t$
178	177	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{t}{R}) = i (\frac{1}{R}) t$
179	1 18	reccld	$⊢ R \in ℝ^{+} \to \frac{1}{R} \in ℂ$
180	179	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{1}{R} \in ℂ$
181	24 180 16	mulassd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{1}{R}) t = i (\frac{1}{R}) t$
182	178 181	eqtr4d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to i (\frac{t}{R}) = i (\frac{1}{R}) t$
183	182	mpteq2dva	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{t}{R})) = (t \in [- R, R] ⟼ i (\frac{1}{R}) t)$
184	23	a1i	$⊢ R \in ℝ^{+} \to i \in ℂ$
185	184 179	mulcld	$⊢ R \in ℝ^{+} \to i (\frac{1}{R}) \in ℂ$
186		cncfmptc	$⊢ (i (\frac{1}{R}) \in ℂ \land [- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ i (\frac{1}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
187	185 8 10 186	syl3anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{1}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
188		cncfmptid	$⊢ ([- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ t) : [- R, R] \underset{cn}{⟶} ℂ$
189	8 10 188	syl2anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ t) : [- R, R] \underset{cn}{⟶} ℂ$
190	187 189	mulcncf	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{1}{R}) t) : [- R, R] \underset{cn}{⟶} ℂ$
191	183 190	eqeltrd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{t}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
192	17 29	mulcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
193	192 17 19	divrec2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{R \sqrt{1 - {(\frac{t}{R})}^{2}}}{R} = (\frac{1}{R}) R \sqrt{1 - {(\frac{t}{R})}^{2}}$
194	29 17 19	divcan3d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{R \sqrt{1 - {(\frac{t}{R})}^{2}}}{R} = \sqrt{1 - {(\frac{t}{R})}^{2}}$
195	104	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} \in ℝ$
196	3	sqge0d	$⊢ R \in ℝ^{+} \to 0 \leq R^{2}$
197	196	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 0 \leq R^{2}$
198	195 197 87 136	sqrtmuld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{R^{2} (1 - {(\frac{t}{R})}^{2})} = \sqrt{R^{2}} \sqrt{1 - {(\frac{t}{R})}^{2}}$
199	2	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} \in ℂ$
200	199 26 27	subdid	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} (1 - {(\frac{t}{R})}^{2}) = R^{2} \cdot 1 - R^{2} {(\frac{t}{R})}^{2}$
201	199	mulridd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} \cdot 1 = R^{2}$
202	16 17 19	sqdivd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to {(\frac{t}{R})}^{2} = \frac{t^{2}}{R^{2}}$
203	202	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} {(\frac{t}{R})}^{2} = R^{2} (\frac{t^{2}}{R^{2}})$
204	16	sqcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to t^{2} \in ℂ$
205		sqne0	$⊢ R \in ℂ \to (R^{2} \neq 0 \leftrightarrow R \neq 0)$
206	1 205	syl	$⊢ R \in ℝ^{+} \to (R^{2} \neq 0 \leftrightarrow R \neq 0)$
207	18 206	mpbird	$⊢ R \in ℝ^{+} \to R^{2} \neq 0$
208	207	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} \neq 0$
209	204 199 208	divcan2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} (\frac{t^{2}}{R^{2}}) = t^{2}$
210	203 209	eqtrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} {(\frac{t}{R})}^{2} = t^{2}$
211	201 210	oveq12d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} \cdot 1 - R^{2} {(\frac{t}{R})}^{2} = R^{2} - t^{2}$
212	200 211	eqtrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} (1 - {(\frac{t}{R})}^{2}) = R^{2} - t^{2}$
213	212	fveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{R^{2} (1 - {(\frac{t}{R})}^{2})} = \sqrt{R^{2} - t^{2}}$
214	109	adantr	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to 0 \leq R$
215	84 214	sqrtsqd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{R^{2}} = R$
216	215	oveq1d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{R^{2}} \sqrt{1 - {(\frac{t}{R})}^{2}} = R \sqrt{1 - {(\frac{t}{R})}^{2}}$
217	198 213 216	3eqtr3rd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R \sqrt{1 - {(\frac{t}{R})}^{2}} = \sqrt{R^{2} - t^{2}}$
218	217	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{1}{R}) R \sqrt{1 - {(\frac{t}{R})}^{2}} = (\frac{1}{R}) \sqrt{R^{2} - t^{2}}$
219	193 194 218	3eqtr3d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{1 - {(\frac{t}{R})}^{2}} = (\frac{1}{R}) \sqrt{R^{2} - t^{2}}$
220	219	mpteq2dva	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ \sqrt{1 - {(\frac{t}{R})}^{2}}) = (t \in [- R, R] ⟼ (\frac{1}{R}) \sqrt{R^{2} - t^{2}})$
221		cncfmptc	$⊢ (\frac{1}{R} \in ℂ \land [- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ \frac{1}{R}) : [- R, R] \underset{cn}{⟶} ℂ$
222	179 8 10 221	syl3anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ \frac{1}{R}) : [- R, R] \underset{cn}{⟶} ℂ$
223		areacirclem2	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
224	3 109 223	syl2anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
225	222 224	mulcncf	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ (\frac{1}{R}) \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
226	220 225	eqeltrd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
227	13 15 191 226	cncfmpt2f	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
228		cncfcdm	$⊢ (ℂ ∖ (−∞, 0] \subseteq ℂ \land (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} ℂ) \to ((t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} (ℂ ∖ (−∞, 0]) \leftrightarrow (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] ⟶ ℂ ∖ (−∞, 0])$
229	176 227 228	syl2anc	$⊢ R \in ℝ^{+} \to ((t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} (ℂ ∖ (−∞, 0]) \leftrightarrow (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] ⟶ ℂ ∖ (−∞, 0])$
230	175 229	mpbird	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} (ℂ ∖ (−∞, 0])$
231		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R] = TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]$
232		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0]) = TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0])$
233	13 231 232	cncfcn	$⊢ ([- R, R] \subseteq ℂ \land ℂ ∖ (−∞, 0] \subseteq ℂ) \to [- R, R] \underset{cn}{⟶} (ℂ ∖ (−∞, 0]) = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0]))$
234	8 176 233	syl2anc	$⊢ R \in ℝ^{+} \to [- R, R] \underset{cn}{⟶} (ℂ ∖ (−∞, 0]) = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0]))$
235	230 234	eleqtrd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0])))$
236		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
237	236	logcn	$⊢ ({log ↾}_{(ℂ ∖ (−∞, 0])}) : (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ$
238		difss	$⊢ ℂ ∖ (−∞, 0] \subseteq ℂ$
239		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
240	13 232 239	cncfcn	$⊢ (ℂ ∖ (−∞, 0] \subseteq ℂ \land ℂ \subseteq ℂ) \to (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0])) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
241	238 9 240	mp2an	$⊢ (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0])) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
242	237 241	eleqtri	$⊢ {log ↾}_{(ℂ ∖ (−∞, 0])} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0])) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
243	242	a1i	$⊢ R \in ℝ^{+} \to {log ↾}_{(ℂ ∖ (−∞, 0])} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ (−∞, 0])) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
244	174 235 243	cnmpt11f	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
245	13 231 239	cncfcn	$⊢ ([- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to [- R, R] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
246	8 10 245	syl2anc	$⊢ R \in ℝ^{+} \to [- R, R] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [- R, R]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
247	244 246	eleqtrrd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})) : [- R, R] \underset{cn}{⟶} ℂ$
248	170 247	mulcncf	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ (- i) ({log ↾}_{(ℂ ∖ (−∞, 0])}) (i (\frac{t}{R}) + \sqrt{1 - {(\frac{t}{R})}^{2}})) : [- R, R] \underset{cn}{⟶} ℂ$
249	166 248	eqeltrd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ arcsin (\frac{t}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
250	219	oveq2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}} = (\frac{t}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}}$
251	199 204	subcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to R^{2} - t^{2} \in ℂ$
252	251	sqrtcld	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \sqrt{R^{2} - t^{2}} \in ℂ$
253	20 180 252	mulassd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{t}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}} = (\frac{t}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}}$
254	16 17 19	divrecd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to \frac{t}{R} = t (\frac{1}{R})$
255	254	oveq1d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{t}{R}) (\frac{1}{R}) = t (\frac{1}{R}) (\frac{1}{R})$
256	16 180 180	mulassd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to t (\frac{1}{R}) (\frac{1}{R}) = t (\frac{1}{R}) (\frac{1}{R})$
257	255 256	eqtrd	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{t}{R}) (\frac{1}{R}) = t (\frac{1}{R}) (\frac{1}{R})$
258	257	oveq1d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{t}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}} = t (\frac{1}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}}$
259	250 253 258	3eqtr2d	$⊢ (R \in ℝ^{+} \land t \in [- R, R]) \to (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}} = t (\frac{1}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}}$
260	259	mpteq2dva	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}) = (t \in [- R, R] ⟼ t (\frac{1}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}})$
261	179 179	mulcld	$⊢ R \in ℝ^{+} \to (\frac{1}{R}) (\frac{1}{R}) \in ℂ$
262		cncfmptc	$⊢ ((\frac{1}{R}) (\frac{1}{R}) \in ℂ \land [- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ (\frac{1}{R}) (\frac{1}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
263	261 8 10 262	syl3anc	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ (\frac{1}{R}) (\frac{1}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
264	189 263	mulcncf	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ t (\frac{1}{R}) (\frac{1}{R})) : [- R, R] \underset{cn}{⟶} ℂ$
265	264 224	mulcncf	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ t (\frac{1}{R}) (\frac{1}{R}) \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
266	260 265	eqeltrd	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
267	13 15 249 266	cncfmpt2f	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
268	12 267	mulcncf	$⊢ R \in ℝ^{+} \to (t \in [- R, R] ⟼ R^{2} (arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}})) : [- R, R] \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem areacirclem4

Proof