Theorem smupf

Description: The sequence of partial sums of the sequence multiplication. (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	smupf	$$⊢\phi \to P:{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0$$

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		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5		iftrue	$$⊢n=0\to if\left(n=0,\varnothing ,n-1\right)=\varnothing$$
6		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)$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8	5 6 7	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$$
9	4 8	mp1i	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)=\varnothing$$
10		0elpw	$$⊢\varnothing \in 𝒫{\mathbb{N}}_0$$
11	9 10	eqeltrdi	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(0\right)\in 𝒫{\mathbb{N}}_0$$
12		df-ov	$$⊢x\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)y=\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(⟨x,y⟩\right)$$
13		elpwi	$$⊢p\in 𝒫{\mathbb{N}}_0\to p\subseteq {\mathbb{N}}_0$$
14	13	adantr	$$⊢\left(p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to p\subseteq {\mathbb{N}}_0$$
15		ssrab2	$$⊢\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\subseteq {\mathbb{N}}_0$$
16		sadcl	$$⊢\left(p\subseteq {\mathbb{N}}_0\wedge \left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\subseteq {\mathbb{N}}_0\right)\to p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\subseteq {\mathbb{N}}_0$$
17	14 15 16	sylancl	$$⊢\left(p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\subseteq {\mathbb{N}}_0$$
18		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
19	18	elpw2	$$⊢p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\in 𝒫{\mathbb{N}}_0\leftrightarrow p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\subseteq {\mathbb{N}}_0$$
20	17 19	sylibr	$$⊢\left(p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\in 𝒫{\mathbb{N}}_0$$
21	20	rgen2	$$⊢\forall p\in 𝒫{\mathbb{N}}_0\forall 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\}\in 𝒫{\mathbb{N}}_0$$
22		eqid	$$⊢\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(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)$$
23	22	fmpo	$$⊢\forall p\in 𝒫{\mathbb{N}}_0\forall 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\}\in 𝒫{\mathbb{N}}_0\leftrightarrow \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):𝒫{\mathbb{N}}_0\times {\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0$$
24	21 23	mpbi	$$⊢\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):𝒫{\mathbb{N}}_0\times {\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0$$
25	24 10	f0cli	$$⊢\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(⟨x,y⟩\right)\in 𝒫{\mathbb{N}}_0$$
26	12 25	eqeltri	$$⊢x\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)y\in 𝒫{\mathbb{N}}_0$$
27	26	a1i	$$⊢\left(\phi \wedge \left(x\in 𝒫{\mathbb{N}}_0\wedge y\in \mathrm{V}\right)\right)\to x\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)y\in 𝒫{\mathbb{N}}_0$$
28		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
29		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
30		fvexd	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge \left(0+1\right)}\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\left(x\right)\in \mathrm{V}$$
31	11 27 28 29 30	seqf2	$$⊢\phi \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):{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0$$
32	3	feq1i	$$⊢P:{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0\leftrightarrow 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):{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0$$
33	31 32	sylibr	$$⊢\phi \to P:{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0$$