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 _ x A
nfsum.2 _ x B
Assertion nfsum _ x k A B

Proof

Step Hyp Ref Expression
1 nfsum.1 _ x A
2 nfsum.2 _ x B
3 df-sum k A B = ι z | m A m seq m + n if n A n / k B 0 z m f f : 1 m 1-1 onto A z = seq 1 + n f n / k B m
4 nfcv _ x
5 nfcv _ x m
6 1 5 nfss x A m
7 nfcv _ x m
8 nfcv _ x +
9 1 nfcri x n A
10 nfcv _ x n
11 10 2 nfcsbw _ x n / k B
12 nfcv _ x 0
13 9 11 12 nfif _ x if n A n / k B 0
14 4 13 nfmpt _ x n if n A n / k B 0
15 7 8 14 nfseq _ x seq m + n if n A n / k B 0
16 nfcv _ x
17 nfcv _ x z
18 15 16 17 nfbr x seq m + n if n A n / k B 0 z
19 6 18 nfan x A m seq m + n if n A n / k B 0 z
20 4 19 nfrex x m A m seq m + n if n A n / k B 0 z
21 nfcv _ x
22 nfcv _ x f
23 nfcv _ x 1 m
24 22 23 1 nff1o x f : 1 m 1-1 onto A
25 nfcv _ x 1
26 nfcv _ x f n
27 26 2 nfcsbw _ x f n / k B
28 21 27 nfmpt _ x n f n / k B
29 25 8 28 nfseq _ x seq 1 + n f n / k B
30 29 7 nffv _ x seq 1 + n f n / k B m
31 30 nfeq2 x z = seq 1 + n f n / k B m
32 24 31 nfan x f : 1 m 1-1 onto A z = seq 1 + n f n / k B m
33 32 nfex x f f : 1 m 1-1 onto A z = seq 1 + n f n / k B m
34 21 33 nfrex x m f f : 1 m 1-1 onto A z = seq 1 + n f n / k B m
35 20 34 nfor x m A m seq m + n if n A n / k B 0 z m f f : 1 m 1-1 onto A z = seq 1 + n f n / k B m
36 35 nfiotaw _ x ι z | m A m seq m + n if n A n / k B 0 z m f f : 1 m 1-1 onto A z = seq 1 + n f n / k B m
37 3 36 nfcxfr _ x k A B