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

Theorem seqp1 11807
Description: Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.)
Assertion
Ref Expression
seqp1  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq M (  .+  ,  F ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  F ) `  N
)  .+  ( F `  ( N  +  1 ) ) ) )

Proof of Theorem seqp1
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluzel2 10856 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
2 fveq2 5681 . . . . . 6  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
( ZZ>= `  M )  =  ( ZZ>= `  if ( M  e.  ZZ ,  M ,  0 ) ) )
32eleq2d 2502 . . . . 5  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
( N  e.  (
ZZ>= `  M )  <->  N  e.  ( ZZ>= `  if ( M  e.  ZZ ,  M ,  0 ) ) ) )
4 seqeq1 11795 . . . . . . 7  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  ->  seq M (  .+  ,  F )  =  seq if ( M  e.  ZZ ,  M ,  0 ) (  .+  ,  F
) )
54fveq1d 5683 . . . . . 6  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
(  seq M (  .+  ,  F ) `  ( N  +  1 ) )  =  (  seq
if ( M  e.  ZZ ,  M , 
0 ) (  .+  ,  F ) `  ( N  +  1 ) ) )
64fveq1d 5683 . . . . . . 7  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
(  seq M (  .+  ,  F ) `  N
)  =  (  seq
if ( M  e.  ZZ ,  M , 
0 ) (  .+  ,  F ) `  N
) )
76oveq2d 6098 . . . . . 6  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
( N ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) (  seq M (  .+  ,  F ) `  N
) )  =  ( N ( z  e. 
_V ,  w  e. 
_V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) (  seq
if ( M  e.  ZZ ,  M , 
0 ) (  .+  ,  F ) `  N
) ) )
85, 7eqeq12d 2449 . . . . 5  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
( (  seq M
(  .+  ,  F
) `  ( N  +  1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) (  seq M ( 
.+  ,  F ) `
 N ) )  <-> 
(  seq if ( M  e.  ZZ ,  M ,  0 ) ( 
.+  ,  F ) `
 ( N  + 
1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) (  seq
if ( M  e.  ZZ ,  M , 
0 ) (  .+  ,  F ) `  N
) ) ) )
93, 8imbi12d 320 . . . 4  |-  ( M  =  if ( M  e.  ZZ ,  M ,  0 )  -> 
( ( N  e.  ( ZZ>= `  M )  ->  (  seq M ( 
.+  ,  F ) `
 ( N  + 
1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) (  seq M (  .+  ,  F ) `  N
) ) )  <->  ( N  e.  ( ZZ>= `  if ( M  e.  ZZ ,  M ,  0 ) )  ->  (  seq if ( M  e.  ZZ ,  M ,  0 ) (  .+  ,  F
) `  ( N  +  1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) (  seq if ( M  e.  ZZ ,  M ,  0 ) (  .+  ,  F
) `  N )
) ) ) )
10 0z 10647 . . . . . 6  |-  0  e.  ZZ
1110elimel 3842 . . . . 5  |-  if ( M  e.  ZZ ,  M ,  0 )  e.  ZZ
12 eqid 2435 . . . . 5  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  if ( M  e.  ZZ ,  M , 
0 ) )  |`  om )  =  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  if ( M  e.  ZZ ,  M , 
0 ) )  |`  om )
13 fvex 5691 . . . . 5  |-  ( F `
 if ( M  e.  ZZ ,  M ,  0 ) )  e.  _V
14 eqid 2435 . . . . 5  |-  ( rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e. 
_V ,  w  e. 
_V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. if ( M  e.  ZZ ,  M ,  0 ) ,  ( F `  if ( M  e.  ZZ ,  M ,  0 ) ) >. )  |`  om )  =  ( rec (
( x  e.  _V ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. if ( M  e.  ZZ ,  M ,  0 ) ,  ( F `  if ( M  e.  ZZ ,  M ,  0 ) ) >. )  |`  om )
1514seqval 11803 . . . . 5  |-  seq if ( M  e.  ZZ ,  M ,  0 ) (  .+  ,  F
)  =  ran  ( rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e. 
_V ,  w  e. 
_V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. if ( M  e.  ZZ ,  M ,  0 ) ,  ( F `  if ( M  e.  ZZ ,  M ,  0 ) ) >. )  |`  om )
1611, 12, 13, 14, 15uzrdgsuci 11769 . . . 4  |-  ( N  e.  ( ZZ>= `  if ( M  e.  ZZ ,  M ,  0 ) )  ->  (  seq if ( M  e.  ZZ ,  M ,  0 ) (  .+  ,  F
) `  ( N  +  1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) (  seq if ( M  e.  ZZ ,  M ,  0 ) (  .+  ,  F
) `  N )
) )
179, 16dedth 3831 . . 3  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  ->  (  seq M (  .+  ,  F ) `  ( N  +  1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) (  seq M
(  .+  ,  F
) `  N )
) ) )
181, 17mpcom 36 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq M (  .+  ,  F ) `  ( N  +  1 ) )  =  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) (  seq M
(  .+  ,  F
) `  N )
) )
19 elex 2973 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  _V )
20 fvex 5691 . . 3  |-  (  seq M (  .+  ,  F ) `  N
)  e.  _V
21 oveq1 6089 . . . . . 6  |-  ( z  =  N  ->  (
z  +  1 )  =  ( N  + 
1 ) )
2221fveq2d 5685 . . . . 5  |-  ( z  =  N  ->  ( F `  ( z  +  1 ) )  =  ( F `  ( N  +  1
) ) )
2322oveq2d 6098 . . . 4  |-  ( z  =  N  ->  (
w  .+  ( F `  ( z  +  1 ) ) )  =  ( w  .+  ( F `  ( N  +  1 ) ) ) )
24 oveq1 6089 . . . 4  |-  ( w  =  (  seq M
(  .+  ,  F
) `  N )  ->  ( w  .+  ( F `  ( N  +  1 ) ) )  =  ( (  seq M (  .+  ,  F ) `  N
)  .+  ( F `  ( N  +  1 ) ) ) )
25 eqid 2435 . . . 4  |-  ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) )  =  ( z  e.  _V ,  w  e.  _V  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) )
26 ovex 6107 . . . 4  |-  ( (  seq M (  .+  ,  F ) `  N
)  .+  ( F `  ( N  +  1 ) ) )  e. 
_V
2723, 24, 25, 26ovmpt2 6217 . . 3  |-  ( ( N  e.  _V  /\  (  seq M (  .+  ,  F ) `  N
)  e.  _V )  ->  ( N ( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) (  seq M (  .+  ,  F ) `  N
) )  =  ( (  seq M ( 
.+  ,  F ) `
 N )  .+  ( F `  ( N  +  1 ) ) ) )
2819, 20, 27sylancl 657 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N
( z  e.  _V ,  w  e.  _V  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) (  seq M
(  .+  ,  F
) `  N )
)  =  ( (  seq M (  .+  ,  F ) `  N
)  .+  ( F `  ( N  +  1 ) ) ) )
2918, 28eqtrd 2467 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq M (  .+  ,  F ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  F ) `  N
)  .+  ( F `  ( N  +  1 ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1757   _Vcvv 2964   ifcif 3781   <.cop 3873    e. cmpt 4340    |` cres 4831   ` cfv 5408  (class class class)co 6082    e. cmpt2 6084   omcom 6467   reccrdg 6853   0cc0 9272   1c1 9273    + caddc 9275   ZZcz 10636   ZZ>=cuz 10851    seqcseq 11792
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-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  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
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-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-2nd 6569  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313  df-n0 10570  df-z 10637  df-uz 10852  df-seq 11793
This theorem is referenced by:  seqp1i  11808  seqm1  11809  seqcl2  11810  seqfveq2  11814  seqshft2  11818  sermono  11824  seqsplit  11825  seqcaopr3  11827  seqf1olem2a  11830  seqf1olem2  11832  seqid2  11838  seqhomo  11839  ser1const  11848  expp1  11858  facp1  12042  seqcoll  12202  climserle  13126  iseraltlem2  13146  iseraltlem3  13147  climcndslem1  13297  climcndslem2  13298  ruclem7  13503  sadcp1  13636  smupp1  13661  seq1st  13731  algrp1  13734  eulerthlem2  13842  pcmpt  13939  gsumprval  15496  mulgnnp1  15617  ovolunlem1a  20823  voliunlem1  20875  volsup  20881  dvnp1  21243  bposlem5  22514  gxnn0suc  23576  opsqrlem5  25373  esumfzf  26374  esumpcvgval  26383  sseqp1  26628  rrvsum  26687  gsumnunsn  26787  relexpsucr  27181  clim2prod  27252  prodfn0  27258  prodfrec  27259  ntrivcvgfvn0  27263  iprodefisumlem  27353  faclimlem1  27398  heiborlem4  28559  heiborlem6  28561  fmul01  29608  fmuldfeqlem1  29610  stoweidlem3  29646  wallispilem4  29711  wallispi2lem1  29714  wallispi2lem2  29715
  Copyright terms: Public domain W3C validator