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	⊢ Ⅎ 𝑥 𝐴
	nfsum.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfsum	⊢ Ⅎ 𝑥 Σ 𝑘 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfsum.1	⊢ Ⅎ 𝑥 𝐴
2		nfsum.2	⊢ Ⅎ 𝑥 𝐵
3		df-sum	⊢ Σ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑧 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
4		nfcv	⊢ Ⅎ 𝑥 ℤ
5		nfcv	⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑚 )
6	1 5	nfss	⊢ Ⅎ 𝑥 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 )
7		nfcv	⊢ Ⅎ 𝑥 𝑚
8		nfcv	⊢ Ⅎ 𝑥 +
9	1	nfcri	⊢ Ⅎ 𝑥 𝑛 ∈ 𝐴
10		nfcv	⊢ Ⅎ 𝑥 𝑛
11	10 2	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑛 / 𝑘 ⦌ 𝐵
12		nfcv	⊢ Ⅎ 𝑥 0
13	9 11 12	nfif	⊢ Ⅎ 𝑥 if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 )
14	4 13	nfmpt	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
15	7 8 14	nfseq	⊢ Ⅎ 𝑥 seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) )
16		nfcv	⊢ Ⅎ 𝑥 ⇝
17		nfcv	⊢ Ⅎ 𝑥 𝑧
18	15 16 17	nfbr	⊢ Ⅎ 𝑥 seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑧
19	6 18	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑧 )
20	4 19	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑧 )
21		nfcv	⊢ Ⅎ 𝑥 ℕ
22		nfcv	⊢ Ⅎ 𝑥 𝑓
23		nfcv	⊢ Ⅎ 𝑥 ( 1 ... 𝑚 )
24	22 23 1	nff1o	⊢ Ⅎ 𝑥 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴
25		nfcv	⊢ Ⅎ 𝑥 1
26		nfcv	⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑛 )
27	26 2	nfcsbw	⊢ Ⅎ 𝑥 ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵
28	21 27	nfmpt	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
29	25 8 28	nfseq	⊢ Ⅎ 𝑥 seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) )
30	29 7	nffv	⊢ Ⅎ 𝑥 ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 )
31	30	nfeq2	⊢ Ⅎ 𝑥 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 )
32	24 31	nfan	⊢ Ⅎ 𝑥 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
33	32	nfex	⊢ Ⅎ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
34	21 33	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
35	20 34	nfor	⊢ Ⅎ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
36	35	nfiotaw	⊢ Ⅎ 𝑥 ( ℩ 𝑧 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
37	3 36	nfcxfr	⊢ Ⅎ 𝑥 Σ 𝑘 ∈ 𝐴 𝐵