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

Metamath Proof Explorer

Theorem nfsum1

Description: Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypothesis nfsum1.1 ⊢ Ⅎ 𝑘 𝐴
Assertion nfsum1 Ⅎ 𝑘 Σ 𝑘 ∈ 𝐴 𝐵

Proof

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