Theorem smu01lem

Description: Lemma for smu01 and smu02 . (Contributed by Mario Carneiro, 19-Sep-2016)

	Ref	Expression
Hypotheses	smu01lem.1	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	smu01lem.2	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	smu01lem.3	$$⊢\left(\phi \wedge \left(k\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\right)\to \neg \left(k\in A\wedge n-k\in B\right)$$
Assertion	smu01lem	$$⊢\phi \to A\mathrm{smul}B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		smu01lem.1	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		smu01lem.2	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		smu01lem.3	$$⊢\left(\phi \wedge \left(k\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\right)\to \neg \left(k\in A\wedge n-k\in B\right)$$
4		smucl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{smul}B\subseteq {\mathbb{N}}_0$$
5	1 2 4	syl2anc	$$⊢\phi \to A\mathrm{smul}B\subseteq {\mathbb{N}}_0$$
6	5	sseld	$$⊢\phi \to \left(k\in \left(A\mathrm{smul}B\right)\to k\in {\mathbb{N}}_0\right)$$
7		noel	$$⊢\neg k\in \varnothing$$
8		peano2nn0	$$⊢k\in {\mathbb{N}}_0\to k+1\in {\mathbb{N}}_0$$
9		fveqeq2	$$⊢x=0\to \left(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(x\right)=\varnothing \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)\left(0\right)=\varnothing \right)$$
10	9	imbi2d	$$⊢x=0\to \left(\left(\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)\left(x\right)=\varnothing \right)\leftrightarrow \left(\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)\left(0\right)=\varnothing \right)\right)$$
11		fveqeq2	$$⊢x=k\to \left(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(x\right)=\varnothing \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)\left(k\right)=\varnothing \right)$$
12	11	imbi2d	$$⊢x=k\to \left(\left(\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)\left(x\right)=\varnothing \right)\leftrightarrow \left(\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)\left(k\right)=\varnothing \right)\right)$$
13		fveqeq2	$$⊢x=k+1\to \left(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(x\right)=\varnothing \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)\left(k+1\right)=\varnothing \right)$$
14	13	imbi2d	$$⊢x=k+1\to \left(\left(\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)\left(x\right)=\varnothing \right)\leftrightarrow \left(\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)\left(k+1\right)=\varnothing \right)\right)$$
15		eqid	$$⊢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)=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)$$
16	1 2 15	smup0	$$⊢\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)\left(0\right)=\varnothing$$
17		oveq1	$$⊢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(k\right)=\varnothing \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(k\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}=\varnothing \mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}$$
18	1	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\subseteq {\mathbb{N}}_0$$
19	2	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to B\subseteq {\mathbb{N}}_0$$
20		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
21	18 19 15 20	smupp1	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\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(k+1\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(k\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}$$
22	3	anassrs	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to \neg \left(k\in A\wedge n-k\in B\right)$$
23	22	ralrimiva	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \forall n\in {\mathbb{N}}_0\neg \left(k\in A\wedge n-k\in B\right)$$
24		rabeq0	$$⊢\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}=\varnothing \leftrightarrow \forall n\in {\mathbb{N}}_0\neg \left(k\in A\wedge n-k\in B\right)$$
25	23 24	sylibr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}=\varnothing$$
26	25	oveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \varnothing \mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}=\varnothing \mathrm{sadd}\varnothing$$
27		0ss	$$⊢\varnothing \subseteq {\mathbb{N}}_0$$
28		sadid1	$$⊢\varnothing \subseteq {\mathbb{N}}_0\to \varnothing \mathrm{sadd}\varnothing =\varnothing$$
29	27 28	mp1i	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \varnothing \mathrm{sadd}\varnothing =\varnothing$$
30	26 29	eqtr2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \varnothing =\varnothing \mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}$$
31	21 30	eqeq12d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(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(k+1\right)=\varnothing \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)\left(k\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}=\varnothing \mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(k\in A\wedge n-k\in B\right)\right\}\right)$$
32	17 31	syl5ibr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(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(k\right)=\varnothing \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(k+1\right)=\varnothing \right)$$
33	32	expcom	$$⊢k\in {\mathbb{N}}_0\to \left(\phi \to \left(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(k\right)=\varnothing \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(k+1\right)=\varnothing \right)\right)$$
34	33	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(\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)\left(k\right)=\varnothing \right)\to \left(\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)\left(k+1\right)=\varnothing \right)\right)$$
35	10 12 14 14 16 34	nn0ind	$$⊢k+1\in {\mathbb{N}}_0\to \left(\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)\left(k+1\right)=\varnothing \right)$$
36	8 35	syl	$$⊢k\in {\mathbb{N}}_0\to \left(\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)\left(k+1\right)=\varnothing \right)$$
37	36	impcom	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\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(k+1\right)=\varnothing$$
38	37	eleq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(k\in 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(k+1\right)\leftrightarrow k\in \varnothing \right)$$
39	7 38	mtbiri	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \neg k\in 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(k+1\right)$$
40	18 19 15 20	smuval	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(k\in \left(A\mathrm{smul}B\right)\leftrightarrow k\in 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(k+1\right)\right)$$
41	39 40	mtbird	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \neg k\in \left(A\mathrm{smul}B\right)$$
42	41	ex	$$⊢\phi \to \left(k\in {\mathbb{N}}_0\to \neg k\in \left(A\mathrm{smul}B\right)\right)$$
43	6 42	syld	$$⊢\phi \to \left(k\in \left(A\mathrm{smul}B\right)\to \neg k\in \left(A\mathrm{smul}B\right)\right)$$
44	43	pm2.01d	$$⊢\phi \to \neg k\in \left(A\mathrm{smul}B\right)$$
45	44	eq0rdv	$$⊢\phi \to A\mathrm{smul}B=\varnothing$$