Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  supcvg Unicode version

Theorem supcvg 12623
 Description: Extract a sequence in such that the image of the points in the bounded set converges to the supremum of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 8304. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
Hypotheses
Ref Expression
supcvg.1
supcvg.2
supcvg.3
supcvg.4
supcvg.5
supcvg.6
supcvg.7
Assertion
Ref Expression
supcvg
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,,)   (,)   (,)

Proof of Theorem supcvg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6080 . . . . . . . . . . . 12
21oveq2d 6088 . . . . . . . . . . 11
3 supcvg.3 . . . . . . . . . . 11
4 ovex 6097 . . . . . . . . . . 11
52, 3, 4fvmpt 5797 . . . . . . . . . 10
65adantl 453 . . . . . . . . 9
7 supcvg.2 . . . . . . . . . . 11
8 supcvg.6 . . . . . . . . . . . . 13
9 supcvg.4 . . . . . . . . . . . . . 14
10 supcvg.5 . . . . . . . . . . . . . . . . . 18
11 fof 5644 . . . . . . . . . . . . . . . . . 18
1210, 11syl 16 . . . . . . . . . . . . . . . . 17
13 feq3 5569 . . . . . . . . . . . . . . . . 17
1412, 13syl5ibcom 212 . . . . . . . . . . . . . . . 16
15 f00 5619 . . . . . . . . . . . . . . . . 17
1615simprbi 451 . . . . . . . . . . . . . . . 16
1714, 16syl6 31 . . . . . . . . . . . . . . 15
1817necon3d 2636 . . . . . . . . . . . . . 14
199, 18mpd 15 . . . . . . . . . . . . 13
20 supcvg.7 . . . . . . . . . . . . 13
218, 19, 203jca 1134 . . . . . . . . . . . 12
22 suprcl 9957 . . . . . . . . . . . 12
2321, 22syl 16 . . . . . . . . . . 11
247, 23syl5eqel 2519 . . . . . . . . . 10
25 nnrp 10610 . . . . . . . . . . 11
2625rpreccld 10647 . . . . . . . . . 10
27 ltsubrp 10632 . . . . . . . . . 10
2824, 26, 27syl2an 464 . . . . . . . . 9
296, 28eqbrtrd 4224 . . . . . . . 8
3029, 7syl6breq 4243 . . . . . . 7
3121adantr 452 . . . . . . . 8
32 nnrecre 10025 . . . . . . . . . . 11
33 resubcl 9354 . . . . . . . . . . 11
3424, 32, 33syl2an 464 . . . . . . . . . 10
3534, 3fmptd 5884 . . . . . . . . 9
3635ffvelrnda 5861 . . . . . . . 8
37 suprlub 9959 . . . . . . . 8
3831, 36, 37syl2anc 643 . . . . . . 7
3930, 38mpbid 202 . . . . . 6
4036adantr 452 . . . . . . . 8
418adantr 452 . . . . . . . . 9
4241sselda 3340 . . . . . . . 8
43 ltle 9152 . . . . . . . 8
4440, 42, 43syl2anc 643 . . . . . . 7
4544reximdva 2810 . . . . . 6
4639, 45mpd 15 . . . . 5
47 forn 5647 . . . . . . . . 9
4810, 47syl 16 . . . . . . . 8
4948rexeqdv 2903 . . . . . . 7
50 ffn 5582 . . . . . . . 8
51 breq2 4208 . . . . . . . . 9
5251rexrn 5863 . . . . . . . 8
5312, 50, 523syl 19 . . . . . . 7
5449, 53bitr3d 247 . . . . . 6
5554adantr 452 . . . . 5
5646, 55mpbid 202 . . . 4
5756ralrimiva 2781 . . 3
58 supcvg.1 . . . 4
59 nnenom 11307 . . . 4
60 fveq2 5719 . . . . 5
6160breq2d 4216 . . . 4
6258, 59, 61axcc4 8308 . . 3
6357, 62syl 16 . 2
64 nnuz 10510 . . . . . 6
65 1z 10300 . . . . . . 7
6665a1i 11 . . . . . 6
6765a1i 11 . . . . . . . . 9
6824recnd 9103 . . . . . . . . . 10
6964eqimss2i 3395 . . . . . . . . . . 11
70 nnex 9995 . . . . . . . . . . 11
7169, 70climconst2 12330 . . . . . . . . . 10
7268, 65, 71sylancl 644 . . . . . . . . 9
7370mptex 5957 . . . . . . . . . . 11
743, 73eqeltri 2505 . . . . . . . . . 10
7574a1i 11 . . . . . . . . 9
76 ax-1cn 9037 . . . . . . . . . 10
77 divcnv 12621 . . . . . . . . . 10
7876, 77mp1i 12 . . . . . . . . 9
79 fvconst2g 5936 . . . . . . . . . . 11
8024, 79sylan 458 . . . . . . . . . 10
8168adantr 452 . . . . . . . . . 10
8280, 81eqeltrd 2509 . . . . . . . . 9
83 eqid 2435 . . . . . . . . . . . 12
84 ovex 6097 . . . . . . . . . . . 12
851, 83, 84fvmpt 5797 . . . . . . . . . . 11
8685adantl 453 . . . . . . . . . 10
87 nnrecre 10025 . . . . . . . . . . . 12
8887recnd 9103 . . . . . . . . . . 11
8988adantl 453 . . . . . . . . . 10
9086, 89eqeltrd 2509 . . . . . . . . 9
9180, 86oveq12d 6090 . . . . . . . . . 10
926, 91eqtr4d 2470 . . . . . . . . 9
9364, 67, 72, 75, 78, 82, 90, 92climsub 12415 . . . . . . . 8
9468subid1d 9389 . . . . . . . 8
9593, 94breqtrd 4228 . . . . . . 7
9695ad2antrr 707 . . . . . 6
9712ad2antrr 707 . . . . . . . 8
98 fex 5960 . . . . . . . 8
9997, 58, 98sylancl 644 . . . . . . 7
100 vex 2951 . . . . . . 7
101 coexg 5403 . . . . . . 7
10299, 100, 101sylancl 644 . . . . . 6
10335ad2antrr 707 . . . . . . 7
104103ffvelrnda 5861 . . . . . 6
105 fss 5590 . . . . . . . . . 10
10612, 8, 105syl2anc 643 . . . . . . . . 9
107 fco 5591 . . . . . . . . 9
108106, 107sylan 458 . . . . . . . 8
109108adantr 452 . . . . . . 7
110109ffvelrnda 5861 . . . . . 6
111 fveq2 5719 . . . . . . . . . 10
112 fveq2 5719 . . . . . . . . . . 11
113112fveq2d 5723 . . . . . . . . . 10
114111, 113breq12d 4217 . . . . . . . . 9
115114rspccva 3043 . . . . . . . 8
116115adantll 695 . . . . . . 7
117 simplr 732 . . . . . . . 8
118 fvco3 5791 . . . . . . . 8
119117, 118sylan 458 . . . . . . 7
120116, 119breqtrrd 4230 . . . . . 6
12121ad3antrrr 711 . . . . . . . . 9
122117ffvelrnda 5861 . . . . . . . . . 10
12397ffvelrnda 5861 . . . . . . . . . 10
124122, 123syldan 457 . . . . . . . . 9
125 suprub 9958 . . . . . . . . 9
126121, 124, 125syl2anc 643 . . . . . . . 8
127126, 7syl6breqr 4244 . . . . . . 7
128119, 127eqbrtrd 4224 . . . . . 6
12964, 66, 96, 102, 104, 110, 120, 128climsqz 12422 . . . . 5
130129ex 424 . . . 4
131130imdistanda 675 . . 3
132131eximdv 1632 . 2
13363, 132mpd 15 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698  cvv 2948   wss 3312  c0 3620  csn 3806   class class class wbr 4204   cmpt 4258   cxp 4867   crn 4870   ccom 4873   wfn 5440  wf 5441  wfo 5443  cfv 5445  (class class class)co 6072  csup 7436  cc 8977  cr 8978  cc0 8979  c1 8980   clt 9109   cle 9110   cmin 9280   cdiv 9666  cn 9989  cz 10271  cuz 10477  crp 10601   cli 12266 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-inf2 7585  ax-cc 8304  ax-cnex 9035  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-mulcom 9043  ax-addass 9044  ax-mulass 9045  ax-distr 9046  ax-i2m1 9047  ax-1ne0 9048  ax-1rid 9049  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054  ax-pre-ltadd 9055  ax-pre-mulgt0 9056  ax-pre-sup 9057 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-2nd 6341  df-riota 6540  df-recs 6624  df-rdg 6659  df-er 6896  df-pm 7012  df-en 7101  df-dom 7102  df-sdom 7103  df-sup 7437  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115  df-sub 9282  df-neg 9283  df-div 9667  df-nn 9990  df-2 10047  df-3 10048  df-n0 10211  df-z 10272  df-uz 10478  df-rp 10602  df-fl 11190  df-seq 11312  df-exp 11371  df-cj 11892  df-re 11893  df-im 11894  df-sqr 12028  df-abs 12029  df-clim 12270  df-rlim 12271
 Copyright terms: Public domain W3C validator