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 Gino Giotto, 24-Feb-2024)

Ref Expression
Hypotheses nfsum.1 ⊢ Ⅎ _ x A
nfsum.2 ⊢ Ⅎ _ x B
Assertion nfsum ⊢ Ⅎ _ x ∑ k ∈ A B

Proof

Step Hyp Ref Expression
1 nfsum.1 ⊢ Ⅎ _ x A
2 nfsum.2 ⊢ Ⅎ _ x B
3 df-sum ⊢ ∑ k ∈ A B = ι z | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ z ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
4 nfcv ⊢ Ⅎ _ x ℤ
5 nfcv ⊢ Ⅎ _ x ℤ ≥ m
6 1 5 nfss ⊢ Ⅎ x A ⊆ ℤ ≥ m
7 nfcv ⊢ Ⅎ _ x m
8 nfcv ⊢ Ⅎ _ x +
9 1 nfcri ⊢ Ⅎ x n ∈ A
10 nfcv ⊢ Ⅎ _ x n
11 10 2 nfcsbw ⊢ Ⅎ _ x ⦋ n / k⦌ B
12 nfcv ⊢ Ⅎ _ x 0
13 9 11 12 nfif ⊢ Ⅎ _ x if n ∈ A ⦋ n / k⦌ B 0
14 4 13 nfmpt ⊢ Ⅎ _ x n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0
15 7 8 14 nfseq ⊢ Ⅎ _ x seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0
16 nfcv ⊢ Ⅎ _ x ⇝
17 nfcv ⊢ Ⅎ _ x z
18 15 16 17 nfbr ⊢ Ⅎ x seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ z
19 6 18 nfan ⊢ Ⅎ x A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ z
20 4 19 nfrex ⊢ Ⅎ x ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ z
21 nfcv ⊢ Ⅎ _ x ℕ
22 nfcv ⊢ Ⅎ _ x f
23 nfcv ⊢ Ⅎ _ x 1 … m
24 22 23 1 nff1o ⊢ Ⅎ x f : 1 … m ⟶ 1-1 onto A
25 nfcv ⊢ Ⅎ _ x 1
26 nfcv ⊢ Ⅎ _ x f ⁡ n
27 26 2 nfcsbw ⊢ Ⅎ _ x ⦋ f ⁡ n / k⦌ B
28 21 27 nfmpt ⊢ Ⅎ _ x n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B
29 25 8 28 nfseq ⊢ Ⅎ _ x seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B
30 29 7 nffv ⊢ Ⅎ _ x seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
31 30 nfeq2 ⊢ Ⅎ x z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
32 24 31 nfan ⊢ Ⅎ x f : 1 … m ⟶ 1-1 onto A ∧ z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
33 32 nfex ⊢ Ⅎ x ∃ f f : 1 … m ⟶ 1-1 onto A ∧ z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
34 21 33 nfrex ⊢ Ⅎ x ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
35 20 34 nfor ⊢ Ⅎ x ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ z ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
36 35 nfiotaw ⊢ Ⅎ _ x ι z | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ z ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ z = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
37 3 36 nfcxfr ⊢ Ⅎ _ x ∑ k ∈ A B