areacirclem1

Description: Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

		Ref	Expression
	Assertion	areacirclem1	$⊢ R \in ℝ^{+} \to \frac{d (t \in (- R, R)⟼ R^{2} (arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}))}{d_{ℝ} t} = (t \in (- R, R) ⟼ 2 \sqrt{R^{2} - t^{2}})$

Proof

Step	Hyp	Ref	Expression
1		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
2	1	a1i	$⊢ R \in ℝ^{+} \to ℝ \in \{ℝ, ℂ\}$
3		elioore	$⊢ t \in (- R, R) \to t \in ℝ$
4	3	recnd	$⊢ t \in (- R, R) \to t \in ℂ$
5	4	adantl	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to t \in ℂ$
6		rpcn	$⊢ R \in ℝ^{+} \to R \in ℂ$
7	6	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R \in ℂ$
8		rpne0	$⊢ R \in ℝ^{+} \to R \neq 0$
9	8	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R \neq 0$
10	5 7 9	divcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \frac{t}{R} \in ℂ$
11		asincl	$⊢ \frac{t}{R} \in ℂ \to arcsin (\frac{t}{R}) \in ℂ$
12	10 11	syl	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to arcsin (\frac{t}{R}) \in ℂ$
13		1cnd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 1 \in ℂ$
14	10	sqcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to {(\frac{t}{R})}^{2} \in ℂ$
15	13 14	subcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 1 - {(\frac{t}{R})}^{2} \in ℂ$
16	15	sqrtcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
17	10 16	mulcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
18	12 17	addcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
19		ovexd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R}) \in V$
20		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
21	20	renegcld	$⊢ R \in ℝ^{+} \to - R \in ℝ$
22	21	rexrd	$⊢ R \in ℝ^{+} \to - R \in ℝ^{*}$
23		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
24		elioo2	$⊢ (- R \in ℝ^{} \land R \in ℝ^{}) \to (t \in (- R, R) \leftrightarrow (t \in ℝ \land - R < t \land t < R))$
25	22 23 24	syl2anc	$⊢ R \in ℝ^{+} \to (t \in (- R, R) \leftrightarrow (t \in ℝ \land - R < t \land t < R))$
26		simpr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to t \in ℝ$
27	20	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \in ℝ$
28	8	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \neq 0$
29	26 27 28	redivcld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to \frac{t}{R} \in ℝ$
30	29	a1d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R < t \land t < R) \to \frac{t}{R} \in ℝ)$
31	6	mulm1d	$⊢ R \in ℝ^{+} \to -1 R = - R$
32	31	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to -1 R = - R$
33	32	breq1d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (-1 R < t \leftrightarrow - R < t)$
34		neg1rr	$⊢ - 1 \in ℝ$
35	34	a1i	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to - 1 \in ℝ$
36		simpl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \in ℝ^{+}$
37	35 26 36	ltmuldivd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (-1 R < t \leftrightarrow - 1 < \frac{t}{R})$
38	33 37	bitr3d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (- R < t \leftrightarrow - 1 < \frac{t}{R})$
39	38	biimpd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (- R < t \to - 1 < \frac{t}{R})$
40	39	adantrd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R < t \land t < R) \to - 1 < \frac{t}{R})$
41		1red	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 1 \in ℝ$
42	26 41 36	ltdivmuld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\frac{t}{R} < 1 \leftrightarrow t < R \cdot 1)$
43	6	mulridd	$⊢ R \in ℝ^{+} \to R \cdot 1 = R$
44	43	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \cdot 1 = R$
45	44	breq2d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (t < R \cdot 1 \leftrightarrow t < R)$
46	42 45	bitr2d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (t < R \leftrightarrow \frac{t}{R} < 1)$
47	46	biimpd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (t < R \to \frac{t}{R} < 1)$
48	47	adantld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R < t \land t < R) \to \frac{t}{R} < 1)$
49	30 40 48	3jcad	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R < t \land t < R) \to (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1))$
50	49	exp4b	$⊢ R \in ℝ^{+} \to (t \in ℝ \to (- R < t \to (t < R \to (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1))))$
51	50	3impd	$⊢ R \in ℝ^{+} \to ((t \in ℝ \land - R < t \land t < R) \to (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1))$
52	25 51	sylbid	$⊢ R \in ℝ^{+} \to (t \in (- R, R) \to (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1))$
53	52	imp	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1)$
54	34	rexri	$⊢ - 1 \in ℝ^{*}$
55		1xr	$⊢ 1 \in ℝ^{*}$
56		elioo2	$⊢ (- 1 \in ℝ^{} \land 1 \in ℝ^{}) \to (\frac{t}{R} \in (- 1, 1) \leftrightarrow (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1))$
57	54 55 56	mp2an	$⊢ \frac{t}{R} \in (- 1, 1) \leftrightarrow (\frac{t}{R} \in ℝ \land - 1 < \frac{t}{R} \land \frac{t}{R} < 1)$
58	53 57	sylibr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \frac{t}{R} \in (- 1, 1)$
59		ovexd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \frac{1}{R} \in V$
60		elioore	$⊢ u \in (- 1, 1) \to u \in ℝ$
61	60	recnd	$⊢ u \in (- 1, 1) \to u \in ℂ$
62		asincl	$⊢ u \in ℂ \to arcsin (u) \in ℂ$
63		id	$⊢ u \in ℂ \to u \in ℂ$
64		1cnd	$⊢ u \in ℂ \to 1 \in ℂ$
65		sqcl	$⊢ u \in ℂ \to u^{2} \in ℂ$
66	64 65	subcld	$⊢ u \in ℂ \to 1 - u^{2} \in ℂ$
67	66	sqrtcld	$⊢ u \in ℂ \to \sqrt{1 - u^{2}} \in ℂ$
68	63 67	mulcld	$⊢ u \in ℂ \to u \sqrt{1 - u^{2}} \in ℂ$
69	62 68	addcld	$⊢ u \in ℂ \to arcsin (u) + u \sqrt{1 - u^{2}} \in ℂ$
70	61 69	syl	$⊢ u \in (- 1, 1) \to arcsin (u) + u \sqrt{1 - u^{2}} \in ℂ$
71	70	adantl	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to arcsin (u) + u \sqrt{1 - u^{2}} \in ℂ$
72		ovexd	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to 2 \sqrt{1 - u^{2}} \in V$
73		recn	$⊢ t \in ℝ \to t \in ℂ$
74	73	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to t \in ℂ$
75		1cnd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 1 \in ℂ$
76	2	dvmptid	$⊢ R \in ℝ^{+} \to \frac{d (t \in ℝ⟼ t)}{d_{ℝ} t} = (t \in ℝ ⟼ 1)$
77		ioossre	$⊢ (- R, R) \subseteq ℝ$
78	77	a1i	$⊢ R \in ℝ^{+} \to (- R, R) \subseteq ℝ$
79		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
80		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
81		iooretop	$⊢ (- R, R) \in topGen (ran (.))$
82	81	a1i	$⊢ R \in ℝ^{+} \to (- R, R) \in topGen (ran (.))$
83	2 74 75 76 78 79 80 82	dvmptres	$⊢ R \in ℝ^{+} \to \frac{d (t \in (- R, R)⟼ t)}{d_{ℝ} t} = (t \in (- R, R) ⟼ 1)$
84	2 5 13 83 6 8	dvmptdivc	$⊢ R \in ℝ^{+} \to \frac{d (t \in (- R, R)⟼ \frac{t}{R})}{d_{ℝ} t} = (t \in (- R, R) ⟼ \frac{1}{R})$
85	61 62	syl	$⊢ u \in (- 1, 1) \to arcsin (u) \in ℂ$
86	85	adantl	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to arcsin (u) \in ℂ$
87		ovexd	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to \frac{1}{\sqrt{1 - u^{2}}} \in V$
88		asinf	$⊢ arcsin : ℂ ⟶ ℂ$
89	88	a1i	$⊢ R \in ℝ^{+} \to arcsin : ℂ ⟶ ℂ$
90		ioossre	$⊢ (- 1, 1) \subseteq ℝ$
91		ax-resscn	$⊢ ℝ \subseteq ℂ$
92	90 91	sstri	$⊢ (- 1, 1) \subseteq ℂ$
93	92	a1i	$⊢ R \in ℝ^{+} \to (- 1, 1) \subseteq ℂ$
94	89 93	feqresmpt	$⊢ R \in ℝ^{+} \to {arcsin ↾}_{(- 1, 1)} = (u \in (- 1, 1) ⟼ arcsin (u))$
95	94	oveq2d	$⊢ R \in ℝ^{+} \to ℝ D ({arcsin ↾}_{(- 1, 1)}) = \frac{d (u \in (- 1, 1)⟼ arcsin (u))}{d_{ℝ} u}$
96		dvreasin	$⊢ ℝ D ({arcsin ↾}_{(- 1, 1)}) = (u \in (- 1, 1) ⟼ \frac{1}{\sqrt{1 - u^{2}}})$
97	95 96	eqtr3di	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ arcsin (u))}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ \frac{1}{\sqrt{1 - u^{2}}})$
98	61 68	syl	$⊢ u \in (- 1, 1) \to u \sqrt{1 - u^{2}} \in ℂ$
99	98	adantl	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to u \sqrt{1 - u^{2}} \in ℂ$
100		ovexd	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u \in V$
101	61	adantl	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to u \in ℂ$
102		1cnd	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to 1 \in ℂ$
103		recn	$⊢ u \in ℝ \to u \in ℂ$
104	103	adantl	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to u \in ℂ$
105		1cnd	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to 1 \in ℂ$
106	2	dvmptid	$⊢ R \in ℝ^{+} \to \frac{d (u \in ℝ⟼ u)}{d_{ℝ} u} = (u \in ℝ ⟼ 1)$
107	90	a1i	$⊢ R \in ℝ^{+} \to (- 1, 1) \subseteq ℝ$
108		iooretop	$⊢ (- 1, 1) \in topGen (ran (.))$
109	108	a1i	$⊢ R \in ℝ^{+} \to (- 1, 1) \in topGen (ran (.))$
110	2 104 105 106 107 79 80 109	dvmptres	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ u)}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ 1)$
111	61 67	syl	$⊢ u \in (- 1, 1) \to \sqrt{1 - u^{2}} \in ℂ$
112	111	adantl	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to \sqrt{1 - u^{2}} \in ℂ$
113		ovexd	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to \frac{- u}{\sqrt{1 - u^{2}}} \in V$
114		1red	$⊢ u \in (- 1, 1) \to 1 \in ℝ$
115	60	resqcld	$⊢ u \in (- 1, 1) \to u^{2} \in ℝ$
116	114 115	resubcld	$⊢ u \in (- 1, 1) \to 1 - u^{2} \in ℝ$
117		elioo2	$⊢ (- 1 \in ℝ^{} \land 1 \in ℝ^{}) \to (u \in (- 1, 1) \leftrightarrow (u \in ℝ \land - 1 < u \land u < 1))$
118	54 55 117	mp2an	$⊢ u \in (- 1, 1) \leftrightarrow (u \in ℝ \land - 1 < u \land u < 1)$
119		id	$⊢ u \in ℝ \to u \in ℝ$
120		1red	$⊢ u \in ℝ \to 1 \in ℝ$
121	119 120	absltd	$⊢ u \in ℝ \to (\|u\| < 1 \leftrightarrow (- 1 < u \land u < 1))$
122	103	abscld	$⊢ u \in ℝ \to \|u\| \in ℝ$
123	103	absge0d	$⊢ u \in ℝ \to 0 \leq \|u\|$
124		0le1	$⊢ 0 \leq 1$
125	124	a1i	$⊢ u \in ℝ \to 0 \leq 1$
126	122 120 123 125	lt2sqd	$⊢ u \in ℝ \to (\|u\| < 1 \leftrightarrow {\|u\|}^{2} < 1^{2})$
127		absresq	$⊢ u \in ℝ \to {\|u\|}^{2} = u^{2}$
128		sq1	$⊢ 1^{2} = 1$
129	128	a1i	$⊢ u \in ℝ \to 1^{2} = 1$
130	127 129	breq12d	$⊢ u \in ℝ \to ({\|u\|}^{2} < 1^{2} \leftrightarrow u^{2} < 1)$
131		resqcl	$⊢ u \in ℝ \to u^{2} \in ℝ$
132	131 120	posdifd	$⊢ u \in ℝ \to (u^{2} < 1 \leftrightarrow 0 < 1 - u^{2})$
133	126 130 132	3bitrd	$⊢ u \in ℝ \to (\|u\| < 1 \leftrightarrow 0 < 1 - u^{2})$
134	121 133	bitr3d	$⊢ u \in ℝ \to ((- 1 < u \land u < 1) \leftrightarrow 0 < 1 - u^{2})$
135	134	biimpd	$⊢ u \in ℝ \to ((- 1 < u \land u < 1) \to 0 < 1 - u^{2})$
136	135	3impib	$⊢ (u \in ℝ \land - 1 < u \land u < 1) \to 0 < 1 - u^{2}$
137	118 136	sylbi	$⊢ u \in (- 1, 1) \to 0 < 1 - u^{2}$
138	116 137	elrpd	$⊢ u \in (- 1, 1) \to 1 - u^{2} \in ℝ^{+}$
139	138	adantl	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to 1 - u^{2} \in ℝ^{+}$
140		negex	$⊢ - 2 u \in V$
141	140	a1i	$⊢ (R \in ℝ^{+} \land u \in (- 1, 1)) \to - 2 u \in V$
142		rpcn	$⊢ v \in ℝ^{+} \to v \in ℂ$
143	142	sqrtcld	$⊢ v \in ℝ^{+} \to \sqrt{v} \in ℂ$
144	143	adantl	$⊢ (R \in ℝ^{+} \land v \in ℝ^{+}) \to \sqrt{v} \in ℂ$
145		ovexd	$⊢ (R \in ℝ^{+} \land v \in ℝ^{+}) \to \frac{1}{2 \sqrt{v}} \in V$
146		1cnd	$⊢ u \in ℝ \to 1 \in ℂ$
147	103	sqcld	$⊢ u \in ℝ \to u^{2} \in ℂ$
148	146 147	subcld	$⊢ u \in ℝ \to 1 - u^{2} \in ℂ$
149	148	adantl	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to 1 - u^{2} \in ℂ$
150	140	a1i	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to - 2 u \in V$
151		0red	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to 0 \in ℝ$
152		1cnd	$⊢ R \in ℝ^{+} \to 1 \in ℂ$
153	2 152	dvmptc	$⊢ R \in ℝ^{+} \to \frac{d (u \in ℝ⟼ 1)}{d_{ℝ} u} = (u \in ℝ ⟼ 0)$
154	147	adantl	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to u^{2} \in ℂ$
155		ovexd	$⊢ (R \in ℝ^{+} \land u \in ℝ) \to 2 u \in V$
156	80	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
157		toponmax	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ) \to ℂ \in TopOpen (ℂ_{fld})$
158	156 157	mp1i	$⊢ R \in ℝ^{+} \to ℂ \in TopOpen (ℂ_{fld})$
159		dfss2	$⊢ ℝ \subseteq ℂ \leftrightarrow ℝ \cap ℂ = ℝ$
160	91 159	mpbi	$⊢ ℝ \cap ℂ = ℝ$
161	160	a1i	$⊢ R \in ℝ^{+} \to ℝ \cap ℂ = ℝ$
162	65	adantl	$⊢ (R \in ℝ^{+} \land u \in ℂ) \to u^{2} \in ℂ$
163		ovexd	$⊢ (R \in ℝ^{+} \land u \in ℂ) \to 2 u \in V$
164		2nn	$⊢ 2 \in ℕ$
165		dvexp	$⊢ 2 \in ℕ \to \frac{d (u \in ℂ⟼ u^{2})}{d_{ℂ} u} = (u \in ℂ ⟼ 2 u^{2 - 1})$
166	164 165	ax-mp	$⊢ \frac{d (u \in ℂ⟼ u^{2})}{d_{ℂ} u} = (u \in ℂ ⟼ 2 u^{2 - 1})$
167		2m1e1	$⊢ 2 - 1 = 1$
168	167	oveq2i	$⊢ u^{2 - 1} = u^{1}$
169		exp1	$⊢ u \in ℂ \to u^{1} = u$
170	168 169	eqtrid	$⊢ u \in ℂ \to u^{2 - 1} = u$
171	170	oveq2d	$⊢ u \in ℂ \to 2 u^{2 - 1} = 2 u$
172	171	mpteq2ia	$⊢ (u \in ℂ ⟼ 2 u^{2 - 1}) = (u \in ℂ ⟼ 2 u)$
173	166 172	eqtri	$⊢ \frac{d (u \in ℂ⟼ u^{2})}{d_{ℂ} u} = (u \in ℂ ⟼ 2 u)$
174	173	a1i	$⊢ R \in ℝ^{+} \to \frac{d (u \in ℂ⟼ u^{2})}{d_{ℂ} u} = (u \in ℂ ⟼ 2 u)$
175	80 2 158 161 162 163 174	dvmptres3	$⊢ R \in ℝ^{+} \to \frac{d (u \in ℝ⟼ u^{2})}{d_{ℝ} u} = (u \in ℝ ⟼ 2 u)$
176	2 105 151 153 154 155 175	dvmptsub	$⊢ R \in ℝ^{+} \to \frac{d (u \in ℝ⟼ 1 - u^{2})}{d_{ℝ} u} = (u \in ℝ ⟼ 0 - 2 u)$
177		df-neg	$⊢ - 2 u = 0 - 2 u$
178	177	mpteq2i	$⊢ (u \in ℝ ⟼ - 2 u) = (u \in ℝ ⟼ 0 - 2 u)$
179	176 178	eqtr4di	$⊢ R \in ℝ^{+} \to \frac{d (u \in ℝ⟼ 1 - u^{2})}{d_{ℝ} u} = (u \in ℝ ⟼ - 2 u)$
180	2 149 150 179 107 79 80 109	dvmptres	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ 1 - u^{2})}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ - 2 u)$
181		dvsqrt	$⊢ \frac{d (v \in ℝ^{+}⟼ \sqrt{v})}{d_{ℝ} v} = (v \in ℝ^{+} ⟼ \frac{1}{2 \sqrt{v}})$
182	181	a1i	$⊢ R \in ℝ^{+} \to \frac{d (v \in ℝ^{+}⟼ \sqrt{v})}{d_{ℝ} v} = (v \in ℝ^{+} ⟼ \frac{1}{2 \sqrt{v}})$
183		fveq2	$⊢ v = 1 - u^{2} \to \sqrt{v} = \sqrt{1 - u^{2}}$
184	183	oveq2d	$⊢ v = 1 - u^{2} \to 2 \sqrt{v} = 2 \sqrt{1 - u^{2}}$
185	184	oveq2d	$⊢ v = 1 - u^{2} \to \frac{1}{2 \sqrt{v}} = \frac{1}{2 \sqrt{1 - u^{2}}}$
186	2 2 139 141 144 145 180 182 183 185	dvmptco	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ \sqrt{1 - u^{2}})}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ (\frac{1}{2 \sqrt{1 - u^{2}}}) (- 2 u))$
187		2cnd	$⊢ u \in (- 1, 1) \to 2 \in ℂ$
188	187 61	mulneg2d	$⊢ u \in (- 1, 1) \to 2 (- u) = - 2 u$
189	188	oveq1d	$⊢ u \in (- 1, 1) \to \frac{2 (- u)}{2 \sqrt{1 - u^{2}}} = \frac{- 2 u}{2 \sqrt{1 - u^{2}}}$
190	61	negcld	$⊢ u \in (- 1, 1) \to - u \in ℂ$
191	137	gt0ne0d	$⊢ u \in (- 1, 1) \to 1 - u^{2} \neq 0$
192	61 66	syl	$⊢ u \in (- 1, 1) \to 1 - u^{2} \in ℂ$
193	192	adantr	$⊢ (u \in (- 1, 1) \land \sqrt{1 - u^{2}} = 0) \to 1 - u^{2} \in ℂ$
194		simpr	$⊢ (u \in (- 1, 1) \land \sqrt{1 - u^{2}} = 0) \to \sqrt{1 - u^{2}} = 0$
195	193 194	sqr00d	$⊢ (u \in (- 1, 1) \land \sqrt{1 - u^{2}} = 0) \to 1 - u^{2} = 0$
196	195	ex	$⊢ u \in (- 1, 1) \to (\sqrt{1 - u^{2}} = 0 \to 1 - u^{2} = 0)$
197	196	necon3d	$⊢ u \in (- 1, 1) \to (1 - u^{2} \neq 0 \to \sqrt{1 - u^{2}} \neq 0)$
198	191 197	mpd	$⊢ u \in (- 1, 1) \to \sqrt{1 - u^{2}} \neq 0$
199		2ne0	$⊢ 2 \neq 0$
200	199	a1i	$⊢ u \in (- 1, 1) \to 2 \neq 0$
201	190 111 187 198 200	divcan5d	$⊢ u \in (- 1, 1) \to \frac{2 (- u)}{2 \sqrt{1 - u^{2}}} = \frac{- u}{\sqrt{1 - u^{2}}}$
202	187 61	mulcld	$⊢ u \in (- 1, 1) \to 2 u \in ℂ$
203	202	negcld	$⊢ u \in (- 1, 1) \to - 2 u \in ℂ$
204	187 111	mulcld	$⊢ u \in (- 1, 1) \to 2 \sqrt{1 - u^{2}} \in ℂ$
205	187 111 200 198	mulne0d	$⊢ u \in (- 1, 1) \to 2 \sqrt{1 - u^{2}} \neq 0$
206	203 204 205	divrec2d	$⊢ u \in (- 1, 1) \to \frac{- 2 u}{2 \sqrt{1 - u^{2}}} = (\frac{1}{2 \sqrt{1 - u^{2}}}) (- 2 u)$
207	189 201 206	3eqtr3rd	$⊢ u \in (- 1, 1) \to (\frac{1}{2 \sqrt{1 - u^{2}}}) (- 2 u) = \frac{- u}{\sqrt{1 - u^{2}}}$
208	207	mpteq2ia	$⊢ (u \in (- 1, 1) ⟼ (\frac{1}{2 \sqrt{1 - u^{2}}}) (- 2 u)) = (u \in (- 1, 1) ⟼ \frac{- u}{\sqrt{1 - u^{2}}})$
209	186 208	eqtrdi	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ \sqrt{1 - u^{2}})}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ \frac{- u}{\sqrt{1 - u^{2}}})$
210	2 101 102 110 112 113 209	dvmptmul	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ u \sqrt{1 - u^{2}})}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u)$
211	2 86 87 97 99 100 210	dvmptadd	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ arcsin (u) + u \sqrt{1 - u^{2}})}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ (\frac{1}{\sqrt{1 - u^{2}}}) + 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u)$
212	111	mullidd	$⊢ u \in (- 1, 1) \to 1 \sqrt{1 - u^{2}} = \sqrt{1 - u^{2}}$
213	190 111 198	divcld	$⊢ u \in (- 1, 1) \to \frac{- u}{\sqrt{1 - u^{2}}} \in ℂ$
214	213 61	mulcomd	$⊢ u \in (- 1, 1) \to (\frac{- u}{\sqrt{1 - u^{2}}}) u = u (\frac{- u}{\sqrt{1 - u^{2}}})$
215	61 190 111 198	divassd	$⊢ u \in (- 1, 1) \to \frac{u (- u)}{\sqrt{1 - u^{2}}} = u (\frac{- u}{\sqrt{1 - u^{2}}})$
216	61 61	mulneg2d	$⊢ u \in (- 1, 1) \to u (- u) = - u u$
217	61	sqvald	$⊢ u \in (- 1, 1) \to u^{2} = u u$
218	217	negeqd	$⊢ u \in (- 1, 1) \to - u^{2} = - u u$
219	216 218	eqtr4d	$⊢ u \in (- 1, 1) \to u (- u) = - u^{2}$
220	219	oveq1d	$⊢ u \in (- 1, 1) \to \frac{u (- u)}{\sqrt{1 - u^{2}}} = \frac{- u^{2}}{\sqrt{1 - u^{2}}}$
221	214 215 220	3eqtr2d	$⊢ u \in (- 1, 1) \to (\frac{- u}{\sqrt{1 - u^{2}}}) u = \frac{- u^{2}}{\sqrt{1 - u^{2}}}$
222	212 221	oveq12d	$⊢ u \in (- 1, 1) \to 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u = \sqrt{1 - u^{2}} + (\frac{- u^{2}}{\sqrt{1 - u^{2}}})$
223	61	sqcld	$⊢ u \in (- 1, 1) \to u^{2} \in ℂ$
224	223	negcld	$⊢ u \in (- 1, 1) \to - u^{2} \in ℂ$
225	224 111 198	divcld	$⊢ u \in (- 1, 1) \to \frac{- u^{2}}{\sqrt{1 - u^{2}}} \in ℂ$
226	111 225	addcomd	$⊢ u \in (- 1, 1) \to \sqrt{1 - u^{2}} + (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) = (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}}$
227	222 226	eqtrd	$⊢ u \in (- 1, 1) \to 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u = (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}}$
228	227	oveq2d	$⊢ u \in (- 1, 1) \to (\frac{1}{\sqrt{1 - u^{2}}}) + 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u = (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}}$
229	111	2timesd	$⊢ u \in (- 1, 1) \to 2 \sqrt{1 - u^{2}} = \sqrt{1 - u^{2}} + \sqrt{1 - u^{2}}$
230	64 65	negsubd	$⊢ u \in ℂ \to 1 + (- u^{2}) = 1 - u^{2}$
231	66	sqsqrtd	$⊢ u \in ℂ \to {\sqrt{1 - u^{2}}}^{2} = 1 - u^{2}$
232	67	sqvald	$⊢ u \in ℂ \to {\sqrt{1 - u^{2}}}^{2} = \sqrt{1 - u^{2}} \sqrt{1 - u^{2}}$
233	230 231 232	3eqtr2d	$⊢ u \in ℂ \to 1 + (- u^{2}) = \sqrt{1 - u^{2}} \sqrt{1 - u^{2}}$
234	61 233	syl	$⊢ u \in (- 1, 1) \to 1 + (- u^{2}) = \sqrt{1 - u^{2}} \sqrt{1 - u^{2}}$
235	234	oveq1d	$⊢ u \in (- 1, 1) \to \frac{1 + (- u^{2})}{\sqrt{1 - u^{2}}} = \frac{\sqrt{1 - u^{2}} \sqrt{1 - u^{2}}}{\sqrt{1 - u^{2}}}$
236		1cnd	$⊢ u \in (- 1, 1) \to 1 \in ℂ$
237	236 224 111 198	divdird	$⊢ u \in (- 1, 1) \to \frac{1 + (- u^{2})}{\sqrt{1 - u^{2}}} = (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}})$
238	111 111 198	divcan3d	$⊢ u \in (- 1, 1) \to \frac{\sqrt{1 - u^{2}} \sqrt{1 - u^{2}}}{\sqrt{1 - u^{2}}} = \sqrt{1 - u^{2}}$
239	235 237 238	3eqtr3rd	$⊢ u \in (- 1, 1) \to \sqrt{1 - u^{2}} = (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}})$
240	239	oveq1d	$⊢ u \in (- 1, 1) \to \sqrt{1 - u^{2}} + \sqrt{1 - u^{2}} = (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}}$
241	111 198	reccld	$⊢ u \in (- 1, 1) \to \frac{1}{\sqrt{1 - u^{2}}} \in ℂ$
242	241 225 111	addassd	$⊢ u \in (- 1, 1) \to (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}} = (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}}$
243	229 240 242	3eqtrrd	$⊢ u \in (- 1, 1) \to (\frac{1}{\sqrt{1 - u^{2}}}) + (\frac{- u^{2}}{\sqrt{1 - u^{2}}}) + \sqrt{1 - u^{2}} = 2 \sqrt{1 - u^{2}}$
244	228 243	eqtrd	$⊢ u \in (- 1, 1) \to (\frac{1}{\sqrt{1 - u^{2}}}) + 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u = 2 \sqrt{1 - u^{2}}$
245	244	mpteq2ia	$⊢ (u \in (- 1, 1) ⟼ (\frac{1}{\sqrt{1 - u^{2}}}) + 1 \sqrt{1 - u^{2}} + (\frac{- u}{\sqrt{1 - u^{2}}}) u) = (u \in (- 1, 1) ⟼ 2 \sqrt{1 - u^{2}})$
246	211 245	eqtrdi	$⊢ R \in ℝ^{+} \to \frac{d (u \in (- 1, 1)⟼ arcsin (u) + u \sqrt{1 - u^{2}})}{d_{ℝ} u} = (u \in (- 1, 1) ⟼ 2 \sqrt{1 - u^{2}})$
247		fveq2	$⊢ u = \frac{t}{R} \to arcsin (u) = arcsin (\frac{t}{R})$
248		id	$⊢ u = \frac{t}{R} \to u = \frac{t}{R}$
249		oveq1	$⊢ u = \frac{t}{R} \to u^{2} = {(\frac{t}{R})}^{2}$
250	249	oveq2d	$⊢ u = \frac{t}{R} \to 1 - u^{2} = 1 - {(\frac{t}{R})}^{2}$
251	250	fveq2d	$⊢ u = \frac{t}{R} \to \sqrt{1 - u^{2}} = \sqrt{1 - {(\frac{t}{R})}^{2}}$
252	248 251	oveq12d	$⊢ u = \frac{t}{R} \to u \sqrt{1 - u^{2}} = (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}$
253	247 252	oveq12d	$⊢ u = \frac{t}{R} \to arcsin (u) + u \sqrt{1 - u^{2}} = arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}$
254	251	oveq2d	$⊢ u = \frac{t}{R} \to 2 \sqrt{1 - u^{2}} = 2 \sqrt{1 - {(\frac{t}{R})}^{2}}$
255	2 2 58 59 71 72 84 246 253 254	dvmptco	$⊢ R \in ℝ^{+} \to \frac{d (t \in (- R, R)⟼ arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}})}{d_{ℝ} t} = (t \in (- R, R) ⟼ 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R}))$
256	6	sqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℂ$
257	2 18 19 255 256	dvmptcmul	$⊢ R \in ℝ^{+} \to \frac{d (t \in (- R, R)⟼ R^{2} (arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}))}{d_{ℝ} t} = (t \in (- R, R) ⟼ R^{2} 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R}))$
258		2cnd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 2 \in ℂ$
259	258 16	mulcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 2 \sqrt{1 - {(\frac{t}{R})}^{2}} \in ℂ$
260	6 8	reccld	$⊢ R \in ℝ^{+} \to \frac{1}{R} \in ℂ$
261	260	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \frac{1}{R} \in ℂ$
262	259 261	mulcomd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R}) = (\frac{1}{R}) 2 \sqrt{1 - {(\frac{t}{R})}^{2}}$
263	262	oveq2d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R}) = R^{2} (\frac{1}{R}) 2 \sqrt{1 - {(\frac{t}{R})}^{2}}$
264	256	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} \in ℂ$
265	264 261 259	mulassd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} (\frac{1}{R}) 2 \sqrt{1 - {(\frac{t}{R})}^{2}} = R^{2} (\frac{1}{R}) 2 \sqrt{1 - {(\frac{t}{R})}^{2}}$
266	6	sqvald	$⊢ R \in ℝ^{+} \to R^{2} = R R$
267	266	oveq1d	$⊢ R \in ℝ^{+} \to \frac{R^{2}}{R} = \frac{R R}{R}$
268	256 6 8	divrecd	$⊢ R \in ℝ^{+} \to \frac{R^{2}}{R} = R^{2} (\frac{1}{R})$
269	6 6 8	divcan3d	$⊢ R \in ℝ^{+} \to \frac{R R}{R} = R$
270	267 268 269	3eqtr3d	$⊢ R \in ℝ^{+} \to R^{2} (\frac{1}{R}) = R$
271	270	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} (\frac{1}{R}) = R$
272	271	oveq1d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} (\frac{1}{R}) 2 \sqrt{1 - {(\frac{t}{R})}^{2}} = R 2 \sqrt{1 - {(\frac{t}{R})}^{2}}$
273	7 258 16	mul12d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R 2 \sqrt{1 - {(\frac{t}{R})}^{2}} = 2 R \sqrt{1 - {(\frac{t}{R})}^{2}}$
274	20	resqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℝ$
275	274	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} \in ℝ$
276	20	sqge0d	$⊢ R \in ℝ^{+} \to 0 \leq R^{2}$
277	276	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 0 \leq R^{2}$
278		1red	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 1 \in ℝ$
279	3	adantl	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to t \in ℝ$
280	20	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R \in ℝ$
281	279 280 9	redivcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \frac{t}{R} \in ℝ$
282	281	resqcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to {(\frac{t}{R})}^{2} \in ℝ$
283	278 282	resubcld	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 1 - {(\frac{t}{R})}^{2} \in ℝ$
284		0red	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 0 \in ℝ$
285	26 27	absltd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\|t\| < R \leftrightarrow (- R < t \land t < R))$
286	73	abscld	$⊢ t \in ℝ \to \|t\| \in ℝ$
287	286	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to \|t\| \in ℝ$
288	73	absge0d	$⊢ t \in ℝ \to 0 \leq \|t\|$
289	288	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 0 \leq \|t\|$
290		rpge0	$⊢ R \in ℝ^{+} \to 0 \leq R$
291	290	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to 0 \leq R$
292	287 27 289 291	lt2sqd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\|t\| < R \leftrightarrow {\|t\|}^{2} < R^{2})$
293		absresq	$⊢ t \in ℝ \to {\|t\|}^{2} = t^{2}$
294	293	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to {\|t\|}^{2} = t^{2}$
295	256	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R^{2} \in ℂ$
296	295	mulridd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R^{2} \cdot 1 = R^{2}$
297	296	eqcomd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R^{2} = R^{2} \cdot 1$
298	294 297	breq12d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ({\|t\|}^{2} < R^{2} \leftrightarrow t^{2} < R^{2} \cdot 1)$
299	6	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R \in ℂ$
300	74 299 28	sqdivd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to {(\frac{t}{R})}^{2} = \frac{t^{2}}{R^{2}}$
301	300	breq1d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ({(\frac{t}{R})}^{2} < 1 \leftrightarrow \frac{t^{2}}{R^{2}} < 1)$
302	29	resqcld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to {(\frac{t}{R})}^{2} \in ℝ$
303	302 41	posdifd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ({(\frac{t}{R})}^{2} < 1 \leftrightarrow 0 < 1 - {(\frac{t}{R})}^{2})$
304		resqcl	$⊢ t \in ℝ \to t^{2} \in ℝ$
305	304	adantl	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to t^{2} \in ℝ$
306		rpgt0	$⊢ R \in ℝ^{+} \to 0 < R$
307		0red	$⊢ R \in ℝ^{+} \to 0 \in ℝ$
308		0le0	$⊢ 0 \leq 0$
309	308	a1i	$⊢ R \in ℝ^{+} \to 0 \leq 0$
310	307 20 309 290	lt2sqd	$⊢ R \in ℝ^{+} \to (0 < R \leftrightarrow 0^{2} < R^{2})$
311		sq0	$⊢ 0^{2} = 0$
312	311	a1i	$⊢ R \in ℝ^{+} \to 0^{2} = 0$
313	312	breq1d	$⊢ R \in ℝ^{+} \to (0^{2} < R^{2} \leftrightarrow 0 < R^{2})$
314	310 313	bitrd	$⊢ R \in ℝ^{+} \to (0 < R \leftrightarrow 0 < R^{2})$
315	306 314	mpbid	$⊢ R \in ℝ^{+} \to 0 < R^{2}$
316	274 315	elrpd	$⊢ R \in ℝ^{+} \to R^{2} \in ℝ^{+}$
317	316	adantr	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to R^{2} \in ℝ^{+}$
318	305 41 317	ltdivmuld	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\frac{t^{2}}{R^{2}} < 1 \leftrightarrow t^{2} < R^{2} \cdot 1)$
319	301 303 318	3bitr3rd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (t^{2} < R^{2} \cdot 1 \leftrightarrow 0 < 1 - {(\frac{t}{R})}^{2})$
320	292 298 319	3bitrd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to (\|t\| < R \leftrightarrow 0 < 1 - {(\frac{t}{R})}^{2})$
321	285 320	bitr3d	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R < t \land t < R) \leftrightarrow 0 < 1 - {(\frac{t}{R})}^{2})$
322	321	biimpd	$⊢ (R \in ℝ^{+} \land t \in ℝ) \to ((- R < t \land t < R) \to 0 < 1 - {(\frac{t}{R})}^{2})$
323	322	exp4b	$⊢ R \in ℝ^{+} \to (t \in ℝ \to (- R < t \to (t < R \to 0 < 1 - {(\frac{t}{R})}^{2})))$
324	323	3impd	$⊢ R \in ℝ^{+} \to ((t \in ℝ \land - R < t \land t < R) \to 0 < 1 - {(\frac{t}{R})}^{2})$
325	25 324	sylbid	$⊢ R \in ℝ^{+} \to (t \in (- R, R) \to 0 < 1 - {(\frac{t}{R})}^{2})$
326	325	imp	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 0 < 1 - {(\frac{t}{R})}^{2}$
327	284 283 326	ltled	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 0 \leq 1 - {(\frac{t}{R})}^{2}$
328	275 277 283 327	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}}$
329	264 13 14	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}$
330	264	mulridd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} \cdot 1 = R^{2}$
331	5 7 9	sqdivd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to {(\frac{t}{R})}^{2} = \frac{t^{2}}{R^{2}}$
332	331	oveq2d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} {(\frac{t}{R})}^{2} = R^{2} (\frac{t^{2}}{R^{2}})$
333	4	sqcld	$⊢ t \in (- R, R) \to t^{2} \in ℂ$
334	333	adantl	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to t^{2} \in ℂ$
335		sqne0	$⊢ R \in ℂ \to (R^{2} \neq 0 \leftrightarrow R \neq 0)$
336	6 335	syl	$⊢ R \in ℝ^{+} \to (R^{2} \neq 0 \leftrightarrow R \neq 0)$
337	8 336	mpbird	$⊢ R \in ℝ^{+} \to R^{2} \neq 0$
338	337	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} \neq 0$
339	334 264 338	divcan2d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} (\frac{t^{2}}{R^{2}}) = t^{2}$
340	332 339	eqtrd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} {(\frac{t}{R})}^{2} = t^{2}$
341	330 340	oveq12d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} \cdot 1 - R^{2} {(\frac{t}{R})}^{2} = R^{2} - t^{2}$
342	329 341	eqtrd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} (1 - {(\frac{t}{R})}^{2}) = R^{2} - t^{2}$
343	342	fveq2d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \sqrt{R^{2} (1 - {(\frac{t}{R})}^{2})} = \sqrt{R^{2} - t^{2}}$
344	20 290	sqrtsqd	$⊢ R \in ℝ^{+} \to \sqrt{R^{2}} = R$
345	344	adantr	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to \sqrt{R^{2}} = R$
346	345	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}}$
347	328 343 346	3eqtr3rd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R \sqrt{1 - {(\frac{t}{R})}^{2}} = \sqrt{R^{2} - t^{2}}$
348	347	oveq2d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to 2 R \sqrt{1 - {(\frac{t}{R})}^{2}} = 2 \sqrt{R^{2} - t^{2}}$
349	272 273 348	3eqtrd	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} (\frac{1}{R}) 2 \sqrt{1 - {(\frac{t}{R})}^{2}} = 2 \sqrt{R^{2} - t^{2}}$
350	263 265 349	3eqtr2d	$⊢ (R \in ℝ^{+} \land t \in (- R, R)) \to R^{2} 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R}) = 2 \sqrt{R^{2} - t^{2}}$
351	350	mpteq2dva	$⊢ R \in ℝ^{+} \to (t \in (- R, R) ⟼ R^{2} 2 \sqrt{1 - {(\frac{t}{R})}^{2}} (\frac{1}{R})) = (t \in (- R, R) ⟼ 2 \sqrt{R^{2} - t^{2}})$
352	257 351	eqtrd	$⊢ R \in ℝ^{+} \to \frac{d (t \in (- R, R)⟼ R^{2} (arcsin (\frac{t}{R}) + (\frac{t}{R}) \sqrt{1 - {(\frac{t}{R})}^{2}}))}{d_{ℝ} t} = (t \in (- R, R) ⟼ 2 \sqrt{R^{2} - t^{2}})$

Metamath Proof Explorer

Theorem areacirclem1

Proof