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

Theorem nfsum 13462
Description: Bound-variable hypothesis builder for sum: if  x is (effectively) not free in  A and  B, it is not free in  sum_ k  e.  A B. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Hypotheses
Ref Expression
nfsum.1  |-  F/_ x A
nfsum.2  |-  F/_ x B
Assertion
Ref Expression
nfsum  |-  F/_ x sum_ k  e.  A  B

Proof of Theorem nfsum
Dummy variables  f  m  n  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 13458 . 2  |-  sum_ k  e.  A  B  =  ( iota z ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  z )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  z  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) ) )
2 nfcv 2622 . . . . 5  |-  F/_ x ZZ
3 nfsum.1 . . . . . . 7  |-  F/_ x A
4 nfcv 2622 . . . . . . 7  |-  F/_ x
( ZZ>= `  m )
53, 4nfss 3490 . . . . . 6  |-  F/ x  A  C_  ( ZZ>= `  m
)
6 nfcv 2622 . . . . . . . 8  |-  F/_ x m
7 nfcv 2622 . . . . . . . 8  |-  F/_ x  +
83nfel2 2640 . . . . . . . . . 10  |-  F/ x  n  e.  A
9 nfcv 2622 . . . . . . . . . . 11  |-  F/_ x n
10 nfsum.2 . . . . . . . . . . 11  |-  F/_ x B
119, 10nfcsb 3446 . . . . . . . . . 10  |-  F/_ x [_ n  /  k ]_ B
12 nfcv 2622 . . . . . . . . . 10  |-  F/_ x
0
138, 11, 12nfif 3961 . . . . . . . . 9  |-  F/_ x if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
142, 13nfmpt 4528 . . . . . . . 8  |-  F/_ x
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
156, 7, 14nfseq 12073 . . . . . . 7  |-  F/_ x  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )
16 nfcv 2622 . . . . . . 7  |-  F/_ x  ~~>
17 nfcv 2622 . . . . . . 7  |-  F/_ x
z
1815, 16, 17nfbr 4484 . . . . . 6  |-  F/ x  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  z
195, 18nfan 1870 . . . . 5  |-  F/ x
( A  C_  ( ZZ>=
`  m )  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  z )
202, 19nfrex 2920 . . . 4  |-  F/ x E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  z )
21 nfcv 2622 . . . . 5  |-  F/_ x NN
22 nfcv 2622 . . . . . . . 8  |-  F/_ x
f
23 nfcv 2622 . . . . . . . 8  |-  F/_ x
( 1 ... m
)
2422, 23, 3nff1o 5805 . . . . . . 7  |-  F/ x  f : ( 1 ... m ) -1-1-onto-> A
25 nfcv 2622 . . . . . . . . . 10  |-  F/_ x
1
26 nfcv 2622 . . . . . . . . . . . 12  |-  F/_ x
( f `  n
)
2726, 10nfcsb 3446 . . . . . . . . . . 11  |-  F/_ x [_ ( f `  n
)  /  k ]_ B
2821, 27nfmpt 4528 . . . . . . . . . 10  |-  F/_ x
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B )
2925, 7, 28nfseq 12073 . . . . . . . . 9  |-  F/_ x  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) )
3029, 6nffv 5864 . . . . . . . 8  |-  F/_ x
(  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m )
3130nfeq2 2639 . . . . . . 7  |-  F/ x  z  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
3224, 31nfan 1870 . . . . . 6  |-  F/ x
( f : ( 1 ... m ) -1-1-onto-> A  /\  z  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) )
3332nfex 1890 . . . . 5  |-  F/ x E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  z  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) )
3421, 33nfrex 2920 . . . 4  |-  F/ x E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  z  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) )
3520, 34nfor 1877 . . 3  |-  F/ x
( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  z )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  z  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) ) )
3635nfiota 5546 . 2  |-  F/_ x
( iota z ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  z )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  z  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) ) )
371, 36nfcxfr 2620 1  |-  F/_ x sum_ k  e.  A  B
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    /\ wa 369    = wceq 1374   E.wex 1591    e. wcel 1762   F/_wnfc 2608   E.wrex 2808   [_csb 3428    C_ wss 3469   ifcif 3932   class class class wbr 4440    |-> cmpt 4498   iotacio 5540   -1-1-onto->wf1o 5578   ` cfv 5579  (class class class)co 6275   0cc0 9481   1c1 9482    + caddc 9484   NNcn 10525   ZZcz 10853   ZZ>=cuz 11071   ...cfz 11661    seqcseq 12063    ~~> cli 13256   sum_csu 13457
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 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-recs 7032  df-rdg 7066  df-seq 12064  df-sum 13458
This theorem is referenced by:  fsum2dlem  13534  fsumcom2  13538  fsumrlim  13574  fsumiun  13584  fsumcn  21102  fsum2cn  21103  nfitg1  21908  nfitg  21909  dvmptfsum  22104  fsumdvdscom  23182  fsumcnf  30929
  Copyright terms: Public domain W3C validator