Metamath Proof Explorer

Theorem areacirclem2

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

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

Proof

Step Hyp Ref Expression
1 resqcl ⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ↑ 2 ) ∈ ℝ )
2 1 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
3 2 adantr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
4 renegcl ⊢ ( 𝑅 ∈ ℝ → - 𝑅 ∈ ℝ )
5 iccssre ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
6 4 5 mpancom ⊢ ( 𝑅 ∈ ℝ → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
7 6 sselda ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 𝑡 ∈ ℝ )
8 7 resqcld ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
9 8 adantlr ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
10 3 9 resubcld ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
11 elicc2 ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
12 4 11 mpancom ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
13 12 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
14 1 3ad2ant1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
15 resqcl ⊢ ( 𝑡 ∈ ℝ → ( 𝑡 ↑ 2 ) ∈ ℝ )
16 15 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
17 14 16 subge0d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ↔ ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
18 absresq ⊢ ( 𝑡 ∈ ℝ → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
19 18 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
20 19 breq1d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ↔ ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
21 17 20 bitr4d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
22 recn ⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
23 22 abscld ⊢ ( 𝑡 ∈ ℝ → ( abs ‘ 𝑡 ) ∈ ℝ )
24 23 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ 𝑡 ) ∈ ℝ )
25 simp1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 𝑅 ∈ ℝ )
26 22 absge0d ⊢ ( 𝑡 ∈ ℝ → 0 ≤ ( abs ‘ 𝑡 ) )
27 26 3ad2ant3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ 𝑡 ) )
28 simp2 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 0 ≤ 𝑅 )
29 24 25 27 28 le2sqd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
30 simp3 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
31 30 25 absled ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
32 21 29 31 3bitr2d ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ↔ ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
33 32 biimprd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
34 33 3expa ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ℝ ) → ( ( - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
35 34 exp4b ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ℝ → ( - 𝑅 ≤ 𝑡 → ( 𝑡 ≤ 𝑅 → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
36 35 3impd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( 𝑡 ∈ ℝ ∧ - 𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
37 13 36 sylbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
38 37 imp ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
39 elrege0 ⊢ ( ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
40 10 38 39 sylanbrc ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ( 0 [,) +∞ ) )
41 fvres ⊢ ( ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ( 0 [,) +∞ ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
42 40 41 syl ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
43 42 mpteq2dva ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( √ ↾ ( 0 [,) +∞ ) ) ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
44 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
45 44 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
46 ax-resscn ⊢ ℝ ⊆ ℂ
47 6 46 sstrdi ⊢ ( 𝑅 ∈ ℝ → ( - 𝑅 [,] 𝑅 ) ⊆ ℂ )
48 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( - 𝑅 [,] 𝑅 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ ( TopOn ‘ ( - 𝑅 [,] 𝑅 ) ) )
49 45 47 48 sylancr ⊢ ( 𝑅 ∈ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ ( TopOn ‘ ( - 𝑅 [,] 𝑅 ) ) )
50 49 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ ( TopOn ‘ ( - 𝑅 [,] 𝑅 ) ) )
51 47 resmptd ⊢ ( 𝑅 ∈ ℝ → ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↾ ( - 𝑅 [,] 𝑅 ) ) = ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
52 45 a1i ⊢ ( 𝑅 ∈ ℝ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
53 recn ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℂ )
54 53 sqcld ⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ↑ 2 ) ∈ ℂ )
55 52 52 54 cnmptc ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ℂ ↦ ( 𝑅 ↑ 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
56 44 sqcn ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
57 56 a1i ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
58 44 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
59 58 a1i ⊢ ( 𝑅 ∈ ℝ → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
60 52 55 57 59 cnmpt12f ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ℂ ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
61 45 toponunii ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
62 61 cnrest ⊢ ( ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( - 𝑅 [,] 𝑅 ) ⊆ ℂ ) → ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↾ ( - 𝑅 [,] 𝑅 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
63 60 47 62 syl2anc ⊢ ( 𝑅 ∈ ℝ → ( ( 𝑡 ∈ ℂ ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↾ ( - 𝑅 [,] 𝑅 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
64 51 63 eqeltrrd ⊢ ( 𝑅 ∈ ℝ → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
65 64 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
66 45 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
67 eqid ⊢ ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
68 67 rnmpt ⊢ ran ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) = { 𝑢 ∣ ∃ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) }
69 simp3 ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ∧ 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) → 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
70 40 3adant3 ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ∧ 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ( 0 [,) +∞ ) )
71 69 70 eqeltrd ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ∧ 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) → 𝑢 ∈ ( 0 [,) +∞ ) )
72 71 rexlimdv3a ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ∃ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) → 𝑢 ∈ ( 0 [,) +∞ ) ) )
73 72 abssdv ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → { 𝑢 ∣ ∃ 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) 𝑢 = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) } ⊆ ( 0 [,) +∞ ) )
74 68 73 eqsstrid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ran ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ⊆ ( 0 [,) +∞ ) )
75 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
76 75 46 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
77 76 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 0 [,) +∞ ) ⊆ ℂ )
78 cnrest2 ⊢ ( ( ( 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 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) ) ) )
80 65 79 mpbid ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) ) )
81 ssid ⊢ ℂ ⊆ ℂ
82 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 0 [,) +∞ ) –cn→ ℝ ) ⊆ ( ( 0 [,) +∞ ) –cn→ ℂ ) )
83 46 81 82 mp2an ⊢ ( ( 0 [,) +∞ ) –cn→ ℝ ) ⊆ ( ( 0 [,) +∞ ) –cn→ ℂ )
84 resqrtcn ⊢ ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ )
85 83 84 sselii ⊢ ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℂ )
86 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) )
87 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
88 44 86 87 cncfcn ⊢ ( ( ( 0 [,) +∞ ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 0 [,) +∞ ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
89 76 81 88 mp2an ⊢ ( ( 0 [,) +∞ ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) )
90 85 89 eleqtri ⊢ ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) )
91 90 a1i ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
92 50 80 91 cnmpt11f ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( √ ↾ ( 0 [,) +∞ ) ) ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
93 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) )
94 44 93 87 cncfcn ⊢ ( ( ( - 𝑅 [,] 𝑅 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
95 47 81 94 sylancl ⊢ ( 𝑅 ∈ ℝ → ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
96 95 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 𝑅 [,] 𝑅 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
97 92 96 eleqtrrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( √ ↾ ( 0 [,) +∞ ) ) ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
98 43 97 eqeltrrd ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )