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