smupp1

Description: The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	smuval.a	$⊢ φ \to A \subseteq ℕ_{0}$
	smuval.b	$⊢ φ \to B \subseteq ℕ_{0}$
	smuval.p	$⊢ P = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
	smuval.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	smupp1	$⊢ φ \to P (N + 1) = P (N) sadd \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$

Proof

Step	Hyp	Ref	Expression
1		smuval.a	$⊢ φ \to A \subseteq ℕ_{0}$
2		smuval.b	$⊢ φ \to B \subseteq ℕ_{0}$
3		smuval.p	$⊢ P = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
4		smuval.n	$⊢ φ \to N \in ℕ_{0}$
5		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
6	4 5	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
7		seqp1	$⊢ N \in ℤ_{\geq 0} \to seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N + 1) = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1)$
8	6 7	syl	$⊢ φ \to seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N + 1) = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1)$
9	3	fveq1i	$⊢ P (N + 1) = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N + 1)$
10	3	fveq1i	$⊢ P (N) = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N)$
11	10	oveq1i	$⊢ P (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1) = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1)$
12	8 9 11	3eqtr4g	$⊢ φ \to P (N + 1) = P (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1)$
13		1nn0	$⊢ 1 \in ℕ_{0}$
14	13	a1i	$⊢ φ \to 1 \in ℕ_{0}$
15	4 14	nn0addcld	$⊢ φ \to N + 1 \in ℕ_{0}$
16		eqeq1	$⊢ n = N + 1 \to (n = 0 \leftrightarrow N + 1 = 0)$
17		oveq1	$⊢ n = N + 1 \to n - 1 = N + 1 - 1$
18	16 17	ifbieq2d	$⊢ n = N + 1 \to if (n = 0, \emptyset, n - 1) = if (N + 1 = 0, \emptyset, N + 1 - 1)$
19		eqid	$⊢ (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) = (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))$
20		0ex	$⊢ \emptyset \in V$
21		ovex	$⊢ N + 1 - 1 \in V$
22	20 21	ifex	$⊢ if (N + 1 = 0, \emptyset, N + 1 - 1) \in V$
23	18 19 22	fvmpt	$⊢ N + 1 \in ℕ_{0} \to (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1) = if (N + 1 = 0, \emptyset, N + 1 - 1)$
24	15 23	syl	$⊢ φ \to (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1) = if (N + 1 = 0, \emptyset, N + 1 - 1)$
25		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
26	4 25	syl	$⊢ φ \to N + 1 \in ℕ$
27	26	nnne0d	$⊢ φ \to N + 1 \neq 0$
28		ifnefalse	$⊢ N + 1 \neq 0 \to if (N + 1 = 0, \emptyset, N + 1 - 1) = N + 1 - 1$
29	27 28	syl	$⊢ φ \to if (N + 1 = 0, \emptyset, N + 1 - 1) = N + 1 - 1$
30	4	nn0cnd	$⊢ φ \to N \in ℂ$
31	14	nn0cnd	$⊢ φ \to 1 \in ℂ$
32	30 31	pncand	$⊢ φ \to N + 1 - 1 = N$
33	24 29 32	3eqtrd	$⊢ φ \to (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1) = N$
34	33	oveq2d	$⊢ φ \to P (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)) (N + 1) = P (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) N$
35	1 2 3	smupf	$⊢ φ \to P : ℕ_{0} ⟶ 𝒫 ℕ_{0}$
36	35 4	ffvelrnd	$⊢ φ \to P (N) \in 𝒫 ℕ_{0}$
37		simpl	$⊢ (x = P (N) \land y = N) \to x = P (N)$
38		simpr	$⊢ (x = P (N) \land y = N) \to y = N$
39	38	eleq1d	$⊢ (x = P (N) \land y = N) \to (y \in A \leftrightarrow N \in A)$
40	38	oveq2d	$⊢ (x = P (N) \land y = N) \to k - y = k - N$
41	40	eleq1d	$⊢ (x = P (N) \land y = N) \to (k - y \in B \leftrightarrow k - N \in B)$
42	39 41	anbi12d	$⊢ (x = P (N) \land y = N) \to ((y \in A \land k - y \in B) \leftrightarrow (N \in A \land k - N \in B))$
43	42	rabbidv	$⊢ (x = P (N) \land y = N) \to \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\} = \{k \in ℕ_{0} \| (N \in A \land k - N \in B)\}$
44		oveq1	$⊢ k = n \to k - N = n - N$
45	44	eleq1d	$⊢ k = n \to (k - N \in B \leftrightarrow n - N \in B)$
46	45	anbi2d	$⊢ k = n \to ((N \in A \land k - N \in B) \leftrightarrow (N \in A \land n - N \in B))$
47	46	cbvrabv	$⊢ \{k \in ℕ_{0} \| (N \in A \land k - N \in B)\} = \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$
48	43 47	eqtrdi	$⊢ (x = P (N) \land y = N) \to \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\} = \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$
49	37 48	oveq12d	$⊢ (x = P (N) \land y = N) \to x sadd \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\} = P (N) sadd \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$
50		oveq1	$⊢ p = x \to p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\} = x sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}$
51		eleq1w	$⊢ m = y \to (m \in A \leftrightarrow y \in A)$
52		oveq2	$⊢ m = y \to n - m = n - y$
53	52	eleq1d	$⊢ m = y \to (n - m \in B \leftrightarrow n - y \in B)$
54	51 53	anbi12d	$⊢ m = y \to ((m \in A \land n - m \in B) \leftrightarrow (y \in A \land n - y \in B))$
55	54	rabbidv	$⊢ m = y \to \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\} = \{n \in ℕ_{0} \| (y \in A \land n - y \in B)\}$
56		oveq1	$⊢ k = n \to k - y = n - y$
57	56	eleq1d	$⊢ k = n \to (k - y \in B \leftrightarrow n - y \in B)$
58	57	anbi2d	$⊢ k = n \to ((y \in A \land k - y \in B) \leftrightarrow (y \in A \land n - y \in B))$
59	58	cbvrabv	$⊢ \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\} = \{n \in ℕ_{0} \| (y \in A \land n - y \in B)\}$
60	55 59	eqtr4di	$⊢ m = y \to \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\} = \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\}$
61	60	oveq2d	$⊢ m = y \to x sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\} = x sadd \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\}$
62	50 61	cbvmpov	$⊢ (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) = (x \in 𝒫 ℕ_{0}, y \in ℕ_{0} ⟼ x sadd \{k \in ℕ_{0} \| (y \in A \land k - y \in B)\})$
63		ovex	$⊢ P (N) sadd \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\} \in V$
64	49 62 63	ovmpoa	$⊢ (P (N) \in 𝒫 ℕ_{0} \land N \in ℕ_{0}) \to P (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) N = P (N) sadd \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$
65	36 4 64	syl2anc	$⊢ φ \to P (N) (p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}) N = P (N) sadd \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$
66	12 34 65	3eqtrd	$⊢ φ \to P (N + 1) = P (N) sadd \{n \in ℕ_{0} \| (N \in A \land n - N \in B)\}$

Metamath Proof Explorer

Theorem smupp1

Proof