Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  2clim Unicode version

Theorem 2clim 11100
 Description: If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
Hypotheses
Ref Expression
2clim.1
2clim.2
2clim.3
2clim.5
2clim.6
2clim.7
Assertion
Ref Expression
2clim
Distinct variable groups:   ,,   ,,,   ,,   ,   ,,   ,,,   ,
Allowed substitution hints:   ()   ()   (,)   (,,)

Proof of Theorem 2clim
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 2clim.6 . . . . . 6
2 rphalfcl 9496 . . . . . 6
3 breq2 3939 . . . . . . . 8
43rexralbidv 2464 . . . . . . 7
54rspccva 2791 . . . . . 6
61, 2, 5syl2an 287 . . . . 5
7 2clim.1 . . . . . 6
8 2clim.2 . . . . . . 7
98adantr 274 . . . . . 6
102adantl 275 . . . . . 6
11 eqidd 2141 . . . . . 6
12 2clim.7 . . . . . . 7
1312adantr 274 . . . . . 6
147, 9, 10, 11, 13climi 11086 . . . . 5
157rexanuz2 10793 . . . . 5
166, 14, 15sylanbrc 414 . . . 4
177uztrn2 9365 . . . . . . . 8
18 an12 551 . . . . . . . . 9
19 simprr 522 . . . . . . . . . . . . . . 15
20 2clim.5 . . . . . . . . . . . . . . . 16
2120ad2ant2r 501 . . . . . . . . . . . . . . 15
2219, 21abssubd 10995 . . . . . . . . . . . . . 14
2322breq1d 3945 . . . . . . . . . . . . 13
2423anbi1d 461 . . . . . . . . . . . 12
25 climcl 11081 . . . . . . . . . . . . . . 15
2612, 25syl 14 . . . . . . . . . . . . . 14
2726ad2antrr 480 . . . . . . . . . . . . 13
28 rpre 9475 . . . . . . . . . . . . . 14
2928ad2antlr 481 . . . . . . . . . . . . 13
30 abs3lem 10913 . . . . . . . . . . . . 13
3121, 27, 19, 29, 30syl22anc 1218 . . . . . . . . . . . 12
3224, 31sylbid 149 . . . . . . . . . . 11
3332anassrs 398 . . . . . . . . . 10
3433expimpd 361 . . . . . . . . 9
3518, 34syl5bi 151 . . . . . . . 8
3617, 35sylan2 284 . . . . . . 7
3736anassrs 398 . . . . . 6
3837ralimdva 2502 . . . . 5
3938reximdva 2537 . . . 4
4016, 39mpd 13 . . 3
4140ralrimiva 2508 . 2
42 2clim.3 . . 3
43 eqidd 2141 . . 3
447, 8, 42, 43, 26, 20clim2c 11083 . 2
4541, 44mpbird 166 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wceq 1332   wcel 1481  wral 2417  wrex 2418   class class class wbr 3935  cfv 5129  (class class class)co 5780  cc 7640  cr 7641   clt 7822   cmin 7955   cdiv 8454  c2 8793  cz 9076  cuz 9348  crp 9468  cabs 10799   cli 11077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4049  ax-sep 4052  ax-nul 4060  ax-pow 4104  ax-pr 4137  ax-un 4361  ax-setind 4458  ax-iinf 4508  ax-cnex 7733  ax-resscn 7734  ax-1cn 7735  ax-1re 7736  ax-icn 7737  ax-addcl 7738  ax-addrcl 7739  ax-mulcl 7740  ax-mulrcl 7741  ax-addcom 7742  ax-mulcom 7743  ax-addass 7744  ax-mulass 7745  ax-distr 7746  ax-i2m1 7747  ax-0lt1 7748  ax-1rid 7749  ax-0id 7750  ax-rnegex 7751  ax-precex 7752  ax-cnre 7753  ax-pre-ltirr 7754  ax-pre-ltwlin 7755  ax-pre-lttrn 7756  ax-pre-apti 7757  ax-pre-ltadd 7758  ax-pre-mulgt0 7759  ax-pre-mulext 7760  ax-arch 7761  ax-caucvg 7762 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3076  df-un 3078  df-in 3080  df-ss 3087  df-nul 3367  df-if 3478  df-pw 3515  df-sn 3536  df-pr 3537  df-op 3539  df-uni 3743  df-int 3778  df-iun 3821  df-br 3936  df-opab 3996  df-mpt 3997  df-tr 4033  df-id 4221  df-po 4224  df-iso 4225  df-iord 4294  df-on 4296  df-ilim 4297  df-suc 4299  df-iom 4511  df-xp 4551  df-rel 4552  df-cnv 4553  df-co 4554  df-dm 4555  df-rn 4556  df-res 4557  df-ima 4558  df-iota 5094  df-fun 5131  df-fn 5132  df-f 5133  df-f1 5134  df-fo 5135  df-f1o 5136  df-fv 5137  df-riota 5736  df-ov 5783  df-oprab 5784  df-mpo 5785  df-1st 6044  df-2nd 6045  df-recs 6208  df-frec 6294  df-pnf 7824  df-mnf 7825  df-xr 7826  df-ltxr 7827  df-le 7828  df-sub 7957  df-neg 7958  df-reap 8359  df-ap 8366  df-div 8455  df-inn 8743  df-2 8801  df-3 8802  df-4 8803  df-n0 9000  df-z 9077  df-uz 9349  df-rp 9469  df-seqfrec 10248  df-exp 10322  df-cj 10644  df-re 10645  df-im 10646  df-rsqrt 10800  df-abs 10801  df-clim 11078 This theorem is referenced by:  mertensabs  11336
 Copyright terms: Public domain W3C validator