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

Theorem seq3-1 10389
Description: Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.)
Hypotheses
Ref Expression
seq3-1.m  |-  ( ph  ->  M  e.  ZZ )
seq3-1.f  |-  ( (
ph  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  S
)
seq3-1.pl  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
Assertion
Ref Expression
seq3-1  |-  ( ph  ->  (  seq M ( 
.+  ,  F ) `
 M )  =  ( F `  M
) )
Distinct variable groups:    x,  .+ , y    x, F, y    x, M, y    x, S, y    ph, x, y

Proof of Theorem seq3-1
Dummy variables  a  b  w  z  c  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seq3-1.m . 2  |-  ( ph  ->  M  e.  ZZ )
2 fveq2 5483 . . . 4  |-  ( x  =  M  ->  ( F `  x )  =  ( F `  M ) )
32eleq1d 2233 . . 3  |-  ( x  =  M  ->  (
( F `  x
)  e.  S  <->  ( F `  M )  e.  S
) )
4 seq3-1.f . . . 4  |-  ( (
ph  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  S
)
54ralrimiva 2537 . . 3  |-  ( ph  ->  A. x  e.  (
ZZ>= `  M ) ( F `  x )  e.  S )
6 uzid 9474 . . . 4  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
71, 6syl 14 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
83, 5, 7rspcdva 2833 . 2  |-  ( ph  ->  ( F `  M
)  e.  S )
9 ssv 3162 . . 3  |-  S  C_  _V
109a1i 9 . 2  |-  ( ph  ->  S  C_  _V )
11 seq3-1.pl . . 3  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
124, 11iseqovex 10385 . 2  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  S
) )  ->  (
x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )  e.  S )
13 iseqvalcbv 10386 . 2  |- frec ( ( a  e.  ( ZZ>= `  M ) ,  b  e.  _V  |->  <. (
a  +  1 ) ,  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) b ) >. ) ,  <. M ,  ( F `  M )
>. )  = frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. )
141, 13, 4, 11seq3val 10387 . 2  |-  ( ph  ->  seq M (  .+  ,  F )  =  ran frec ( ( a  e.  (
ZZ>= `  M ) ,  b  e.  _V  |->  <.
( a  +  1 ) ,  ( a ( c  e.  (
ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `
 ( c  +  1 ) ) ) ) b ) >.
) ,  <. M , 
( F `  M
) >. ) )
151, 8, 10, 12, 13, 14frecuzrdg0t 10351 1  |-  ( ph  ->  (  seq M ( 
.+  ,  F ) `
 M )  =  ( F `  M
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1342    e. wcel 2135   _Vcvv 2724    C_ wss 3114   <.cop 3576   ` cfv 5185  (class class class)co 5839    e. cmpo 5841  freccfrec 6352   1c1 7748    + caddc 7750   ZZcz 9185   ZZ>=cuz 9460    seqcseq 10374
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4094  ax-sep 4097  ax-nul 4105  ax-pow 4150  ax-pr 4184  ax-un 4408  ax-setind 4511  ax-iinf 4562  ax-cnex 7838  ax-resscn 7839  ax-1cn 7840  ax-1re 7841  ax-icn 7842  ax-addcl 7843  ax-addrcl 7844  ax-mulcl 7845  ax-addcom 7847  ax-addass 7849  ax-distr 7851  ax-i2m1 7852  ax-0lt1 7853  ax-0id 7855  ax-rnegex 7856  ax-cnre 7858  ax-pre-ltirr 7859  ax-pre-ltwlin 7860  ax-pre-lttrn 7861  ax-pre-ltadd 7863
This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2726  df-sbc 2950  df-csb 3044  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3408  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-int 3822  df-iun 3865  df-br 3980  df-opab 4041  df-mpt 4042  df-tr 4078  df-id 4268  df-iord 4341  df-on 4343  df-ilim 4344  df-suc 4346  df-iom 4565  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-rn 4612  df-res 4613  df-ima 4614  df-iota 5150  df-fun 5187  df-fn 5188  df-f 5189  df-f1 5190  df-fo 5191  df-f1o 5192  df-fv 5193  df-riota 5795  df-ov 5842  df-oprab 5843  df-mpo 5844  df-1st 6103  df-2nd 6104  df-recs 6267  df-frec 6353  df-pnf 7929  df-mnf 7930  df-xr 7931  df-ltxr 7932  df-le 7933  df-sub 8065  df-neg 8066  df-inn 8852  df-n0 9109  df-z 9186  df-uz 9461  df-seqfrec 10375
This theorem is referenced by:  seq3clss  10396  seq3fveq2  10398  seq3fveq  10400  seq3shft2  10402  seq3split  10408  seq3-1p  10409  seq3caopr3  10410  seq3id3  10436  seq3id  10437  seq3homo  10439  seq3z  10440  ser3ge0  10446  exp3vallem  10450  exp1  10455  fac1  10636  bcn2  10671  seq3coll  10749  resqrexlemf1  10944  sumsnf  11344  isumrpcl  11429  clim2prod  11474  prodfap0  11480  prodfrecap  11481  prodsnf  11527  ef0lem  11595  ege2le3  11606  efgt1p2  11630  efgt1p  11631  ialgr0  11970  pcmpt  12267
  Copyright terms: Public domain W3C validator