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 35795

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 12669	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
2	1	sqcld 13790	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
3		rpre 12667	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
4	3	renegcld 11332	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
5		iccssre 13090	. . . . 5 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
6	4, 3, 5	syl2anc 583	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
7		ax-resscn 10859	. . . 4 ⊢ ℝ ⊆ ℂ
8	6, 7	sstrdi 3929	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℂ)
9		ssid 3939	. . . 4 ⊢ ℂ ⊆ ℂ
10	9	a1i 11	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → ℂ ⊆ ℂ)
11		cncfmptc 23981	. . 3 ⊢ (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
12	2, 8, 10, 11	syl3anc 1369	. 2 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13		eqid 2738	. . 3 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
14	13	addcn 23934	. . . 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 3917	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
17	1	adantr 480	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18		rpne0 12675	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
20	16, 17, 19	divcld 11681	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21		asinval 25937	. . . . . . 7 ⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
22	20, 21	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23		ax-icn 10861	. . . . . . . . . . . 12 ⊢ i ∈ ℂ
24	23	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
25	24, 20	mulcld 10926	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26		1cnd 10901	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
27	20	sqcld 13790	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
28	26, 27	subcld 11262	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
29	28	sqrtcld 15077	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
30	25, 29	addcld 10925	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31		0lt1 11427	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
32		simp3 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
33	32	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
34	1, 18	div0d 11680	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → (0 / 𝑅) = 0)
35	34	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
36	33, 35	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
37	36	oveq2d 7271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38		it0e0 12125	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i · 0) = 0
39	37, 38	eqtrdi 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
40	36	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
41	40	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
42	41	fveq2d 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43		sq0 13837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑2) = 0
44	43	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 − (0↑2)) = (1 − 0)
45		1m0e1 12024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 − 0) = 1
46	44, 45	eqtri 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − (0↑2)) = 1
47	46	fveq2i 6759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (√‘(1 − (0↑2))) = (√‘1)
48		sqrt1 14911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (√‘1) = 1
49	47, 48	eqtri 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (√‘(1 − (0↑2))) = 1
50	42, 49	eqtrdi 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
51	39, 50	oveq12d 7273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52		0p1e1 12025	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
53	51, 52	eqtrdi 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
54	53	breq2d 5082	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55		0red 10909	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56		1red 10907	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
57	53, 56	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
58	55, 57	ltnled 11052	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
59	54, 58	bitr3d 280	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
60	31, 59	mpbii 232	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
61	60	3expa 1116	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
62	61	olcd 870	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63		inelr 11893	. . . . . . . . . . . . . 14 ⊢ ¬ i ∈ ℝ
64	25, 29	pncand 11263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65	64	3adant3 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
66	65	oveq1d 7270	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
67	23	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68	20	3adant3 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
69	1	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70	16	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71		simp3 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
72	69, 70, 71	divcld 11681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
73	67, 68, 72	mulassd 10929	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
74	66, 73	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75	18	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
76	70, 69, 71, 75	divcan6d 11700	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
77	76	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
78	67	mulid1d 10923	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
79	74, 77, 78	3eqtrrd 2783	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
80	79	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82		1red 10907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
83	6	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
84	3	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
85	83, 84, 19	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
86	85	resqcld 13893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
87	82, 86	resubcld 11333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88		elicc2 13073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89	4, 3, 88	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
90		1red 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
91		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
92	3	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
93	18	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ≠ 0)
94	91, 92, 93	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
95	94	resqcld 13893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
96	90, 95	subge0d 11495	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97		recn 10892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
98	97	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
99	1	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
100	98, 99, 93	sqdivd 13805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101	100	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102		resqcl 13772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103	102	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
104	3	resqcld 13893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
105		rpgt0 12671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑅 ∈ ℝ⁺ → 0 < 𝑅)
106		0red 10909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ∈ ℝ)
107		0le0 12004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 0 ≤ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 0)
109		rpge0 12672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
110	106, 3, 108, 109	lt2sqd 13901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑅 ∈ ℝ⁺ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
111	43	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → (0↑2) = 0)
112	111	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑅 ∈ ℝ⁺ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
113	110, 112	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑅 ∈ ℝ⁺ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
114	105, 113	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑅 ∈ ℝ⁺ → 0 < (𝑅↑2))
115	104, 114	elrpd 12698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ⁺)
116	115	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ⁺)
117	103, 90, 116	ledivmuld 12754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118		absresq 14942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119	118	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
120	2	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · 1) = (𝑅↑2))
121	119, 120	breqan12rd 5087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
122	97	abscld 15076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123	122	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
124	97	absge0d 15084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125	124	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126	109	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127	123, 92, 125, 126	le2sqd 13902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
128	91, 92	absled 15070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
129	121, 127, 128	3bitr2d 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
130	117, 129	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
131	96, 101, 130	3bitrrd 305	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
132	131	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
133	132	exp4b 430	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
134	133	3impd 1346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
135	89, 134	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136	135	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
137	87, 136	resqrtcld 15057	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
138	137	3adant3 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139	138	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
140	81, 139	resubcld 11333	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
141	3	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142	83	3adant3 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143	141, 142, 71	redivcld 11733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144	143	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145	140, 144	remulcld 10936	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
146	80, 145	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147	146	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
148	147	3expa 1116	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
149	63, 148	mtoi 198	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150	149	orcd 869	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
151	62, 150	pm2.61dane 3031	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
152		ianor 978	. . . . . . . . . . 11 ⊢ (¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
153	151, 152	sylibr 233	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
154		mnfxr 10963	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
155		0re 10908	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
156		elioc2 13071	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157	154, 155, 156	mp2an 688	. . . . . . . . . . 11 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158		3simpb 1147	. . . . . . . . . . 11 ⊢ ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
159	157, 158	sylbi 216	. . . . . . . . . 10 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
160	153, 159	nsyl 140	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0))
161	30, 160	eldifd 3894	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162		fvres 6775	. . . . . . . 8 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))
163	161, 162	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))
164	163	oveq2d 7271	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
165	22, 164	eqtr4d 2781	. . . . 5 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166	165	mpteq2dva 5170	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167		negicn 11152	. . . . . . 7 ⊢ -i ∈ ℂ
168	167	a1i 11	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → -i ∈ ℂ)
169		cncfmptc 23981	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170	168, 8, 10, 169	syl3anc 1369	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
171	13	cnfldtopon 23852	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
172	171	a1i 11	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
173		resttopon 22220	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174	172, 8, 173	syl2anc 583	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175	161	fmpttd 6971	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
176		difssd 4063	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
177	16, 17, 19	divrec2d 11685	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
178	177	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
179	1, 18	reccld 11674	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 / 𝑅) ∈ ℂ)
180	179	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
181	24, 180, 16	mulassd 10929	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
182	178, 181	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
183	182	mpteq2dva 5170	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
184	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → i ∈ ℂ)
185	184, 179	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (i · (1 / 𝑅)) ∈ ℂ)
186		cncfmptc 23981	. . . . . . . . . . . . . 14 ⊢ (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
187	185, 8, 10, 186	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188		cncfmptid 23982	. . . . . . . . . . . . . 14 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
189	8, 10, 188	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
190	187, 189	mulcncf 24515	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191	183, 190	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
192	17, 29	mulcld 10926	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
193	192, 17, 19	divrec2d 11685	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
194	29, 17, 19	divcan3d 11686	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
195	104	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
196	3	sqge0d 13894	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅↑2))
197	196	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
198	195, 197, 87, 136	sqrtmuld 15064	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
199	2	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
200	199, 26, 27	subdid 11361	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
201	199	mulid1d 10923	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
202	16, 17, 19	sqdivd 13805	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
203	202	oveq2d 7271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
204	16	sqcld 13790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
205		sqne0 13771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
206	1, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
207	18, 206	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ≠ 0)
208	207	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
209	204, 199, 208	divcan2d 11683	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
210	203, 209	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
211	201, 210	oveq12d 7273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
212	200, 211	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213	212	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
214	109	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
215	84, 214	sqrtsqd 15059	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
216	215	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
217	198, 213, 216	3eqtr3rd 2787	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
218	217	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
219	193, 194, 218	3eqtr3d 2786	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220	219	mpteq2dva 5170	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
221		cncfmptc 23981	. . . . . . . . . . . . . 14 ⊢ (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
222	179, 8, 10, 221	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223		areacirclem2 35793	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
224	3, 109, 223	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
225	222, 224	mulcncf 24515	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226	220, 225	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
227	13, 15, 191, 226	cncfmpt2f 23984	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
228		cncffvrn 23967	. . . . . . . . . 10 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
229	176, 227, 228	syl2anc 583	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230	175, 229	mpbird 256	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
231		eqid 2738	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) = ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅))
232		eqid 2738	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))
233	13, 231, 232	cncfcn 23979	. . . . . . . . 9 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
234	8, 176, 233	syl2anc 583	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
235	230, 234	eleqtrd 2841	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
236		eqid 2738	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
237	236	logcn 25707	. . . . . . . . 9 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
238		difss 4062	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ ℂ
239		eqid 2738	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
240	13, 232, 239	cncfcn 23979	. . . . . . . . . 10 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
241	238, 9, 240	mp2an 688	. . . . . . . . 9 ⊢ ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
242	237, 241	eleqtri 2837	. . . . . . . 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 22723	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
245	13, 231, 239	cncfcn 23979	. . . . . . 7 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
246	8, 10, 245	syl2anc 583	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
247	244, 246	eleqtrrd 2842	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
248	170, 247	mulcncf 24515	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249	166, 248	eqeltrd 2839	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250	219	oveq2d 7271	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
251	199, 204	subcld 11262	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
252	251	sqrtcld 15077	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
253	20, 180, 252	mulassd 10929	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
254	16, 17, 19	divrecd 11684	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
255	254	oveq1d 7270	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
256	16, 180, 180	mulassd 10929	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
257	255, 256	eqtrd 2778	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258	257	oveq1d 7270	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
259	250, 253, 258	3eqtr2d 2784	. . . . 5 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260	259	mpteq2dva 5170	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
261	179, 179	mulcld 10926	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
262		cncfmptc 23981	. . . . . . 7 ⊢ ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
263	261, 8, 10, 262	syl3anc 1369	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264	189, 263	mulcncf 24515	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265	264, 224	mulcncf 24515	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266	260, 265	eqeltrd 2839	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
267	13, 15, 249, 266	cncfmpt2f 23984	. 2 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
268	12, 267	mulcncf 24515	1 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∖ cdif 3880 ⊆ wss 3883 class class class wbr 5070 ↦ cmpt 5153 ↾ cres 5582 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 ici 10804 + caddc 10805 · cmul 10807 -∞cmnf 10938 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 -cneg 11136 / cdiv 11562 2c2 11958 ℝ⁺crp 12659 (,]cioc 13009 [,]cicc 13011 ↑cexp 13710 √csqrt 14872 abscabs 14873 ↾_t crest 17048 TopOpenctopn 17049 ℂ_fldccnfld 20510 TopOnctopon 21967 Cn ccn 22283 ×_t ctx 22619 –cn→ccncf 23945 logclog 25615 arcsincasin 25917

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ioc 13013 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-fac 13916 df-bc 13945 df-hash 13973 df-shft 14706 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-limsup 15108 df-clim 15125 df-rlim 15126 df-sum 15326 df-ef 15705 df-sin 15707 df-cos 15708 df-tan 15709 df-pi 15710 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-hom 16912 df-cco 16913 df-rest 17050 df-topn 17051 df-0g 17069 df-gsum 17070 df-topgen 17071 df-pt 17072 df-prds 17075 df-xrs 17130 df-qtop 17135 df-imas 17136 df-xps 17138 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-submnd 18346 df-mulg 18616 df-cntz 18838 df-cmn 19303 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-fbas 20507 df-fg 20508 df-cnfld 20511 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-nei 22157 df-lp 22195 df-perf 22196 df-cn 22286 df-cnp 22287 df-haus 22374 df-cmp 22446 df-tx 22621 df-hmeo 22814 df-fil 22905 df-fm 22997 df-flim 22998 df-flf 22999 df-xms 23381 df-ms 23382 df-tms 23383 df-cncf 23947 df-limc 24935 df-dv 24936 df-log 25617 df-cxp 25618 df-asin 25920

This theorem is referenced by: areacirc 35797

W3C validator