Metamath Proof Explorer


Theorem nfsumOLD

Description: Obsolete version of nfsum as of 24-Feb-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses nfsumOLD.1 𝑥 𝐴
nfsumOLD.2 𝑥 𝐵
Assertion nfsumOLD 𝑥 Σ 𝑘𝐴 𝐵

Proof

Step Hyp Ref Expression
1 nfsumOLD.1 𝑥 𝐴
2 nfsumOLD.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 nfcsb 𝑥 𝑛 / 𝑘 𝐵
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 nfcsb 𝑥 ( 𝑓𝑛 ) / 𝑘 𝐵
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 nfiota 𝑥 ( ℩ 𝑧 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑧 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
37 3 36 nfcxfr 𝑥 Σ 𝑘𝐴 𝐵