areacirclem4 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > areacirclem4		Structured version Visualization version GIF version

Theorem areacirclem4 38419

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.)

**Assertion**
Ref	Expression
areacirclem4	⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))

Distinct variable group: 𝑡,𝑅

**Proof of Theorem areacirclem4**
Step	Hyp	Ref	Expression
1		rpcn 13043	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
2	1	sqcld 14198	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
3		rpre 13041	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
4	3	renegcld 11656	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
5		iccssre 13472	. . . . 5 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
6	4, 3, 5	syl2anc 596	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
7		ax-resscn 11172	. . . 4 ⊢ ℝ ⊆ ℂ
8	6, 7	sstrdi 3950	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℂ)
9		ssid 3960	. . . 4 ⊢ ℂ ⊆ ℂ
10	9	a1i 11	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → ℂ ⊆ ℂ)
11		cncfmptc 25122	. . 3 ⊢ (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
12	2, 8, 10, 11	syl3anc 1398	. 2 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13		eqid 2765	. . 3 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
14	13	addcn 25074	. . . 4 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
15	14	a1i 11	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
16	8	sselda 3938	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
17	1	adantr 486	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18		rpne0 13049	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
19	18	adantr 486	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
20	16, 17, 19	divcld 12006	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21		asinval 27098	. . . . . . 7 ⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
22	20, 21	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23		ax-icn 11174	. . . . . . . . . . . 12 ⊢ i ∈ ℂ
24	23	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
25	24, 20	mulcld 11244	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26		1cnd 11217	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
27	20	sqcld 14198	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
28	26, 27	subcld 11584	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
29	28	sqrtcld 15515	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
30	25, 29	addcld 11243	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31		0lt1 11751	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
32		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
33	32	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
34	1, 18	div0d 12005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → (0 / 𝑅) = 0)
35	34	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
36	33, 35	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
37	36	oveq2d 7435	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38		it0e0 12482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i · 0) = 0
39	37, 38	eqtrdi 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
40	36	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
41	40	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
42	41	fveq2d 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43		sq0 14246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑2) = 0
44	43	oveq2i 7430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 − (0↑2)) = (1 − 0)
45		1m0e1 12375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 − 0) = 1
46	44, 45	eqtri 2788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − (0↑2)) = 1
47	46	fveq2i 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (√‘(1 − (0↑2))) = (√‘1)
48		sqrt1 15346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (√‘1) = 1
49	47, 48	eqtri 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (√‘(1 − (0↑2))) = 1
50	42, 49	eqtrdi 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
51	39, 50	oveq12d 7437	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52		0p1e1 12376	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
53	51, 52	eqtrdi 2816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
54	53	breq2d 5123	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55		0red 11226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56		1red 11224	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
57	53, 56	eqeltrd 2865	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
58	55, 57	ltnled 11372	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
59	54, 58	bitr3d 284	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
60	31, 59	mpbii 236	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
61	60	3expa 1136	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
62	61	olcd 888	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63		inelr 12223	. . . . . . . . . . . . . 14 ⊢ ¬ i ∈ ℝ
64	25, 29	pncand 11585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65	64	3adant3 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
66	65	oveq1d 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
67	23	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68	20	3adant3 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
69	1	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70	16	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71		simp3 1156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
72	69, 70, 71	divcld 12006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
73	67, 68, 72	mulassd 11247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
74	66, 73	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75	18	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
76	70, 69, 71, 75	divcan6d 12025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
77	76	oveq2d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
78	67	mulridd 11241	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
79	74, 77, 78	3eqtrrd 2805	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
80	79	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82		1red 11224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
83	6	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
84	3	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
85	83, 84, 19	redivcld 12058	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
86	85	resqcld 14179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
87	82, 86	resubcld 11657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88		elicc2 13454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89	4, 3, 88	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
90		1red 11224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
91		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
92	3	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
93	18	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ≠ 0)
94	91, 92, 93	redivcld 12058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
95	94	resqcld 14179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
96	90, 95	subge0d 11819	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97		recn 11205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
98	97	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
99	1	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
100	98, 99, 93	sqdivd 14213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101	100	breq1d 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102		resqcl 14178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103	102	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
104	3	resqcld 14179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
105		rpgt0 13045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑅 ∈ ℝ⁺ → 0 < 𝑅)
106		0red 11226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ∈ ℝ)
107		0le0 12357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 0 ≤ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 0)
109		rpge0 13046	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
110	106, 3, 108, 109	lt2sqd 14310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑅 ∈ ℝ⁺ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
111	43	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → (0↑2) = 0)
112	111	breq1d 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑅 ∈ ℝ⁺ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
113	110, 112	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑅 ∈ ℝ⁺ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
114	105, 113	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑅 ∈ ℝ⁺ → 0 < (𝑅↑2))
115	104, 114	elrpd 13073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ⁺)
116	115	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ⁺)
117	103, 90, 116	ledivmuld 13129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118		absresq 15377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119	118	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
120	2	mulridd 11241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · 1) = (𝑅↑2))
121	119, 120	breqan12rd 5128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
122	97	abscld 15514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123	122	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
124	97	absge0d 15522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125	124	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126	109	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127	123, 92, 125, 126	le2sqd 14311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
128	91, 92	absled 15508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
129	121, 127, 128	3bitr2d 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
130	117, 129	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
131	96, 101, 130	3bitrrd 309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
132	131	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
133	132	exp4b 436	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
134	133	3impd 1367	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
135	89, 134	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136	135	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
137	87, 136	resqrtcld 15493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
138	137	3adant3 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139	138	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
140	81, 139	resubcld 11657	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
141	3	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142	83	3adant3 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143	141, 142, 71	redivcld 12058	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144	143	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145	140, 144	remulcld 11254	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
146	80, 145	eqeltrd 2865	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147	146	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
148	147	3expa 1136	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
149	63, 148	mtoi 202	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150	149	orcd 887	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
151	62, 150	pm2.61dane 3047	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
152		ianor 997	. . . . . . . . . . 11 ⊢ (¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
153	151, 152	sylibr 237	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
154		mnfxr 11281	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
155		0re 11225	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
156		elioc2 13452	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157	154, 155, 156	mp2an 705	. . . . . . . . . . 11 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158		3simpb 1167	. . . . . . . . . . 11 ⊢ ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
159	157, 158	sylbi 220	. . . . . . . . . 10 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
160	153, 159	nsyl 141	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0))
161	30, 160	eldifd 3917	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162		fvres 6904	. . . . . . . 8 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))
163	161, 162	syl 18	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))
164	163	oveq2d 7435	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
165	22, 164	eqtr4d 2803	. . . . 5 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166	165	mpteq2dva 5206	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167		negicn 11473	. . . . . . 7 ⊢ -i ∈ ℂ
168	167	a1i 11	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → -i ∈ ℂ)
169		cncfmptc 25122	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170	168, 8, 10, 169	syl3anc 1398	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
171	13	cnfldtopon 24990	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
172	171	a1i 11	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
173		resttopon 23368	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174	172, 8, 173	syl2anc 596	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175	161	fmpttd 7114	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
176		difssd 4091	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
177	16, 17, 19	divrec2d 12010	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
178	177	oveq2d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
179	1, 18	reccld 11999	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 / 𝑅) ∈ ℂ)
180	179	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
181	24, 180, 16	mulassd 11247	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
182	178, 181	eqtr4d 2803	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
183	182	mpteq2dva 5206	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
184	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → i ∈ ℂ)
185	184, 179	mulcld 11244	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (i · (1 / 𝑅)) ∈ ℂ)
186		cncfmptc 25122	. . . . . . . . . . . . . 14 ⊢ (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
187	185, 8, 10, 186	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188		cncfmptid 25123	. . . . . . . . . . . . . 14 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
189	8, 10, 188	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
190	187, 189	mulcncf 25656	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191	183, 190	eqeltrd 2865	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
192	17, 29	mulcld 11244	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
193	192, 17, 19	divrec2d 12010	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
194	29, 17, 19	divcan3d 12011	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
195	104	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
196	3	sqge0d 14191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅↑2))
197	196	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
198	195, 197, 87, 136	sqrtmuld 15500	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
199	2	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
200	199, 26, 27	subdid 11685	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
201	199	mulridd 11241	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
202	16, 17, 19	sqdivd 14213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
203	202	oveq2d 7435	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
204	16	sqcld 14198	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
205		sqne0 14177	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
206	1, 205	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
207	18, 206	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ≠ 0)
208	207	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
209	204, 199, 208	divcan2d 12008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
210	203, 209	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
211	201, 210	oveq12d 7437	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
212	200, 211	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213	212	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
214	109	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
215	84, 214	sqrtsqd 15495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
216	215	oveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
217	198, 213, 216	3eqtr3rd 2809	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
218	217	oveq2d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
219	193, 194, 218	3eqtr3d 2808	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220	219	mpteq2dva 5206	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
221		cncfmptc 25122	. . . . . . . . . . . . . 14 ⊢ (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
222	179, 8, 10, 221	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223		areacirclem2 38417	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
224	3, 109, 223	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
225	222, 224	mulcncf 25656	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226	220, 225	eqeltrd 2865	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
227	13, 15, 191, 226	cncfmpt2f 25125	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
228		cncfcdm 25108	. . . . . . . . . 10 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
229	176, 227, 228	syl2anc 596	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230	175, 229	mpbird 260	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
231		eqid 2765	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) = ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅))
232		eqid 2765	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))
233	13, 231, 232	cncfcn 25120	. . . . . . . . 9 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
234	8, 176, 233	syl2anc 596	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
235	230, 234	eleqtrd 2867	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
236		eqid 2765	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
237	236	logcn 26863	. . . . . . . . 9 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
238		difss 4090	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ ℂ
239		eqid 2765	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
240	13, 232, 239	cncfcn 25120	. . . . . . . . . 10 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
241	238, 9, 240	mp2an 705	. . . . . . . . 9 ⊢ ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
242	237, 241	eleqtri 2863	. . . . . . . 8 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
243	242	a1i 11	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
244	174, 235, 243	cnmpt11f 23872	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
245	13, 231, 239	cncfcn 25120	. . . . . . 7 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
246	8, 10, 245	syl2anc 596	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
247	244, 246	eleqtrrd 2868	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
248	170, 247	mulcncf 25656	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249	166, 248	eqeltrd 2865	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250	219	oveq2d 7435	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
251	199, 204	subcld 11584	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
252	251	sqrtcld 15515	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
253	20, 180, 252	mulassd 11247	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
254	16, 17, 19	divrecd 12009	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
255	254	oveq1d 7434	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
256	16, 180, 180	mulassd 11247	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
257	255, 256	eqtrd 2800	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258	257	oveq1d 7434	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
259	250, 253, 258	3eqtr2d 2806	. . . . 5 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260	259	mpteq2dva 5206	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
261	179, 179	mulcld 11244	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
262		cncfmptc 25122	. . . . . . 7 ⊢ ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
263	261, 8, 10, 262	syl3anc 1398	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264	189, 263	mulcncf 25656	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265	264, 224	mulcncf 25656	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266	260, 265	eqeltrd 2865	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
267	13, 15, 249, 266	cncfmpt2f 25125	. 2 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
268	12, 267	mulcncf 25656	1 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∖ cdif 3903 ⊆ wss 3906 class class class wbr 5111 ↦ cmpt 5194 ↾ cres 5665 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ℂcc 11113 ℝcr 11114 0cc0 11115 1c1 11116 ici 11117 + caddc 11118 · cmul 11120 -∞cmnf 11256 ℝ^*cxr 11257 < clt 11258 ≤ cle 11259 − cmin 11456 -cneg 11457 / cdiv 11886 2c2 12310 ℝ⁺crp 13032 (,]cioc 13389 [,]cicc 13391 ↑cexp 14115 √csqrt 15308 abscabs 15309 ↾_t crest 17495 TopOpenctopn 17496 ℂ_fldccnfld 21572 TopOnctopon 23117 Cn ccn 23431 ×_t ctx 23768 –cn→ccncf 25086 logclog 26770 arcsincasin 27078

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193 ax-addf 11194

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-fi 9378 df-sup 9409 df-inf 9410 df-oi 9479 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-4 12320 df-5 12321 df-6 12322 df-7 12323 df-8 12324 df-9 12325 df-n0 12520 df-z 12607 df-dec 12728 df-uz 12879 df-q 12989 df-rp 13033 df-xneg 13153 df-xadd 13154 df-xmul 13155 df-ioo 13392 df-ioc 13393 df-ico 13394 df-icc 13395 df-fz 13552 df-fzo 13700 df-fl 13843 df-mod 13921 df-seq 14056 df-exp 14116 df-fac 14328 df-bc 14357 df-hash 14385 df-shft 15128 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-limsup 15546 df-clim 15563 df-rlim 15564 df-sum 15762 df-ef 16143 df-sin 16145 df-cos 16146 df-tan 16147 df-pi 16148 df-struct 17229 df-sets 17246 df-slot 17264 df-ndx 17276 df-base 17292 df-ress 17313 df-plusg 17345 df-mulr 17346 df-starv 17347 df-sca 17348 df-vsca 17349 df-ip 17350 df-tset 17351 df-ple 17352 df-ds 17354 df-unif 17355 df-hom 17356 df-cco 17357 df-rest 17497 df-topn 17498 df-0g 17516 df-gsum 17517 df-topgen 17518 df-pt 17519 df-prds 17522 df-xrs 17578 df-qtop 17583 df-imas 17584 df-xps 17586 df-mre 17660 df-mrc 17661 df-acs 17663 df-mgm 18720 df-sgrp 18809 df-mnd 18825 df-submnd 18879 df-mulg 19178 df-cntz 19431 df-cmn 19896 df-psmet 21564 df-xmet 21565 df-met 21566 df-bl 21567 df-mopn 21568 df-fbas 21569 df-fg 21570 df-cnfld 21573 df-top 23101 df-topon 23118 df-topsp 23140 df-bases 23153 df-cld 23226 df-ntr 23227 df-cls 23228 df-nei 23305 df-lp 23343 df-perf 23344 df-cn 23434 df-cnp 23435 df-haus 23522 df-cmp 23594 df-tx 23770 df-hmeo 23963 df-fil 24054 df-fm 24146 df-flim 24147 df-flf 24148 df-xms 24528 df-ms 24529 df-tms 24530 df-cncf 25088 df-limc 26076 df-dv 26077 df-log 26772 df-cxp 26773 df-asin 27081

This theorem is used by: areacirc 38421

W3C validator