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	⊢ ( 𝑅 ∈ ℝ⁺ → ( ℝ D ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑡 / 𝑅 ) ) + ( ( 𝑡 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑡 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ) = ( 𝑡 ∈ ( - 𝑅 (,) 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem areacirclem1

Proof