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 38888

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 14305	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
2	1	adantr 486	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑅↑2) ∈ ℝ)
3	2	adantr 486	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
4		renegcl 11658	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
5		iccssre 13598	. . . . . . . . . 10 ⊢ (( -𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ( -𝑅[,]𝑅) ⊆ ℝ)
6	4, 5	mpancom 701	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → ( -𝑅[,]𝑅) ⊆ ℝ)
7	6	sselda 3913	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
8	7	resqcld 14306	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
9	8	adantlr 728	. . . . . 6 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ)
10	3, 9	resubcld 11781	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
11		elicc2 13580	. . . . . . . . 9 ⊢ (( -𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ ( -𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
12	4, 11	mpancom 701	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ( -𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
13	12	adantr 486	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
14	1	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
15		resqcl 14305	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
16	15	3ad2ant3 1153	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
17	14, 16	subge0d 11944	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
18		absresq 15510	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
19	18	3ad2ant3 1153	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
20	19	breq1d 5116	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
21	17, 20	bitr4d 285	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
22		recn 11327	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
23	22	abscld 15647	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
24	23	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
25		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
26	22	absge0d 15655	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
27	26	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
28		simp2 1155	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅)
29	24, 25, 27, 28	le2sqd 14440	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
30		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
31	30, 25	absled 15641	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ( -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
32	21, 29, 31	3bitr2d 310	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ ( -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))
33	32	biimprd 251	. . . . . . . . . 10 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (( -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
34	33	3expa 1136	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ℝ) → (( -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
35	34	exp4b 436	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ℝ → ( -𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))))
36	35	3impd 1367	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
37	13, 36	sylbid 243	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))))
38	37	imp 412	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
39		elrege0 13623	. . . . 5 ⊢ (((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞) ↔ (((𝑅↑2) − (𝑡↑2)) ∈ ℝ ∧ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
40	10, 38, 39	sylanbrc 595	. . . 4 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞))
41		fvres 6933	. . . 4 ⊢ (((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞) → ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
42	40, 41	syl 18	. . 3 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅)) → ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2))) = (√‘((𝑅↑2) − (𝑡↑2))))
43	42	mpteq2dva 5202	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2)))) = (𝑡 ∈ ( -𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))))
44		eqid 2763	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
45	44	cnfldtopon 25145	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
46		ax-resscn 11294	. . . . . . 7 ⊢ ℝ ⊆ ℂ
47	6, 46	sstrdi 3925	. . . . . 6 ⊢ (𝑅 ∈ ℝ → ( -𝑅[,]𝑅) ⊆ ℂ)
48		resttopon 23523	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ( -𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) ∈ (TopOn‘( -𝑅[,]𝑅)))
49	45, 47, 48	sylancr 599	. . . . 5 ⊢ (𝑅 ∈ ℝ → ((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) ∈ (TopOn‘( -𝑅[,]𝑅)))
50	49	adantr 486	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) ∈ (TopOn‘( -𝑅[,]𝑅)))
51	47	resmptd 6048	. . . . . . 7 ⊢ (𝑅 ∈ ℝ → ((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ↾ ( -𝑅[,]𝑅)) = (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))))
52	45	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
53		recn 11327	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ → 𝑅 ∈ ℂ)
54	53	sqcld 14325	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℂ)
55	52, 52, 54	cnmptc 24025	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ℂ ↦ (𝑅↑2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
56	44	sqcn 25239	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℂ ↦ (𝑡↑2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld))
57	56	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ℂ ↦ (𝑡↑2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
58	44	subcn 25230	. . . . . . . . . 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 24029	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
61	45	toponunii 23278	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
62	61	cnrest 23647	. . . . . . . 8 ⊢ (((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)) ∧ ( -𝑅[,]𝑅) ⊆ ℂ) → ((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ↾ ( -𝑅[,]𝑅)) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
63	60, 47, 62	syl2anc 596	. . . . . . 7 ⊢ (𝑅 ∈ ℝ → ((𝑡 ∈ ℂ ↦ ((𝑅↑2) − (𝑡↑2))) ↾ ( -𝑅[,]𝑅)) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
64	51, 63	eqeltrrd 2865	. . . . . 6 ⊢ (𝑅 ∈ ℝ → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
65	64	adantr 486	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)))
66	45	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
67		eqid 2763	. . . . . . . 8 ⊢ (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) = (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2)))
68	67	rnmpt 5949	. . . . . . 7 ⊢ ran (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) = {𝑢 ∣ ∃𝑡 ∈ ( -𝑅[,]𝑅)𝑢 = ((𝑅↑2) − (𝑡↑2))}
69		simp3 1156	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅) ∧ 𝑢 = ((𝑅↑2) − (𝑡↑2))) → 𝑢 = ((𝑅↑2) − (𝑡↑2)))
70	40	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅) ∧ 𝑢 = ((𝑅↑2) − (𝑡↑2))) → ((𝑅↑2) − (𝑡↑2)) ∈ (0[,)+∞))
71	69, 70	eqeltrd 2864	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑡 ∈ ( -𝑅[,]𝑅) ∧ 𝑢 = ((𝑅↑2) − (𝑡↑2))) → 𝑢 ∈ (0[,)+∞))
72	71	rexlimdv3a 3171	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (∃𝑡 ∈ ( -𝑅[,]𝑅)𝑢 = ((𝑅↑2) − (𝑡↑2)) → 𝑢 ∈ (0[,)+∞)))
73	72	abssdv 3995	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → {𝑢 ∣ ∃𝑡 ∈ ( -𝑅[,]𝑅)𝑢 = ((𝑅↑2) − (𝑡↑2))} ⊆ (0[,)+∞))
74	68, 73	eqsstrid 3951	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ran (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ⊆ (0[,)+∞))
75		rge0ssre 13625	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
76	75, 46	sstri 3922	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℂ
77	76	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (0[,)+∞) ⊆ ℂ)
78		cnrest2 23648	. . . . . 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 1399	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → ((𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn (TopOpen‘ℂ_fld)) ↔ (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)))))
80	65, 79	mpbid 235	. . . 4 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((𝑅↑2) − (𝑡↑2))) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞))))
81		ssid 3935	. . . . . . . 8 ⊢ ℂ ⊆ ℂ
82		cncfss 25264	. . . . . . . 8 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((0[,)+∞)–cn→ℝ) ⊆ ((0[,)+∞)–cn→ℂ))
83	46, 81, 82	mp2an 705	. . . . . . 7 ⊢ ((0[,)+∞)–cn→ℝ) ⊆ ((0[,)+∞)–cn→ℂ)
84		resqrtcn 27123	. . . . . . 7 ⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ)
85	83, 84	sselii 3910	. . . . . 6 ⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℂ)
86		eqid 2763	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) = ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞))
87		eqid 2763	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
88	44, 86, 87	cncfcn 25275	. . . . . . 7 ⊢ (((0[,)+∞) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((0[,)+∞)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
89	76, 81, 88	mp2an 705	. . . . . 6 ⊢ ((0[,)+∞)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ))
90	85, 89	eleqtri 2862	. . . . 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 24027	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2)))) ∈ (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
93		eqid 2763	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) = ((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅))
94	44, 93, 87	cncfcn 25275	. . . . 5 ⊢ ((( -𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (( -𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
95	47, 81, 94	sylancl 598	. . . 4 ⊢ (𝑅 ∈ ℝ → (( -𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
96	95	adantr 486	. . 3 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (( -𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ( -𝑅[,]𝑅)) Cn ((TopOpen‘ℂ_fld) ↾_t ℂ)))
97	92, 96	eleqtrrd 2867	. 2 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ ((√ ↾ (0[,)+∞))‘((𝑅↑2) − (𝑡↑2)))) ∈ (( -𝑅[,]𝑅)–cn→ℂ))
98	43, 97	eqeltrrd 2865	1 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ ( -𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ (( -𝑅[,]𝑅)–cn→ℂ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 {cab 2741 ∃wrex 3090 ⊆ wss 3900 class class class wbr 5106 ↦ cmpt 5190 ran crn 5657 ↾ cres 5658 ‘cfv 6564 (class class class)co 7449 ℂcc 11235 ℝcr 11236 0cc0 11237 +∞cpnf 11377 ≤ cle 11381 − cmin 11578 -cneg 11579 2c2 12435 [,)cico 13516 [,]cicc 13517 ↑cexp 14242 √csqrt 15441 abscabs 15442 ↾_t crest 17632 TopOpenctopn 17633 ℂ_fldccnfld 21720 TopOnctopon 23272 Cn ccn 23586 ×_t ctx 23923 –cn→ccncf 25241

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315 ax-addf 11316

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-of 7723 df-om 7910 df-1st 8033 df-2nd 8034 df-supp 8213 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-er 8753 df-map 8885 df-pm 8886 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-fsupp 9390 df-fi 9438 df-sup 9469 df-inf 9470 df-oi 9539 df-card 10055 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-z 12732 df-dec 12853 df-uz 13004 df-q 13114 df-rp 13159 df-xneg 13279 df-xadd 13280 df-xmul 13281 df-ioo 13518 df-ioc 13519 df-ico 13520 df-icc 13521 df-fz 13678 df-fzo 13827 df-fl 13970 df-mod 14048 df-seq 14183 df-exp 14243 df-fac 14457 df-bc 14486 df-hash 14514 df-shft 15261 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-limsup 15679 df-clim 15696 df-rlim 15697 df-sum 15895 df-ef 16274 df-sin 16276 df-cos 16277 df-tan 16278 df-pi 16279 df-struct 17366 df-sets 17383 df-slot 17401 df-ndx 17413 df-base 17429 df-ress 17450 df-plusg 17482 df-mulr 17483 df-starv 17484 df-sca 17485 df-vsca 17486 df-ip 17487 df-tset 17488 df-ple 17489 df-ds 17491 df-unif 17492 df-hom 17493 df-cco 17494 df-rest 17634 df-topn 17635 df-0g 17653 df-gsum 17654 df-topgen 17655 df-pt 17656 df-prds 17659 df-xrs 17715 df-qtop 17720 df-imas 17721 df-xps 17723 df-mre 17797 df-mrc 17798 df-acs 17800 df-mgm 18857 df-sgrp 18949 df-mnd 18965 df-submnd 19020 df-mulg 19319 df-cntz 19573 df-cmn 20038 df-psmet 21712 df-xmet 21713 df-met 21714 df-bl 21715 df-mopn 21716 df-fbas 21717 df-fg 21718 df-cnfld 21721 df-top 23256 df-topon 23273 df-topsp 23295 df-bases 23308 df-cld 23381 df-ntr 23382 df-cls 23383 df-nei 23460 df-lp 23498 df-perf 23499 df-cn 23589 df-cnp 23590 df-haus 23677 df-cmp 23749 df-tx 23925 df-hmeo 24118 df-fil 24209 df-fm 24301 df-flim 24302 df-flf 24303 df-xms 24683 df-ms 24684 df-tms 24685 df-cncf 25243 df-limc 26230 df-dv 26231 df-log 26930 df-cxp 26931

This theorem is used by: areacirclem3 38889 areacirclem4 38890 areacirc 38892

W3C validator