Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1cnnc Structured version   Unicode version

Theorem ftc1cnnc 26269
 Description: Choice-free proof of ftc1cn 19919. (Contributed by Brendan Leahy, 20-Nov-2017.)
Hypotheses
Ref Expression
ftc1cnnc.g
ftc1cnnc.a
ftc1cnnc.b
ftc1cnnc.le
ftc1cnnc.f
ftc1cnnc.i
Assertion
Ref Expression
ftc1cnnc
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem ftc1cnnc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvf 19786 . . . . 5
21a1i 11 . . . 4
3 ffun 5585 . . . 4
42, 3syl 16 . . 3
5 ax-resscn 9039 . . . . . . 7
65a1i 11 . . . . . 6
7 ftc1cnnc.g . . . . . . 7
8 ftc1cnnc.a . . . . . . 7
9 ftc1cnnc.b . . . . . . 7
10 ftc1cnnc.le . . . . . . 7
11 ssid 3359 . . . . . . . 8
1211a1i 11 . . . . . . 7
13 ioossre 10964 . . . . . . . 8
1413a1i 11 . . . . . . 7
15 ftc1cnnc.i . . . . . . 7
16 ftc1cnnc.f . . . . . . . 8
17 cncff 18915 . . . . . . . 8
1816, 17syl 16 . . . . . . 7
197, 8, 9, 10, 12, 14, 15, 18ftc1lem2 19912 . . . . . 6
20 iccssre 10984 . . . . . . 7
218, 9, 20syl2anc 643 . . . . . 6
22 eqid 2435 . . . . . . 7 fld fld
2322tgioo2 18826 . . . . . 6 fldt
246, 19, 21, 23, 22dvbssntr 19779 . . . . 5
25 iccntr 18844 . . . . . 6
268, 9, 25syl2anc 643 . . . . 5
2724, 26sseqtrd 3376 . . . 4
28 retop 18787 . . . . . . . . . . . 12
2923, 28eqeltrri 2506 . . . . . . . . . . 11 fldt
3029a1i 11 . . . . . . . . . 10 fldt
3121adantr 452 . . . . . . . . . 10
32 iooretop 18792 . . . . . . . . . . . 12
3332, 23eleqtri 2507 . . . . . . . . . . 11 fldt
3433a1i 11 . . . . . . . . . 10 fldt
35 ioossicc 10988 . . . . . . . . . . 11
3635a1i 11 . . . . . . . . . 10
37 uniretop 18788 . . . . . . . . . . . 12
3823unieqi 4017 . . . . . . . . . . . 12 fldt
3937, 38eqtri 2455 . . . . . . . . . . 11 fldt
4039ssntr 17114 . . . . . . . . . 10 fldt fldt fldt
4130, 31, 34, 36, 40syl22anc 1185 . . . . . . . . 9 fldt
42 simpr 448 . . . . . . . . 9
4341, 42sseldd 3341 . . . . . . . 8 fldt
4418ffvelrnda 5862 . . . . . . . . 9
45 cnxmet 18799 . . . . . . . . . . . . . 14
4613, 5sstri 3349 . . . . . . . . . . . . . 14
47 xmetres2 18383 . . . . . . . . . . . . . 14
4845, 46, 47mp2an 654 . . . . . . . . . . . . 13
4948a1i 11 . . . . . . . . . . . 12
5045a1i 11 . . . . . . . . . . . 12
51 ssid 3359 . . . . . . . . . . . . . . . . 17
52 eqid 2435 . . . . . . . . . . . . . . . . . 18 fldt fldt
5322cnfldtop 18810 . . . . . . . . . . . . . . . . . . . 20 fld
5422cnfldtopon 18809 . . . . . . . . . . . . . . . . . . . . . 22 fld TopOn
5554toponunii 16989 . . . . . . . . . . . . . . . . . . . . 21 fld
5655restid 13653 . . . . . . . . . . . . . . . . . . . 20 fld fldt fld
5753, 56ax-mp 8 . . . . . . . . . . . . . . . . . . 19 fldt fld
5857eqcomi 2439 . . . . . . . . . . . . . . . . . 18 fld fldt
5922, 52, 58cncfcn 18931 . . . . . . . . . . . . . . . . 17 fldt fld
6046, 51, 59mp2an 654 . . . . . . . . . . . . . . . 16 fldt fld
6116, 60syl6eleq 2525 . . . . . . . . . . . . . . 15 fldt fld
62 resttopon 17217 . . . . . . . . . . . . . . . . . . 19 fld TopOn fldt TopOn
6354, 46, 62mp2an 654 . . . . . . . . . . . . . . . . . 18 fldt TopOn
6463toponunii 16989 . . . . . . . . . . . . . . . . 17 fldt
6564eleq2i 2499 . . . . . . . . . . . . . . . 16 fldt
6665biimpi 187 . . . . . . . . . . . . . . 15 fldt
67 eqid 2435 . . . . . . . . . . . . . . . 16 fldt fldt
6867cncnpi 17334 . . . . . . . . . . . . . . 15 fldt fld fldt fldt fld
6961, 66, 68syl2an 464 . . . . . . . . . . . . . 14 fldt fld
70 eqid 2435 . . . . . . . . . . . . . . . . . 18
7122cnfldtopn 18808 . . . . . . . . . . . . . . . . . 18 fld
72 eqid 2435 . . . . . . . . . . . . . . . . . 18
7370, 71, 72metrest 18546 . . . . . . . . . . . . . . . . 17 fldt
7445, 46, 73mp2an 654 . . . . . . . . . . . . . . . 16 fldt
7574oveq1i 6083 . . . . . . . . . . . . . . 15 fldt fld fld
7675fveq1i 5721 . . . . . . . . . . . . . 14 fldt fld fld
7769, 76syl6eleq 2525 . . . . . . . . . . . . 13 fld
7877adantr 452 . . . . . . . . . . . 12 fld
79 simpr 448 . . . . . . . . . . . 12
8072, 71metcnpi2 18567 . . . . . . . . . . . 12 fld
8149, 50, 78, 79, 80syl22anc 1185 . . . . . . . . . . 11
82 simpr 448 . . . . . . . . . . . . . . . . . . 19
83 simpllr 736 . . . . . . . . . . . . . . . . . . 19
8482, 83ovresd 6206 . . . . . . . . . . . . . . . . . 18
85 elioore 10938 . . . . . . . . . . . . . . . . . . . . 21
8685recnd 9106 . . . . . . . . . . . . . . . . . . . 20
8786adantl 453 . . . . . . . . . . . . . . . . . . 19
8846sseli 3336 . . . . . . . . . . . . . . . . . . . 20
8988ad3antlr 712 . . . . . . . . . . . . . . . . . . 19
90 eqid 2435 . . . . . . . . . . . . . . . . . . . 20
9190cnmetdval 18797 . . . . . . . . . . . . . . . . . . 19
9287, 89, 91syl2anc 643 . . . . . . . . . . . . . . . . . 18
9384, 92eqtrd 2467 . . . . . . . . . . . . . . . . 17
9493breq1d 4214 . . . . . . . . . . . . . . . 16
9518ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
9695ffvelrnda 5862 . . . . . . . . . . . . . . . . . 18
9744ad2antrr 707 . . . . . . . . . . . . . . . . . 18
9890cnmetdval 18797 . . . . . . . . . . . . . . . . . 18
9996, 97, 98syl2anc 643 . . . . . . . . . . . . . . . . 17
10099breq1d 4214 . . . . . . . . . . . . . . . 16
10194, 100imbi12d 312 . . . . . . . . . . . . . . 15
102101ralbidva 2713 . . . . . . . . . . . . . 14
103 simprll 739 . . . . . . . . . . . . . . . . . . . 20
104 eldifsni 3920 . . . . . . . . . . . . . . . . . . . 20
105103, 104syl 16 . . . . . . . . . . . . . . . . . . 19
10621ssdifssd 3477 . . . . . . . . . . . . . . . . . . . . . . . . 25
107106sselda 3340 . . . . . . . . . . . . . . . . . . . . . . . 24
108107ad2ant2r 728 . . . . . . . . . . . . . . . . . . . . . . 23
109108ad2ant2r 728 . . . . . . . . . . . . . . . . . . . . . 22
110 elioore 10938 . . . . . . . . . . . . . . . . . . . . . . 23
111110ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . 22
112109, 111lttri2d 9204 . . . . . . . . . . . . . . . . . . . . 21
113112biimpa 471 . . . . . . . . . . . . . . . . . . . 20
114 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115114oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117115, 116oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
118 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
119 ovex 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
120117, 118, 119fvmpt 5798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
121120ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26
122121ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25
12319ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
124 eldifi 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125124ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
126125ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
127123, 126ffvelrnd 5863 . . . . . . . . . . . . . . . . . . . . . . . . . 26
12835sseli 3336 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
12919ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
130128, 129sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
131130ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26
132109adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133132recnd 9106 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13488ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26
135 ltne 9162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136135necomd 2681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
137109, 136sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26
138127, 131, 133, 134, 137div2subd 9832 . . . . . . . . . . . . . . . . . . . . . . . . 25
139122, 138eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . 24
140139oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . 23
141140fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . 22
1428ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
1439ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
14410ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
14516ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
14615ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
147 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . 23
148 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . 23
149 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . 23
150 simprlr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
151 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
152151fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
153152breq1d 4214 . . . . . . . . . . . . . . . . . . . . . . . . . 26
154 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
155154oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
156155fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
157156breq1d 4214 . . . . . . . . . . . . . . . . . . . . . . . . . 26
158153, 157imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . 25
159158rspccva 3043 . . . . . . . . . . . . . . . . . . . . . . . 24
160150, 159sylan 458 . . . . . . . . . . . . . . . . . . . . . . 23
161103, 124syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
162 simprr 734 . . . . . . . . . . . . . . . . . . . . . . 23
163128ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . 23
164110recnd 9106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
165164subidd 9391 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166165abs00bd 12088 . . . . . . . . . . . . . . . . . . . . . . . . 25
167166ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . 24
168149rpgt0d 10643 . . . . . . . . . . . . . . . . . . . . . . . 24
169167, 168eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . . . 23
1707, 142, 143, 144, 145, 146, 147, 118, 148, 149, 160, 161, 162, 163, 169ftc1cnnclem 26268 . . . . . . . . . . . . . . . . . . . . . 22
171141, 170eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . 21
172120oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . 25
173172fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . 24
174173ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23
175174ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . 22
1767, 142, 143, 144, 145, 146, 147, 118, 148, 149, 160, 163, 169, 161, 162ftc1cnnclem 26268 . . . . . . . . . . . . . . . . . . . . . 22
177175, 176eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . 21
178171, 177jaodan 761 . . . . . . . . . . . . . . . . . . . 20
179113, 178syldan 457 . . . . . . . . . . . . . . . . . . 19
180105, 179mpdan 650 . . . . . . . . . . . . . . . . . 18
181180expr 599 . . . . . . . . . . . . . . . . 17
182181adantld 454 . . . . . . . . . . . . . . . 16
183182expr 599 . . . . . . . . . . . . . . 15
184183ralrimdva 2788 . . . . . . . . . . . . . 14
185102, 184sylbid 207 . . . . . . . . . . . . 13
186185anassrs 630 . . . . . . . . . . . 12
187186reximdva 2810 . . . . . . . . . . 11
18881, 187mpd 15 . . . . . . . . . 10
189188ralrimiva 2781 . . . . . . . . 9
19019adantr 452 . . . . . . . . . . . 12
19121, 5syl6ss 3352 . . . . . . . . . . . . 13
192191adantr 452 . . . . . . . . . . . 12
193128adantl 453 . . . . . . . . . . . 12
194190, 192, 193dvlem 19775 . . . . . . . . . . 11
195194, 118fmptd 5885 . . . . . . . . . 10
196191ssdifssd 3477 . . . . . . . . . . 11
197196adantr 452 . . . . . . . . . 10
19888adantl 453 . . . . . . . . . 10
199195, 197, 198ellimc3 19758 . . . . . . . . 9 lim
20044, 189, 199mpbir2and 889 . . . . . . . 8 lim
201 eqid 2435 . . . . . . . . . 10 fldt fldt
202201, 22, 118, 6, 19, 21eldv 19777 . . . . . . . . 9 fldt lim
203202adantr 452 . . . . . . . 8 fldt lim
20443, 200, 203mpbir2and 889 . . . . . . 7
205 vex 2951 . . . . . . . 8
206 fvex 5734 . . . . . . . 8
207205, 206breldm 5066 . . . . . . 7
208204, 207syl 16 . . . . . 6
209208ex 424 . . . . 5
210209ssrdv 3346 . . . 4
21127, 210eqssd 3357 . . 3
212 df-fn 5449 . . 3
2134, 211, 212sylanbrc 646 . 2
214 ffn 5583 . . 3
21518, 214syl 16 . 2