Metamath Proof Explorer

Theorem nfsum

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 . Version of nfsum with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 11-Dec-2005) (Revised by Gino Giotto, 24-Feb-2024)

Ref Expression
Hypotheses nfsum.1 
|- F/_ x A
nfsum.2 
|- F/_ x B
Assertion nfsum 
|- F/_ x sum_ k e. A B

Proof

Step Hyp Ref Expression
1 nfsum.1 
 |-  F/_ x A
2 nfsum.2 
 |-  F/_ x B
3 df-sum 
 |-  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 ) ) ) )
4 nfcv 
 |-  F/_ x ZZ
5 nfcv 
 |-  F/_ x ( ZZ>= ` m )
6 1 5 nfss 
 |-  F/ x A C_ ( ZZ>= ` m )
7 nfcv 
 |-  F/_ x m
8 nfcv 
 |-  F/_ x +
9 1 nfcri 
 |-  F/ x n e. A
10 nfcv 
 |-  F/_ x n
11 10 2 nfcsbw 
 |-  F/_ x [_ n / k ]_ B
12 nfcv 
 |-  F/_ x 0
13 9 11 12 nfif 
 |-  F/_ x if ( n e. A , [_ n / k ]_ B , 0 )
14 4 13 nfmpt 
 |-  F/_ x ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
15 7 8 14 nfseq 
 |-  F/_ x seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
16 nfcv 
 |-  F/_ x ~~>
17 nfcv 
 |-  F/_ x z
18 15 16 17 nfbr 
 |-  F/ x seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> z
19 6 18 nfan 
 |-  F/ x ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> z )
20 4 19 nfrex 
 |-  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 
 |-  F/_ x NN
22 nfcv 
 |-  F/_ x f
23 nfcv 
 |-  F/_ x ( 1 ... m )
24 22 23 1 nff1o 
 |-  F/ x f : ( 1 ... m ) -1-1-onto-> A
25 nfcv 
 |-  F/_ x 1
26 nfcv 
 |-  F/_ x ( f ` n )
27 26 2 nfcsbw 
 |-  F/_ x [_ ( f ` n ) / k ]_ B
28 21 27 nfmpt 
 |-  F/_ x ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
29 25 8 28 nfseq 
 |-  F/_ x seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) )
30 29 7 nffv 
 |-  F/_ x ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
31 30 nfeq2 
 |-  F/ x z = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
32 24 31 nfan 
 |-  F/ x ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
33 32 nfex 
 |-  F/ x E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
34 21 33 nfrex 
 |-  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 ) )
35 20 34 nfor 
 |-  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 ) ) )
36 35 nfiotaw 
 |-  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 ) ) ) )
37 3 36 nfcxfr 
 |-  F/_ x sum_ k e. A B