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

Proof

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

Metamath Proof Explorer

Theorem areacirclem4

Proof