This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 GG, 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 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ 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 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 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 ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ 𝐴 𝐵