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	$⊢ \underline{Ⅎ} k A$
	Assertion	nfsum1	$⊢ \underline{Ⅎ} k \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		nfsum1.1	$⊢ \underline{Ⅎ} k A$
2		df-sum	$⊢ \sum_{k \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
3		nfcv	$⊢ \underline{Ⅎ} k ℤ$
4		nfcv	$⊢ \underline{Ⅎ} k ℤ_{\geq m}$
5	1 4	nfss	$⊢ Ⅎ k A \subseteq ℤ_{\geq m}$
6		nfcv	$⊢ \underline{Ⅎ} k m$
7		nfcv	$⊢ \underline{Ⅎ} k +$
8	1	nfcri	$⊢ Ⅎ k n \in A$
9		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ B$
10		nfcv	$⊢ \underline{Ⅎ} k 0$
11	8 9 10	nfif	$⊢ \underline{Ⅎ} k if (n \in A, ⦋ n / k ⦌ B, 0)$
12	3 11	nfmpt	$⊢ \underline{Ⅎ} k (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))$
13	6 7 12	nfseq	$⊢ \underline{Ⅎ} k seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)))$
14		nfcv	$⊢ \underline{Ⅎ} k ⇝$
15		nfcv	$⊢ \underline{Ⅎ} k x$
16	13 14 15	nfbr	$⊢ Ⅎ k seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x$
17	5 16	nfan	$⊢ Ⅎ k (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
18	3 17	nfrexw	$⊢ Ⅎ k \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
19		nfcv	$⊢ \underline{Ⅎ} k ℕ$
20		nfcv	$⊢ \underline{Ⅎ} k f$
21		nfcv	$⊢ \underline{Ⅎ} k (1 \dots m)$
22	20 21 1	nff1o	$⊢ Ⅎ k f : (1 \dots m) \underset{1-1 onto}{⟶} A$
23		nfcv	$⊢ \underline{Ⅎ} k 1$
24		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (n) / k ⦌ B$
25	19 24	nfmpt	$⊢ \underline{Ⅎ} k (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
26	23 7 25	nfseq	$⊢ \underline{Ⅎ} k seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B))$
27	26 6	nffv	$⊢ \underline{Ⅎ} k seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
28	27	nfeq2	$⊢ Ⅎ k x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
29	22 28	nfan	$⊢ Ⅎ k (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
30	29	nfex	$⊢ Ⅎ k \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
31	19 30	nfrexw	$⊢ Ⅎ k \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
32	18 31	nfor	$⊢ Ⅎ k (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
33	32	nfiotaw	$⊢ \underline{Ⅎ} k (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
34	2 33	nfcxfr	$⊢ \underline{Ⅎ} k \sum_{k \in A} B$

Metamath Proof Explorer

Theorem nfsum1

Proof