Theorem divalglem4

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Hypotheses	divalglem0.1	$$⊢N\in \mathbb{Z}$$
	divalglem0.2	$$⊢D\in \mathbb{Z}$$
	divalglem1.3	$$⊢D\ne 0$$
	divalglem2.4	$$⊢S=\left\{r\in {\mathbb{N}}_0|D\parallel \left(N-r\right)\right\}$$
Assertion	divalglem4	$$⊢S=\left\{r\in {\mathbb{N}}_0|\exists q\in \mathbb{Z}N=qD+r\right\}$$

Proof

Step	Hyp	Ref	Expression
1		divalglem0.1	$$⊢N\in \mathbb{Z}$$
2		divalglem0.2	$$⊢D\in \mathbb{Z}$$
3		divalglem1.3	$$⊢D\ne 0$$
4		divalglem2.4	$$⊢S=\left\{r\in {\mathbb{N}}_0|D\parallel \left(N-r\right)\right\}$$
5		nn0z	$$⊢z\in {\mathbb{N}}_0\to z\in \mathbb{Z}$$
6		zsubcl	$$⊢\left(N\in \mathbb{Z}\wedge z\in \mathbb{Z}\right)\to N-z\in \mathbb{Z}$$
7	1 5 6	sylancr	$$⊢z\in {\mathbb{N}}_0\to N-z\in \mathbb{Z}$$
8		divides	$$⊢\left(D\in \mathbb{Z}\wedge N-z\in \mathbb{Z}\right)\to \left(D\parallel \left(N-z\right)\leftrightarrow \exists q\in \mathbb{Z}qD=N-z\right)$$
9	2 7 8	sylancr	$$⊢z\in {\mathbb{N}}_0\to \left(D\parallel \left(N-z\right)\leftrightarrow \exists q\in \mathbb{Z}qD=N-z\right)$$
10		nn0cn	$$⊢z\in {\mathbb{N}}_0\to z\in ℂ$$
11		zmulcl	$$⊢\left(q\in \mathbb{Z}\wedge D\in \mathbb{Z}\right)\to qD\in \mathbb{Z}$$
12	2 11	mpan2	$$⊢q\in \mathbb{Z}\to qD\in \mathbb{Z}$$
13	12	zcnd	$$⊢q\in \mathbb{Z}\to qD\in ℂ$$
14		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
15	1 14	ax-mp	$$⊢N\in ℂ$$
16		subadd	$$⊢\left(N\in ℂ\wedge z\in ℂ\wedge qD\in ℂ\right)\to \left(N-z=qD\leftrightarrow z+qD=N\right)$$
17	15 16	mp3an1	$$⊢\left(z\in ℂ\wedge qD\in ℂ\right)\to \left(N-z=qD\leftrightarrow z+qD=N\right)$$
18		addcom	$$⊢\left(z\in ℂ\wedge qD\in ℂ\right)\to z+qD=qD+z$$
19	18	eqeq1d	$$⊢\left(z\in ℂ\wedge qD\in ℂ\right)\to \left(z+qD=N\leftrightarrow qD+z=N\right)$$
20	17 19	bitrd	$$⊢\left(z\in ℂ\wedge qD\in ℂ\right)\to \left(N-z=qD\leftrightarrow qD+z=N\right)$$
21	10 13 20	syl2an	$$⊢\left(z\in {\mathbb{N}}_0\wedge q\in \mathbb{Z}\right)\to \left(N-z=qD\leftrightarrow qD+z=N\right)$$
22		eqcom	$$⊢N-z=qD\leftrightarrow qD=N-z$$
23		eqcom	$$⊢qD+z=N\leftrightarrow N=qD+z$$
24	21 22 23	3bitr3g	$$⊢\left(z\in {\mathbb{N}}_0\wedge q\in \mathbb{Z}\right)\to \left(qD=N-z\leftrightarrow N=qD+z\right)$$
25	24	rexbidva	$$⊢z\in {\mathbb{N}}_0\to \left(\exists q\in \mathbb{Z}qD=N-z\leftrightarrow \exists q\in \mathbb{Z}N=qD+z\right)$$
26	9 25	bitrd	$$⊢z\in {\mathbb{N}}_0\to \left(D\parallel \left(N-z\right)\leftrightarrow \exists q\in \mathbb{Z}N=qD+z\right)$$
27	26	pm5.32i	$$⊢\left(z\in {\mathbb{N}}_0\wedge D\parallel \left(N-z\right)\right)\leftrightarrow \left(z\in {\mathbb{N}}_0\wedge \exists q\in \mathbb{Z}N=qD+z\right)$$
28		oveq2	$$⊢r=z\to N-r=N-z$$
29	28	breq2d	$$⊢r=z\to \left(D\parallel \left(N-r\right)\leftrightarrow D\parallel \left(N-z\right)\right)$$
30	29 4	elrab2	$$⊢z\in S\leftrightarrow \left(z\in {\mathbb{N}}_0\wedge D\parallel \left(N-z\right)\right)$$
31		oveq2	$$⊢r=z\to qD+r=qD+z$$
32	31	eqeq2d	$$⊢r=z\to \left(N=qD+r\leftrightarrow N=qD+z\right)$$
33	32	rexbidv	$$⊢r=z\to \left(\exists q\in \mathbb{Z}N=qD+r\leftrightarrow \exists q\in \mathbb{Z}N=qD+z\right)$$
34	33	elrab	$$⊢z\in \left\{r\in {\mathbb{N}}_0|\exists q\in \mathbb{Z}N=qD+r\right\}\leftrightarrow \left(z\in {\mathbb{N}}_0\wedge \exists q\in \mathbb{Z}N=qD+z\right)$$
35	27 30 34	3bitr4i	$$⊢z\in S\leftrightarrow z\in \left\{r\in {\mathbb{N}}_0|\exists q\in \mathbb{Z}N=qD+r\right\}$$
36	35	eqriv	$$⊢S=\left\{r\in {\mathbb{N}}_0|\exists q\in \mathbb{Z}N=qD+r\right\}$$