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 0 R t R R R 2 t 2 : R R cn

Proof

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