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

Theorem ntrivcvg 13763
Description: A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.)
Hypotheses
Ref Expression
ntrivcvg.1  |-  Z  =  ( ZZ>= `  M )
ntrivcvg.2  |-  ( ph  ->  E. n  e.  Z  E. y ( y  =/=  0  /\  seq n
(  x.  ,  F
)  ~~>  y ) )
ntrivcvg.3  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
Assertion
Ref Expression
ntrivcvg  |-  ( ph  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  )
Distinct variable groups:    k, F, n, y    ph, k, y   
k, M, n, y    ph, n, y    k, Z, y
Allowed substitution hint:    Z( n)

Proof of Theorem ntrivcvg
StepHypRef Expression
1 ntrivcvg.2 . 2  |-  ( ph  ->  E. n  e.  Z  E. y ( y  =/=  0  /\  seq n
(  x.  ,  F
)  ~~>  y ) )
2 uzm1 11073 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  M
)  ->  ( n  =  M  \/  (
n  -  1 )  e.  ( ZZ>= `  M
) ) )
3 ntrivcvg.1 . . . . . . . . 9  |-  Z  =  ( ZZ>= `  M )
42, 3eleq2s 2508 . . . . . . . 8  |-  ( n  e.  Z  ->  (
n  =  M  \/  ( n  -  1
)  e.  ( ZZ>= `  M ) ) )
54ad2antlr 725 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  ( n  =  M  \/  ( n  -  1 )  e.  ( ZZ>= `  M )
) )
6 seqeq1 12062 . . . . . . . . . . 11  |-  ( n  =  M  ->  seq n (  x.  ,  F )  =  seq M (  x.  ,  F ) )
76breq1d 4402 . . . . . . . . . 10  |-  ( n  =  M  ->  (  seq n (  x.  ,  F )  ~~>  y  <->  seq M (  x.  ,  F )  ~~>  y ) )
8 seqex 12061 . . . . . . . . . . 11  |-  seq M
(  x.  ,  F
)  e.  _V
9 vex 3059 . . . . . . . . . . 11  |-  y  e. 
_V
108, 9breldm 5147 . . . . . . . . . 10  |-  (  seq M (  x.  ,  F )  ~~>  y  ->  seq M (  x.  ,  F )  e.  dom  ~~>  )
117, 10syl6bi 228 . . . . . . . . 9  |-  ( n  =  M  ->  (  seq n (  x.  ,  F )  ~~>  y  ->  seq M (  x.  ,  F )  e.  dom  ~~>  ) )
1211adantld 465 . . . . . . . 8  |-  ( n  =  M  ->  (
( ( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  ) )
13 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  n  e.  Z )  /\  ( n  -  1 )  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  (
n  -  1 )  e.  Z )
14 ntrivcvg.3 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
1514adantlr 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  Z )  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
1615adantlr 713 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  n  e.  Z )  /\  ( n  -  1 )  e.  Z )  /\  k  e.  Z
)  ->  ( F `  k )  e.  CC )
1716adantlr 713 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  n  e.  Z )  /\  ( n  - 
1 )  e.  Z
)  /\  seq n
(  x.  ,  F
)  ~~>  y )  /\  k  e.  Z )  ->  ( F `  k
)  e.  CC )
18 uzssz 11062 . . . . . . . . . . . . . . . . . . . 20  |-  ( ZZ>= `  M )  C_  ZZ
193, 18eqsstri 3469 . . . . . . . . . . . . . . . . . . 19  |-  Z  C_  ZZ
20 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  ->  n  e.  Z )
2119, 20sseldi 3437 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  ->  n  e.  ZZ )
2221zcnd 10927 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  ->  n  e.  CC )
23 1cnd 9560 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  -> 
1  e.  CC )
2422, 23npcand 9889 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  -> 
( ( n  - 
1 )  +  1 )  =  n )
2524seqeq1d 12065 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  ->  seq ( ( n  - 
1 )  +  1 ) (  x.  ,  F )  =  seq n (  x.  ,  F ) )
2625breq1d 4402 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  Z )  /\  (
n  -  1 )  e.  Z )  -> 
(  seq ( ( n  -  1 )  +  1 ) (  x.  ,  F )  ~~>  y  <->  seq n
(  x.  ,  F
)  ~~>  y ) )
2726biimpar 483 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  n  e.  Z )  /\  ( n  -  1 )  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq ( ( n  - 
1 )  +  1 ) (  x.  ,  F )  ~~>  y )
283, 13, 17, 27clim2prod 13754 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  Z )  /\  ( n  -  1 )  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  ~~>  ( (  seq M (  x.  ,  F ) `  ( n  -  1
) )  x.  y
) )
29 ovex 6260 . . . . . . . . . . . . 13  |-  ( (  seq M (  x.  ,  F ) `  ( n  -  1
) )  x.  y
)  e.  _V
308, 29breldm 5147 . . . . . . . . . . . 12  |-  (  seq M (  x.  ,  F )  ~~>  ( (  seq M (  x.  ,  F ) `  ( n  -  1
) )  x.  y
)  ->  seq M (  x.  ,  F )  e.  dom  ~~>  )
3128, 30syl 17 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  Z )  /\  ( n  -  1 )  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e.  dom  ~~>  )
3231an32s 803 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  /\  ( n  - 
1 )  e.  Z
)  ->  seq M (  x.  ,  F )  e.  dom  ~~>  )
3332expcom 433 . . . . . . . . 9  |-  ( ( n  -  1 )  e.  Z  ->  (
( ( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  ) )
343eqcomi 2413 . . . . . . . . 9  |-  ( ZZ>= `  M )  =  Z
3533, 34eleq2s 2508 . . . . . . . 8  |-  ( ( n  -  1 )  e.  ( ZZ>= `  M
)  ->  ( (
( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  ) )
3612, 35jaoi 377 . . . . . . 7  |-  ( ( n  =  M  \/  ( n  -  1
)  e.  ( ZZ>= `  M ) )  -> 
( ( ( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e.  dom  ~~>  ) )
375, 36mpcom 34 . . . . . 6  |-  ( ( ( ph  /\  n  e.  Z )  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  )
3837ex 432 . . . . 5  |-  ( (
ph  /\  n  e.  Z )  ->  (  seq n (  x.  ,  F )  ~~>  y  ->  seq M (  x.  ,  F )  e.  dom  ~~>  ) )
3938adantld 465 . . . 4  |-  ( (
ph  /\  n  e.  Z )  ->  (
( y  =/=  0  /\  seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  ) )
4039exlimdv 1743 . . 3  |-  ( (
ph  /\  n  e.  Z )  ->  ( E. y ( y  =/=  0  /\  seq n
(  x.  ,  F
)  ~~>  y )  ->  seq M (  x.  ,  F )  e.  dom  ~~>  ) )
4140rexlimdva 2893 . 2  |-  ( ph  ->  ( E. n  e.  Z  E. y ( y  =/=  0  /\ 
seq n (  x.  ,  F )  ~~>  y )  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  ) )
421, 41mpd 15 1  |-  ( ph  ->  seq M (  x.  ,  F )  e. 
dom 
~~>  )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 366    /\ wa 367    = wceq 1403   E.wex 1631    e. wcel 1840    =/= wne 2596   E.wrex 2752   class class class wbr 4392   dom cdm 4940   ` cfv 5523  (class class class)co 6232   CCcc 9438   0cc0 9440   1c1 9441    + caddc 9443    x. cmul 9445    - cmin 9759   ZZcz 10823   ZZ>=cuz 11043    seqcseq 12059    ~~> cli 13361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4569  ax-pr 4627  ax-un 6528  ax-inf2 8009  ax-cnex 9496  ax-resscn 9497  ax-1cn 9498  ax-icn 9499  ax-addcl 9500  ax-addrcl 9501  ax-mulcl 9502  ax-mulrcl 9503  ax-mulcom 9504  ax-addass 9505  ax-mulass 9506  ax-distr 9507  ax-i2m1 9508  ax-1ne0 9509  ax-1rid 9510  ax-rnegex 9511  ax-rrecex 9512  ax-cnre 9513  ax-pre-lttri 9514  ax-pre-lttrn 9515  ax-pre-ltadd 9516  ax-pre-mulgt0 9517  ax-pre-sup 9518
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 973  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-nel 2599  df-ral 2756  df-rex 2757  df-reu 2758  df-rmo 2759  df-rab 2760  df-v 3058  df-sbc 3275  df-csb 3371  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-pss 3427  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-tp 3974  df-op 3976  df-uni 4189  df-iun 4270  df-br 4393  df-opab 4451  df-mpt 4452  df-tr 4487  df-eprel 4731  df-id 4735  df-po 4741  df-so 4742  df-fr 4779  df-we 4781  df-ord 4822  df-on 4823  df-lim 4824  df-suc 4825  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-f1 5528  df-fo 5529  df-f1o 5530  df-fv 5531  df-riota 6194  df-ov 6235  df-oprab 6236  df-mpt2 6237  df-om 6637  df-1st 6736  df-2nd 6737  df-recs 6997  df-rdg 7031  df-er 7266  df-en 7473  df-dom 7474  df-sdom 7475  df-sup 7853  df-pnf 9578  df-mnf 9579  df-xr 9580  df-ltxr 9581  df-le 9582  df-sub 9761  df-neg 9762  df-div 10166  df-nn 10495  df-2 10553  df-3 10554  df-n0 10755  df-z 10824  df-uz 11044  df-rp 11182  df-fz 11642  df-seq 12060  df-exp 12119  df-cj 12986  df-re 12987  df-im 12988  df-sqrt 13122  df-abs 13123  df-clim 13365
This theorem is referenced by:  iprodclim2  13849  iprodcl  13851
  Copyright terms: Public domain W3C validator