areacirclem2 - Mathbox for Brendan Leahy

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

Theorem areacirclem2 37703

Description: Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)

**Assertion**
Ref	Expression
areacirclem2	⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))

Distinct variable group: 𝑡,𝑅

Proof of Theorem areacirclem2 Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		resqcl 14089	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
2	1	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑅↑2) ∈ ℝ)
3	2	adantr 480	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
4		renegcl 11485	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
5		iccssre 13390	. . . . . . . . . 10 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
6	4, 5	mpancom 688	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
7	6	sselda 3946	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
8	7	resqcld 14090	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
9	8	adantlr 715	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
10	3, 9	resubcld 11606	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
11		elicc2 13372	. . . . . . . . 9 ⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
12	4, 11	mpancom 688	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
13	12	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
14	1	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
15		resqcl 14089	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
16	15	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
17	14, 16	subge0d 11768	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
18		absresq 15268	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
19	18	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
20	19	breq1d 5117	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
21	17, 20	bitr4d 282	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
22		recn 11158	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
23	22	abscld 15405	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
24	23	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
25		simp1 1136	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
26	22	absge0d 15413	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
27	26	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
28		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
29	24, 25, 27, 28	le2sqd 14222	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
30		simp3 1138	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
31	30, 25	absled 15399	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
32	21, 29, 31	3bitr2d 307	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
33	32	biimprd 248	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
34	33	3expa 1118	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
35	34	exp4b 430	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
36	35	3impd 1349	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
37	13, 36	sylbid 240	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
38	37	imp 406	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
39		elrege0 13415	. . . . 5 ⊢ (((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞) ↔ (((𝑅↑2) − (𝑡↑2)) ∈ ℝ ∧ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
40	10, 38, 39	sylanbrc 583	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞))
41		fvres 6877	. . . 4 ⊢ (((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞) → ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
42	40, 41	syl 17	. . 3 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
43	42	mpteq2dva 5200	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))))
44		eqid 2729	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
45	44	cnfldtopon 24670	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
46		ax-resscn 11125	. . . . . . 7 ⊢ ℝ ⊆ ℂ
47	6, 46	sstrdi 3959	. . . . . 6 ⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℂ)
48		resttopon 23048	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
49	45, 47, 48	sylancr 587	. . . . 5 ⊢ (𝑅 ∈ ℝ → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
50	49	adantr 480	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
51	47	resmptd 6011	. . . . . . 7 ⊢ (𝑅 ∈ ℝ → ((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ↾ (-𝑅[,]𝑅)) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))))
52	45	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
53		recn 11158	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
54	53	sqcld 14109	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
55	52, 52, 54	cnmptc 23549	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ℂ ↦ (𝑅↑2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
56	44	sqcn 24767	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℂ ↦ (𝑡↑2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld))
57	56	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ℂ ↦ (𝑡↑2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
58	44	subcn 24755	. . . . . . . . . 10 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
60	52, 55, 57, 59	cnmpt12f 23553	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
61	45	toponunii 22803	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
62	61	cnrest 23172	. . . . . . . 8 ⊢ (((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ↾ (-𝑅[,]𝑅)) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
63	60, 47, 62	syl2anc 584	. . . . . . 7 ⊢ (𝑅 ∈ ℝ → ((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ↾ (-𝑅[,]𝑅)) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
64	51, 63	eqeltrrd 2829	. . . . . 6 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
65	64	adantr 480	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
66	45	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
67		eqid 2729	. . . . . . . 8 ⊢ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2)))
68	67	rnmpt 5921	. . . . . . 7 ⊢ ran (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) = {𝑢 ∣ ∃𝑡 ∈ (-𝑅[,]𝑅)𝑢 = ((𝑅↑2) − (𝑡↑2))}
69		simp3 1138	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑢 = ((𝑅↑2) − (𝑡↑2))) → 𝑢 = ((𝑅↑2) − (𝑡↑2)))
70	40	3adant3 1132	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑢 = ((𝑅↑2) − (𝑡↑2))) → ((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞))
71	69, 70	eqeltrd 2828	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑢 = ((𝑅↑2) − (𝑡↑2))) → 𝑢 ∈ (0[,)+∞))
72	71	rexlimdv3a 3138	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (∃𝑡 ∈ (-𝑅[,]𝑅)𝑢 = ((𝑅↑2) − (𝑡↑2)) → 𝑢 ∈ (0[,)+∞)))
73	72	abssdv 4031	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → {𝑢 ∣ ∃𝑡 ∈ (-𝑅[,]𝑅)𝑢 = ((𝑅↑2) − (𝑡↑2))} ⊆ (0[,)+∞))
74	68, 73	eqsstrid 3985	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ran (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ⊆ (0[,)+∞))
75		rge0ssre 13417	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
76	75, 46	sstri 3956	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℂ
77	76	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0[,)+∞) ⊆ ℂ)
78		cnrest2 23173	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ran (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ⊆ (0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)))))
79	66, 74, 77, 78	syl3anc 1373	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)))))
80	65, 79	mpbid 232	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞))))
81		ssid 3969	. . . . . . . 8 ⊢ ℂ ⊆ ℂ
82		cncfss 24792	. . . . . . . 8 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((0[,)+∞)–cn→ℝ) ⊆ ((0[,)+∞)–cn→ℂ))
83	46, 81, 82	mp2an 692	. . . . . . 7 ⊢ ((0[,)+∞)–cn→ℝ) ⊆ ((0[,)+∞)–cn→ℂ)
84		resqrtcn 26659	. . . . . . 7 ⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ)
85	83, 84	sselii 3943	. . . . . 6 ⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℂ)
86		eqid 2729	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) = ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞))
87		eqid 2729	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
88	44, 86, 87	cncfcn 24803	. . . . . . 7 ⊢ (((0[,)+∞) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((0[,)+∞)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
89	76, 81, 88	mp2an 692	. . . . . 6 ⊢ ((0[,)+∞)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
90	85, 89	eleqtri 2826	. . . . 5 ⊢ (√ ↾ (0[,)+∞)) ∈ (((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
91	90	a1i 11	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (√ ↾ (0[,)+∞)) ∈ (((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
92	50, 80, 91	cnmpt11f 23551	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2)))) ∈ (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
93		eqid 2729	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) = ((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅))
94	44, 93, 87	cncfcn 24803	. . . . 5 ⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
95	47, 81, 94	sylancl 586	. . . 4 ⊢ (𝑅 ∈ ℝ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
96	95	adantr 480	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
97	92, 96	eleqtrrd 2831	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
98	43, 97	eqeltrrd 2829	1 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 {cab 2707 ∃wrex 3053 ⊆ wss 3914 class class class wbr 5107 ↦ cmpt 5188 ran crn 5639 ↾ cres 5640 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 +∞cpnf 11205 ≤ cle 11209 − cmin 11405 -cneg 11406 2c2 12241 [,)cico 13308 [,]cicc 13309 ↑cexp 14026 √csqrt 15199 abscabs 15200 ↾_t crest 17383 TopOpenctopn 17384 ℂ_fldccnfld 21264 TopOnctopon 22797 Cn ccn 23111 ×_t ctx 23447 –cn→ccncf 24769

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-fac 14239 df-bc 14268 df-hash 14296 df-shft 15033 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-limsup 15437 df-clim 15454 df-rlim 15455 df-sum 15653 df-ef 16033 df-sin 16035 df-cos 16036 df-tan 16037 df-pi 16038 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17465 df-qtop 17470 df-imas 17471 df-xps 17473 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19249 df-cmn 19712 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-fbas 21261 df-fg 21262 df-cnfld 21265 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-nei 22985 df-lp 23023 df-perf 23024 df-cn 23114 df-cnp 23115 df-haus 23202 df-cmp 23274 df-tx 23449 df-hmeo 23642 df-fil 23733 df-fm 23825 df-flim 23826 df-flf 23827 df-xms 24208 df-ms 24209 df-tms 24210 df-cncf 24771 df-limc 25767 df-dv 25768 df-log 26465 df-cxp 26466

This theorem is referenced by: areacirclem3 37704 areacirclem4 37705 areacirc 37707

W3C validator