Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  climsuse Structured version   Unicode version

Theorem climsuse 37506
 Description: A subsequence of a converging sequence , converges to the same limit. is the strictly increasing and it is used to index the subsequence (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
climsuse.1
climsuse.3
climsuse.2
climsuse.4
climsuse.5
climsuse.6
climsuse.7
climsuse.8
climsuse.9
climsuse.10
climsuse.11
climsuse.12
climsuse.13
Assertion
Ref Expression
climsuse
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem climsuse
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climsuse.9 . . 3
2 climcl 13550 . . 3
31, 2syl 17 . 2
4 nfv 1751 . . 3
5 simpllr 767 . . . . . . 7
6 climsuse.6 . . . . . . . 8
76ad4antr 736 . . . . . . 7
85, 7ifclda 3941 . . . . . 6
9 nfv 1751 . . . . . . . 8
10 nfra1 2806 . . . . . . . 8
119, 10nfan 1984 . . . . . . 7
12 simp-4l 774 . . . . . . . . . 10
13 simpllr 767 . . . . . . . . . . . 12
1412, 13jca 534 . . . . . . . . . . 11
15 simpr 462 . . . . . . . . . . 11
16 simpr 462 . . . . . . . . . . . . . . . 16
176anim1i 570 . . . . . . . . . . . . . . . . . 18
1817adantr 466 . . . . . . . . . . . . . . . . 17
19 eluz 11172 . . . . . . . . . . . . . . . . 17
2018, 19syl 17 . . . . . . . . . . . . . . . 16
2116, 20mpbird 235 . . . . . . . . . . . . . . 15
22 simpll 758 . . . . . . . . . . . . . . . 16
23 uzid 11173 . . . . . . . . . . . . . . . 16
2422, 6, 233syl 18 . . . . . . . . . . . . . . 15
2521, 24ifclda 3941 . . . . . . . . . . . . . 14
26 uzss 11179 . . . . . . . . . . . . . 14
2725, 26syl 17 . . . . . . . . . . . . 13
28 climsuse.5 . . . . . . . . . . . . 13
2927, 28syl6sseqr 3511 . . . . . . . . . . . 12
3029sseld 3463 . . . . . . . . . . 11
3114, 15, 30sylc 62 . . . . . . . . . 10
32 climsuse.1 . . . . . . . . . . . . . 14
33 nfv 1751 . . . . . . . . . . . . . 14
3432, 33nfan 1984 . . . . . . . . . . . . 13
35 climsuse.2 . . . . . . . . . . . . . . 15
36 nfcv 2584 . . . . . . . . . . . . . . 15
3735, 36nffv 5884 . . . . . . . . . . . . . 14
38 climsuse.3 . . . . . . . . . . . . . . 15
39 climsuse.4 . . . . . . . . . . . . . . . 16
4039, 36nffv 5884 . . . . . . . . . . . . . . 15
4138, 40nffv 5884 . . . . . . . . . . . . . 14
4237, 41nfeq 2595 . . . . . . . . . . . . 13
4334, 42nfim 1976 . . . . . . . . . . . 12
44 eleq1 2494 . . . . . . . . . . . . . 14
4544anbi2d 708 . . . . . . . . . . . . 13
46 fveq2 5877 . . . . . . . . . . . . . 14
47 fveq2 5877 . . . . . . . . . . . . . . 15
4847fveq2d 5881 . . . . . . . . . . . . . 14
4946, 48eqeq12d 2444 . . . . . . . . . . . . 13
5045, 49imbi12d 321 . . . . . . . . . . . 12
51 climsuse.13 . . . . . . . . . . . 12
5243, 50, 51chvar 2067 . . . . . . . . . . 11
5328eleq2i 2500 . . . . . . . . . . . . . . . . 17
5453biimpi 197 . . . . . . . . . . . . . . . 16
5554adantl 467 . . . . . . . . . . . . . . 15
56 uzss 11179 . . . . . . . . . . . . . . 15
5755, 56syl 17 . . . . . . . . . . . . . 14
58 climsuse.10 . . . . . . . . . . . . . . 15
59 nfcv 2584 . . . . . . . . . . . . . . . . . . 19
6039, 59nffv 5884 . . . . . . . . . . . . . . . . . 18
61 nfcv 2584 . . . . . . . . . . . . . . . . . . 19
62 nfcv 2584 . . . . . . . . . . . . . . . . . . . 20
63 nfcv 2584 . . . . . . . . . . . . . . . . . . . 20
6440, 62, 63nfov 6327 . . . . . . . . . . . . . . . . . . 19
6561, 64nffv 5884 . . . . . . . . . . . . . . . . . 18
6660, 65nfel 2597 . . . . . . . . . . . . . . . . 17
6734, 66nfim 1976 . . . . . . . . . . . . . . . 16
68 oveq1 6308 . . . . . . . . . . . . . . . . . . 19
6968fveq2d 5881 . . . . . . . . . . . . . . . . . 18
7047oveq1d 6316 . . . . . . . . . . . . . . . . . . 19
7170fveq2d 5881 . . . . . . . . . . . . . . . . . 18
7269, 71eleq12d 2504 . . . . . . . . . . . . . . . . 17
7345, 72imbi12d 321 . . . . . . . . . . . . . . . 16
74 climsuse.11 . . . . . . . . . . . . . . . 16
7567, 73, 74chvar 2067 . . . . . . . . . . . . . . 15
7628, 6, 58, 75climsuselem1 37505 . . . . . . . . . . . . . 14
7757, 76sseldd 3465 . . . . . . . . . . . . 13
7877, 28syl6eleqr 2521 . . . . . . . . . . . 12
7978ex 435 . . . . . . . . . . . . 13
8079imdistani 694 . . . . . . . . . . . 12
8133nfci 2573 . . . . . . . . . . . . . . . 16
8240, 81nfel 2597 . . . . . . . . . . . . . . 15
8332, 82nfan 1984 . . . . . . . . . . . . . 14
8441nfel1 2600 . . . . . . . . . . . . . 14
8583, 84nfim 1976 . . . . . . . . . . . . 13
86 eleq1 2494 . . . . . . . . . . . . . . 15
8786anbi2d 708 . . . . . . . . . . . . . 14
88 fveq2 5877 . . . . . . . . . . . . . . 15
8988eleq1d 2491 . . . . . . . . . . . . . 14
9087, 89imbi12d 321 . . . . . . . . . . . . 13
91 climsuse.8 . . . . . . . . . . . . 13
9240, 85, 90, 91vtoclgf 3137 . . . . . . . . . . . 12
9378, 80, 92sylc 62 . . . . . . . . . . 11
9452, 93eqeltrd 2510 . . . . . . . . . 10
9512, 31, 94syl2anc 665 . . . . . . . . 9
9612, 31, 52syl2anc 665 . . . . . . . . . . . 12
9796oveq1d 6316 . . . . . . . . . . 11
9897fveq2d 5881 . . . . . . . . . 10
99 fveq2 5877 . . . . . . . . . . . . . . . 16
10099eleq1d 2491 . . . . . . . . . . . . . . 15
10199oveq1d 6316 . . . . . . . . . . . . . . . . 17
102101fveq2d 5881 . . . . . . . . . . . . . . . 16
103102breq1d 4430 . . . . . . . . . . . . . . 15
104100, 103anbi12d 715 . . . . . . . . . . . . . 14
105104cbvralv 3055 . . . . . . . . . . . . 13
106105biimpi 197 . . . . . . . . . . . 12
107106ad2antlr 731 . . . . . . . . . . 11
108 zre 10941 . . . . . . . . . . . . . . 15
1091083ad2ant2 1027 . . . . . . . . . . . . . 14
110 simp3 1007 . . . . . . . . . . . . . . 15
111 eluzelz 11168 . . . . . . . . . . . . . . 15
112 zre 10941 . . . . . . . . . . . . . . 15
113110, 111, 1123syl 18 . . . . . . . . . . . . . 14
114 simp1 1005 . . . . . . . . . . . . . . . 16
1156zred 11040 . . . . . . . . . . . . . . . . . . . 20
116114, 115syl 17 . . . . . . . . . . . . . . . . . . 19
117 simpl2 1009 . . . . . . . . . . . . . . . . . . . . 21
118117zred 11040 . . . . . . . . . . . . . . . . . . . 20
119116adantr 466 . . . . . . . . . . . . . . . . . . . 20
120118, 119ifclda 3941 . . . . . . . . . . . . . . . . . . 19
121 max1 11480 . . . . . . . . . . . . . . . . . . . 20
122116, 109, 121syl2anc 665 . . . . . . . . . . . . . . . . . . 19
123 eluzle 11171 . . . . . . . . . . . . . . . . . . . 20
1241233ad2ant3 1028 . . . . . . . . . . . . . . . . . . 19
125116, 120, 113, 122, 124letrd 9792 . . . . . . . . . . . . . . . . . 18
126114, 6syl 17 . . . . . . . . . . . . . . . . . . 19
1271113ad2ant3 1028 . . . . . . . . . . . . . . . . . . 19
128 eluz 11172 . . . . . . . . . . . . . . . . . . 19
129126, 127, 128syl2anc 665 . . . . . . . . . . . . . . . . . 18
130125, 129mpbird 235 . . . . . . . . . . . . . . . . 17
131130, 28syl6eleqr 2521 . . . . . . . . . . . . . . . 16
132114, 131jca 534 . . . . . . . . . . . . . . 15
133 eluzelre 11169 . . . . . . . . . . . . . . 15
134132, 77, 1333syl 18 . . . . . . . . . . . . . 14
135 max2 11482 . . . . . . . . . . . . . . . 16
136116, 109, 135syl2anc 665 . . . . . . . . . . . . . . 15
137109, 120, 113, 136, 124letrd 9792 . . . . . . . . . . . . . 14
138 eluzle 11171 . . . . . . . . . . . . . . 15
139132, 76, 1383syl 18 . . . . . . . . . . . . . 14
140109, 113, 134, 137, 139letrd 9792 . . . . . . . . . . . . 13
141 simp2 1006 . . . . . . . . . . . . . 14
142 eluzelz 11168 . . . . . . . . . . . . . . 15
143132, 76, 1423syl 18 . . . . . . . . . . . . . 14
144 eluz 11172 . . . . . . . . . . . . . 14
145141, 143, 144syl2anc 665 . . . . . . . . . . . . 13
146140, 145mpbird 235 . . . . . . . . . . . 12
14712, 13, 15, 146syl3anc 1264 . . . . . . . . . . 11
148 fveq2 5877 . . . . . . . . . . . . . . 15
149148eleq1d 2491 . . . . . . . . . . . . . 14
150148oveq1d 6316 . . . . . . . . . . . . . . . 16
151150fveq2d 5881 . . . . . . . . . . . . . . 15
152151breq1d 4430 . . . . . . . . . . . . . 14
153149, 152anbi12d 715 . . . . . . . . . . . . 13
154153rspccva 3181 . . . . . . . . . . . 12
155154simprd 464 . . . . . . . . . . 11
156107, 147, 155syl2anc 665 . . . . . . . . . 10
15798, 156eqbrtrd 4441 . . . . . . . . 9
15895, 157jca 534 . . . . . . . 8
159158ex 435 . . . . . . 7
16011, 159ralrimi 2825 . . . . . 6
161 fveq2 5877 . . . . . . . 8
162161raleqdv 3031 . . . . . . 7
163162rspcev 3182 . . . . . 6
1648, 160, 163syl2anc 665 . . . . 5
165 climsuse.7 . . . . . . . . 9
166 eqidd 2423 . . . . . . . . 9
167165, 166clim 13545 . . . . . . . 8
1681, 167mpbid 213 . . . . . . 7
169168simprd 464 . . . . . 6
170169r19.21bi 2794 . . . . 5
171164, 170r19.29a 2970 . . . 4
172171ex 435 . . 3
1734, 172ralrimi 2825 . 2
174 climsuse.12 . . 3
175 eqidd 2423 . . 3
176174, 175clim 13545 . 2
1773, 173, 176mpbir2and 930 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wnf 1663   wcel 1868  wnfc 2570  wral 2775  wrex 2776   wss 3436  cif 3909   class class class wbr 4420  cfv 5597  (class class class)co 6301  cc 9537  cr 9538  c1 9540   caddc 9542   clt 9675   cle 9676   cmin 9860  cz 10937  cuz 11159  crp 11302  cabs 13285   cli 13535 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-n0 10870  df-z 10938  df-uz 11160  df-clim 13539 This theorem is referenced by:  sumnnodd  37529  stirlinglem8  37762
 Copyright terms: Public domain W3C validator