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

Theorem iserex 13120
Description: An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)
Hypotheses
Ref Expression
clim2ser.1  |-  Z  =  ( ZZ>= `  M )
iserex.2  |-  ( ph  ->  N  e.  Z )
iserex.3  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
Assertion
Ref Expression
iserex  |-  ( ph  ->  (  seq M (  +  ,  F )  e.  dom  ~~>  <->  seq N (  +  ,  F )  e.  dom  ~~>  ) )
Distinct variable groups:    k, F    k, M    k, N    ph, k    k, Z

Proof of Theorem iserex
StepHypRef Expression
1 seqeq1 11795 . . . . 5  |-  ( N  =  M  ->  seq N (  +  ,  F )  =  seq M (  +  ,  F ) )
21eleq1d 2501 . . . 4  |-  ( N  =  M  ->  (  seq N (  +  ,  F )  e.  dom  ~~>  <->  seq M (  +  ,  F )  e.  dom  ~~>  ) )
32bicomd 201 . . 3  |-  ( N  =  M  ->  (  seq M (  +  ,  F )  e.  dom  ~~>  <->  seq N (  +  ,  F )  e.  dom  ~~>  ) )
43a1i 11 . 2  |-  ( ph  ->  ( N  =  M  ->  (  seq M
(  +  ,  F
)  e.  dom  ~~>  <->  seq N (  +  ,  F )  e.  dom  ~~>  ) ) )
5 simpll 748 . . . . . . 7  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  ph )
6 iserex.2 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  Z )
7 clim2ser.1 . . . . . . . . . . . 12  |-  Z  =  ( ZZ>= `  M )
86, 7syl6eleq 2525 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
9 eluzelz 10860 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
108, 9syl 16 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ZZ )
1110zcnd 10738 . . . . . . . . 9  |-  ( ph  ->  N  e.  CC )
12 ax-1cn 9330 . . . . . . . . 9  |-  1  e.  CC
13 npcan 9609 . . . . . . . . 9  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
1411, 12, 13sylancl 657 . . . . . . . 8  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
1514seqeq1d 11798 . . . . . . 7  |-  ( ph  ->  seq ( ( N  -  1 )  +  1 ) (  +  ,  F )  =  seq N (  +  ,  F ) )
165, 15syl 16 . . . . . 6  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  seq ( ( N  -  1 )  +  1 ) (  +  ,  F )  =  seq N (  +  ,  F ) )
17 simplr 749 . . . . . . . 8  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  ( N  - 
1 )  e.  (
ZZ>= `  M ) )
1817, 7syl6eleqr 2526 . . . . . . 7  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  ( N  - 
1 )  e.  Z
)
19 iserex.3 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
205, 19sylan 468 . . . . . . 7  |-  ( ( ( ( ph  /\  ( N  -  1
)  e.  ( ZZ>= `  M ) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  /\  k  e.  Z
)  ->  ( F `  k )  e.  CC )
21 simpr 458 . . . . . . . 8  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
22 climdm 13018 . . . . . . . 8  |-  (  seq M (  +  ,  F )  e.  dom  ~~>  <->  seq M (  +  ,  F )  ~~>  (  ~~>  `  seq M (  +  ,  F ) ) )
2321, 22sylib 196 . . . . . . 7  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  seq M (  +  ,  F )  ~~>  (  ~~>  `  seq M (  +  ,  F ) ) )
247, 18, 20, 23clim2ser 13118 . . . . . 6  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  seq ( ( N  -  1 )  +  1 ) (  +  ,  F )  ~~>  ( (  ~~>  `
 seq M (  +  ,  F ) )  -  (  seq M
(  +  ,  F
) `  ( N  -  1 ) ) ) )
2516, 24eqbrtrrd 4304 . . . . 5  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  seq N (  +  ,  F )  ~~>  ( (  ~~>  `
 seq M (  +  ,  F ) )  -  (  seq M
(  +  ,  F
) `  ( N  -  1 ) ) ) )
26 climrel 12956 . . . . . 6  |-  Rel  ~~>
2726releldmi 5065 . . . . 5  |-  (  seq N (  +  ,  F )  ~~>  ( (  ~~>  `
 seq M (  +  ,  F ) )  -  (  seq M
(  +  ,  F
) `  ( N  -  1 ) ) )  ->  seq N (  +  ,  F )  e.  dom  ~~>  )
2825, 27syl 16 . . . 4  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq M (  +  ,  F )  e.  dom  ~~>  )  ->  seq N (  +  ,  F )  e. 
dom 
~~>  )
29 simpr 458 . . . . . . . 8  |-  ( (
ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M )
)  ->  ( N  -  1 )  e.  ( ZZ>= `  M )
)
3029, 7syl6eleqr 2526 . . . . . . 7  |-  ( (
ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M )
)  ->  ( N  -  1 )  e.  Z )
3130adantr 462 . . . . . 6  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  ( N  - 
1 )  e.  Z
)
32 simpll 748 . . . . . . 7  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  ph )
3332, 19sylan 468 . . . . . 6  |-  ( ( ( ( ph  /\  ( N  -  1
)  e.  ( ZZ>= `  M ) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  /\  k  e.  Z
)  ->  ( F `  k )  e.  CC )
3432, 15syl 16 . . . . . . 7  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  seq ( ( N  -  1 )  +  1 ) (  +  ,  F )  =  seq N (  +  ,  F ) )
35 simpr 458 . . . . . . . 8  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  seq N (  +  ,  F )  e. 
dom 
~~>  )
36 climdm 13018 . . . . . . . 8  |-  (  seq N (  +  ,  F )  e.  dom  ~~>  <->  seq N (  +  ,  F )  ~~>  (  ~~>  `  seq N (  +  ,  F ) ) )
3735, 36sylib 196 . . . . . . 7  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  seq N (  +  ,  F )  ~~>  (  ~~>  `  seq N (  +  ,  F ) ) )
3834, 37eqbrtrd 4302 . . . . . 6  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  seq ( ( N  -  1 )  +  1 ) (  +  ,  F )  ~~>  (  ~~>  `  seq N (  +  ,  F ) ) )
397, 31, 33, 38clim2ser2 13119 . . . . 5  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  seq M (  +  ,  F )  ~~>  ( (  ~~>  `
 seq N (  +  ,  F ) )  +  (  seq M
(  +  ,  F
) `  ( N  -  1 ) ) ) )
4026releldmi 5065 . . . . 5  |-  (  seq M (  +  ,  F )  ~~>  ( (  ~~>  `
 seq N (  +  ,  F ) )  +  (  seq M
(  +  ,  F
) `  ( N  -  1 ) ) )  ->  seq M (  +  ,  F )  e.  dom  ~~>  )
4139, 40syl 16 . . . 4  |-  ( ( ( ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M
) )  /\  seq N (  +  ,  F )  e.  dom  ~~>  )  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
4228, 41impbida 823 . . 3  |-  ( (
ph  /\  ( N  -  1 )  e.  ( ZZ>= `  M )
)  ->  (  seq M (  +  ,  F )  e.  dom  ~~>  <->  seq N (  +  ,  F )  e.  dom  ~~>  ) )
4342ex 434 . 2  |-  ( ph  ->  ( ( N  - 
1 )  e.  (
ZZ>= `  M )  -> 
(  seq M (  +  ,  F )  e. 
dom 
~~> 
<->  seq N (  +  ,  F )  e. 
dom 
~~>  ) ) )
44 uzm1 10881 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  =  M  \/  ( N  -  1 )  e.  ( ZZ>= `  M
) ) )
458, 44syl 16 . 2  |-  ( ph  ->  ( N  =  M  \/  ( N  - 
1 )  e.  (
ZZ>= `  M ) ) )
464, 43, 45mpjaod 381 1  |-  ( ph  ->  (  seq M (  +  ,  F )  e.  dom  ~~>  <->  seq N (  +  ,  F )  e.  dom  ~~>  ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1364    e. wcel 1757   class class class wbr 4282   dom cdm 4829   ` cfv 5408  (class class class)co 6082   CCcc 9270   1c1 9273    + caddc 9275    - cmin 9585   ZZcz 10636   ZZ>=cuz 10851    seqcseq 11792    ~~> cli 12948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-inf2 7837  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-pre-sup 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-sup 7681  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-2 10370  df-3 10371  df-n0 10570  df-z 10637  df-uz 10852  df-rp 10982  df-fz 11427  df-seq 11793  df-exp 11852  df-cj 12574  df-re 12575  df-im 12576  df-sqr 12710  df-abs 12711  df-clim 12952
This theorem is referenced by:  isumsplit  13288  isumrpcl  13291  climcnds  13299  geolim2  13316  cvgrat  13328  mertenslem1  13329  mertenslem2  13330  mertens  13331  eftlcvg  13375  rpnnen2lem5  13486  prmreclem5  13966  prmreclem6  13967  dvradcnv  21773  abelthlem7  21790  log2tlbnd  22227  lgamgulmlem4  26868
  Copyright terms: Public domain W3C validator