Theorem smup0

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

	Ref	Expression
Hypotheses	smuval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	smuval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	smuval.p	$$⊢P=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
Assertion	smup0	$$⊢\phi \to P\left(0\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		smuval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		smuval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		smuval.p	$$⊢P=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4		0z	$$⊢0\in \mathbb{Z}$$
5	3	fveq1i	$$⊢P\left(0\right)=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(0\right)$$
6		seq1	$$⊢0\in \mathbb{Z}\to seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)$$
7	5 6	eqtrid	$$⊢0\in \mathbb{Z}\to P\left(0\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)$$
8	4 7	mp1i	$$⊢\phi \to P\left(0\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)$$
9		0nn0	$$⊢0\in {\mathbb{N}}_0$$
10		iftrue	$$⊢n=0\to if\left(n=0,\varnothing ,n-1\right)=\varnothing$$
11		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)$$
12		0ex	$$⊢\varnothing \in \mathrm{V}$$
13	10 11 12	fvmpt	$$⊢0\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)=\varnothing$$
14	9 13	mp1i	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)=\varnothing$$
15	8 14	eqtrd	$$⊢\phi \to P\left(0\right)=\varnothing$$