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 38245

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 13023	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
2	1	sqcld 14176	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
3		rpre 13021	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
4	3	renegcld 11637	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → -𝑅 ∈ ℝ)
5		iccssre 13452	. . . . 5 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
6	4, 3, 5	syl2anc 595	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℝ)
7		ax-resscn 11153	. . . 4 ⊢ ℝ ⊆ ℂ
8	6, 7	sstrdi 3957	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (-𝑅[,]𝑅) ⊆ ℂ)
9		ssid 3967	. . . 4 ⊢ ℂ ⊆ ℂ
10	9	a1i 11	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → ℂ ⊆ ℂ)
11		cncfmptc 25036	. . 3 ⊢ (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
12	2, 8, 10, 11	syl3anc 1396	. 2 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13		eqid 2769	. . 3 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
14	13	addcn 24988	. . . 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 3945	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
17	1	adantr 485	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18		rpne0 13029	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ≠ 0)
19	18	adantr 485	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
20	16, 17, 19	divcld 11987	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21		asinval 27009	. . . . . . 7 ⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
22	20, 21	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23		ax-icn 11155	. . . . . . . . . . . 12 ⊢ i ∈ ℂ
24	23	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
25	24, 20	mulcld 11225	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26		1cnd 11198	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
27	20	sqcld 14176	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
28	26, 27	subcld 11565	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
29	28	sqrtcld 15487	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
30	25, 29	addcld 11224	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31		0lt1 11732	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
32		simp3 1154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
33	32	oveq1d 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
34	1, 18	div0d 11986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → (0 / 𝑅) = 0)
35	34	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
36	33, 35	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
37	36	oveq2d 7424	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38		it0e0 12463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i · 0) = 0
39	37, 38	eqtrdi 2820	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
40	36	oveq1d 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
41	40	oveq2d 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
42	41	fveq2d 6883	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43		sq0 14224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑2) = 0
44	43	oveq2i 7419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 − (0↑2)) = (1 − 0)
45		1m0e1 12356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 − 0) = 1
46	44, 45	eqtri 2792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − (0↑2)) = 1
47	46	fveq2i 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (√‘(1 − (0↑2))) = (√‘1)
48		sqrt1 15318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (√‘1) = 1
49	47, 48	eqtri 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (√‘(1 − (0↑2))) = 1
50	42, 49	eqtrdi 2820	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
51	39, 50	oveq12d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52		0p1e1 12357	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
53	51, 52	eqtrdi 2820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
54	53	breq2d 5122	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55		0red 11207	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56		1red 11205	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
57	53, 56	eqeltrd 2869	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
58	55, 57	ltnled 11353	. . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
62	61	olcd 887	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63		inelr 12204	. . . . . . . . . . . . . 14 ⊢ ¬ i ∈ ℝ
64	25, 29	pncand 11566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65	64	3adant3 1148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
66	65	oveq1d 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
67	23	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68	20	3adant3 1148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
69	1	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70	16	3adant3 1148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71		simp3 1154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
72	69, 70, 71	divcld 11987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
73	67, 68, 72	mulassd 11228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
74	66, 73	eqtrd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75	18	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
76	70, 69, 71, 75	divcan6d 12006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
77	76	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
78	67	mulridd 11222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
79	74, 77, 78	3eqtrrd 2809	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
80	79	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82		1red 11205	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
83	6	sselda 3945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
84	3	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
85	83, 84, 19	redivcld 12039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
86	85	resqcld 14157	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
87	82, 86	resubcld 11638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88		elicc2 13434	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
89	4, 3, 88	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
90		1red 11205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
91		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
92	3	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
93	18	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ≠ 0)
94	91, 92, 93	redivcld 12039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
95	94	resqcld 14157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
96	90, 95	subge0d 11800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97		recn 11186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
98	97	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
99	1	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
100	98, 99, 93	sqdivd 14191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101	100	breq1d 5120	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102		resqcl 14156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103	102	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
104	3	resqcld 14157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
105		rpgt0 13025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑅 ∈ ℝ⁺ → 0 < 𝑅)
106		0red 11207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ∈ ℝ)
107		0le0 12338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 0 ≤ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 0)
109		rpge0 13026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
110	106, 3, 108, 109	lt2sqd 14288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑅 ∈ ℝ⁺ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
111	43	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑅 ∈ ℝ⁺ → (0↑2) = 0)
112	111	breq1d 5120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ⁺)
116	115	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ⁺)
117	103, 90, 116	ledivmuld 13109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118		absresq 15349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119	118	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
120	2	mulridd 11222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) · 1) = (𝑅↑2))
121	119, 120	breqan12rd 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
122	97	abscld 15486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123	122	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
124	97	absge0d 15494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125	124	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126	109	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127	123, 92, 125, 126	le2sqd 14289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
128	91, 92	absled 15480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
134	133	3impd 1365	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
135	89, 134	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136	135	imp 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
137	87, 136	resqrtcld 15465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
138	137	3adant3 1148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139	138	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
140	81, 139	resubcld 11638	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
141	3	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142	83	3adant3 1148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143	141, 142, 71	redivcld 12039	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144	143	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145	140, 144	remulcld 11235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
146	80, 145	eqeltrd 2869	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147	146	ex 417	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
148	147	3expa 1134	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
149	63, 148	mtoi 202	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150	149	orcd 886	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
151	62, 150	pm2.61dane 3051	. . . . . . . . . . 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 11262	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
155		0re 11206	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
156		elioc2 13432	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157	154, 155, 156	mp2an 704	. . . . . . . . . . 11 ⊢ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158		3simpb 1165	. . . . . . . . . . 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 3924	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162		fvres 6898	. . . . . . . 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 7424	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
165	22, 164	eqtr4d 2807	. . . . 5 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166	165	mpteq2dva 5205	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167		negicn 11454	. . . . . . 7 ⊢ -i ∈ ℂ
168	167	a1i 11	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → -i ∈ ℂ)
169		cncfmptc 25036	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170	168, 8, 10, 169	syl3anc 1396	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
171	13	cnfldtopon 24904	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
172	171	a1i 11	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
173		resttopon 23283	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174	172, 8, 173	syl2anc 595	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175	161	fmpttd 7108	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
176		difssd 4099	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
177	16, 17, 19	divrec2d 11991	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
178	177	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
179	1, 18	reccld 11980	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → (1 / 𝑅) ∈ ℂ)
180	179	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
181	24, 180, 16	mulassd 11228	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
182	178, 181	eqtr4d 2807	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
183	182	mpteq2dva 5205	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
184	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → i ∈ ℂ)
185	184, 179	mulcld 11225	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → (i · (1 / 𝑅)) ∈ ℂ)
186		cncfmptc 25036	. . . . . . . . . . . . . 14 ⊢ (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
187	185, 8, 10, 186	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188		cncfmptid 25037	. . . . . . . . . . . . . 14 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
189	8, 10, 188	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
190	187, 189	mulcncf 25570	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191	183, 190	eqeltrd 2869	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
192	17, 29	mulcld 11225	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
193	192, 17, 19	divrec2d 11991	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
194	29, 17, 19	divcan3d 11992	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
195	104	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
196	3	sqge0d 14169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ (𝑅↑2))
197	196	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
198	195, 197, 87, 136	sqrtmuld 15472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
199	2	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
200	199, 26, 27	subdid 11666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
201	199	mulridd 11222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
202	16, 17, 19	sqdivd 14191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
203	202	oveq2d 7424	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
204	16	sqcld 14176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
205		sqne0 14155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
206	1, 205	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
207	18, 206	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ≠ 0)
208	207	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
209	204, 199, 208	divcan2d 11989	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
210	203, 209	eqtrd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
211	201, 210	oveq12d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
212	200, 211	eqtrd 2804	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213	212	fveq2d 6883	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
214	109	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
215	84, 214	sqrtsqd 15467	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
216	215	oveq1d 7423	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
217	198, 213, 216	3eqtr3rd 2813	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
218	217	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
219	193, 194, 218	3eqtr3d 2812	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220	219	mpteq2dva 5205	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
221		cncfmptc 25036	. . . . . . . . . . . . . 14 ⊢ (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
222	179, 8, 10, 221	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223		areacirclem2 38243	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
224	3, 109, 223	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
225	222, 224	mulcncf 25570	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226	220, 225	eqeltrd 2869	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
227	13, 15, 191, 226	cncfmpt2f 25039	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
228		cncfcdm 25022	. . . . . . . . . 10 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
229	176, 227, 228	syl2anc 595	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230	175, 229	mpbird 260	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
231		eqid 2769	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) = ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅))
232		eqid 2769	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))
233	13, 231, 232	cncfcn 25034	. . . . . . . . 9 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
234	8, 176, 233	syl2anc 595	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
235	230, 234	eleqtrd 2871	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0)))))
236		eqid 2769	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
237	236	logcn 26774	. . . . . . . . 9 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
238		difss 4098	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ ℂ
239		eqid 2769	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
240	13, 232, 239	cncfcn 25034	. . . . . . . . . 10 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
241	238, 9, 240	mp2an 704	. . . . . . . . 9 ⊢ ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
242	237, 241	eleqtri 2867	. . . . . . . 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 23786	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
245	13, 231, 239	cncfcn 25034	. . . . . . 7 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
246	8, 10, 245	syl2anc 595	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
247	244, 246	eleqtrrd 2872	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
248	170, 247	mulcncf 25570	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249	166, 248	eqeltrd 2869	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250	219	oveq2d 7424	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
251	199, 204	subcld 11565	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
252	251	sqrtcld 15487	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
253	20, 180, 252	mulassd 11228	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
254	16, 17, 19	divrecd 11990	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
255	254	oveq1d 7423	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
256	16, 180, 180	mulassd 11228	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
257	255, 256	eqtrd 2804	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258	257	oveq1d 7423	. . . . . 6 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
259	250, 253, 258	3eqtr2d 2810	. . . . 5 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260	259	mpteq2dva 5205	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
261	179, 179	mulcld 11225	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
262		cncfmptc 25036	. . . . . . 7 ⊢ ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
263	261, 8, 10, 262	syl3anc 1396	. . . . . 6 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264	189, 263	mulcncf 25570	. . . . 5 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265	264, 224	mulcncf 25570	. . . 4 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266	260, 265	eqeltrd 2869	. . 3 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
267	13, 15, 249, 266	cncfmpt2f 25039	. 2 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
268	12, 267	mulcncf 25570	1 ⊢ (𝑅 ∈ ℝ⁺ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∖ cdif 3910 ⊆ wss 3913 class class class wbr 5110 ↦ cmpt 5193 ↾ cres 5661 ⟶wf 6530 ‘cfv 6534 (class class class)co 7408 ℂcc 11094 ℝcr 11095 0cc0 11096 1c1 11097 ici 11098 + caddc 11099 · cmul 11101 -∞cmnf 11237 ℝ^*cxr 11238 < clt 11239 ≤ cle 11240 − cmin 11437 -cneg 11438 / cdiv 11867 2c2 12291 ℝ⁺crp 13012 (,]cioc 13369 [,]cicc 13371 ↑cexp 14093 √csqrt 15280 abscabs 15281 ↾_t crest 17469 TopOpenctopn 17470 ℂ_fldccnfld 21487 TopOnctopon 23032 Cn ccn 23346 ×_t ctx 23682 –cn→ccncf 25000 logclog 26681 arcsincasin 26989

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-inf2 9606 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173 ax-pre-sup 11174 ax-addf 11175

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-isom 6543 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7672 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-er 8690 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-fi 9367 df-sup 9398 df-inf 9399 df-oi 9468 df-card 9921 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-div 11868 df-nn 12230 df-2 12299 df-3 12300 df-4 12301 df-5 12302 df-6 12303 df-7 12304 df-8 12305 df-9 12306 df-n0 12501 df-z 12588 df-dec 12708 df-uz 12859 df-q 12969 df-rp 13013 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13372 df-ioc 13373 df-ico 13374 df-icc 13375 df-fz 13532 df-fzo 13679 df-fl 13821 df-mod 13899 df-seq 14034 df-exp 14094 df-fac 14306 df-bc 14335 df-hash 14363 df-shft 15100 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-limsup 15518 df-clim 15535 df-rlim 15536 df-sum 15734 df-ef 16117 df-sin 16119 df-cos 16120 df-tan 16121 df-pi 16122 df-struct 17203 df-sets 17220 df-slot 17238 df-ndx 17250 df-base 17266 df-ress 17287 df-plusg 17319 df-mulr 17320 df-starv 17321 df-sca 17322 df-vsca 17323 df-ip 17324 df-tset 17325 df-ple 17326 df-ds 17328 df-unif 17329 df-hom 17330 df-cco 17331 df-rest 17471 df-topn 17472 df-0g 17490 df-gsum 17491 df-topgen 17492 df-pt 17493 df-prds 17496 df-xrs 17552 df-qtop 17557 df-imas 17558 df-xps 17560 df-mre 17634 df-mrc 17635 df-acs 17637 df-mgm 18694 df-sgrp 18773 df-mnd 18789 df-submnd 18838 df-mulg 19130 df-cntz 19383 df-cmn 19848 df-psmet 21479 df-xmet 21480 df-met 21481 df-bl 21482 df-mopn 21483 df-fbas 21484 df-fg 21485 df-cnfld 21488 df-top 23016 df-topon 23033 df-topsp 23055 df-bases 23068 df-cld 23141 df-ntr 23142 df-cls 23143 df-nei 23220 df-lp 23258 df-perf 23259 df-cn 23349 df-cnp 23350 df-haus 23437 df-cmp 23509 df-tx 23684 df-hmeo 23877 df-fil 23968 df-fm 24060 df-flim 24061 df-flf 24062 df-xms 24442 df-ms 24443 df-tms 24444 df-cncf 25002 df-limc 25990 df-dv 25991 df-log 26683 df-cxp 26684 df-asin 26992

This theorem is referenced by: areacirc 38247

W3C validator