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 
|- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )

Proof

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