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

Theorem clim 11160
 Description: Express the predicate: The limit of complex number sequence is , or converges to . This means that for any real , no matter how small, there always exists an integer such that the absolute difference of any later complex number in the sequence and the limit is less than . (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Hypotheses
Ref Expression
clim.1
clim.3
Assertion
Ref Expression
clim
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem clim
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climrel 11159 . . . . 5
21brrelex2i 4627 . . . 4
32a1i 9 . . 3
4 elex 2723 . . . . 5
54adantr 274 . . . 4
65a1i 9 . . 3
7 clim.1 . . . 4
8 simpr 109 . . . . . . . 8
98eleq1d 2226 . . . . . . 7
10 fveq1 5464 . . . . . . . . . . . . 13
1110adantr 274 . . . . . . . . . . . 12
1211eleq1d 2226 . . . . . . . . . . 11
13 oveq12 5827 . . . . . . . . . . . . . 14
1410, 13sylan 281 . . . . . . . . . . . . 13
1514fveq2d 5469 . . . . . . . . . . . 12
1615breq1d 3975 . . . . . . . . . . 11
1712, 16anbi12d 465 . . . . . . . . . 10
1817ralbidv 2457 . . . . . . . . 9
1918rexbidv 2458 . . . . . . . 8
2019ralbidv 2457 . . . . . . 7
219, 20anbi12d 465 . . . . . 6
22 df-clim 11158 . . . . . 6
2321, 22brabga 4223 . . . . 5
2423ex 114 . . . 4
257, 24syl 14 . . 3
263, 6, 25pm5.21ndd 695 . 2
27 eluzelz 9431 . . . . . . 7
28 clim.3 . . . . . . . . 9
2928eleq1d 2226 . . . . . . . 8
3028oveq1d 5833 . . . . . . . . . 10
3130fveq2d 5469 . . . . . . . . 9
3231breq1d 3975 . . . . . . . 8
3329, 32anbi12d 465 . . . . . . 7
3427, 33sylan2 284 . . . . . 6
3534ralbidva 2453 . . . . 5
3635rexbidv 2458 . . . 4
3736ralbidv 2457 . . 3
3837anbi2d 460 . 2
3926, 38bitrd 187 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1335   wcel 2128  wral 2435  wrex 2436  cvv 2712   class class class wbr 3965  cfv 5167  (class class class)co 5818  cc 7713   clt 7895   cmin 8029  cz 9150  cuz 9422  crp 9542  cabs 10879   cli 11157 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-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-cnex 7806  ax-resscn 7807 This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4252  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-ov 5821  df-neg 8032  df-z 9151  df-uz 9423  df-clim 11158 This theorem is referenced by:  climcl  11161  clim2  11162  climshftlemg  11181
 Copyright terms: Public domain W3C validator