Theorem divalglem5

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011) (Revised by AV, 2-Oct-2020)

	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\}$$
	divalglem5.5	$$⊢R=sup\left(S,ℝ,<\right)$$
Assertion	divalglem5	$$⊢\left(0\le R\wedge R<\left|D\right|\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		divalglem5.5	$$⊢R=sup\left(S,ℝ,<\right)$$
6	1 2 3 4	divalglem2	$$⊢sup\left(S,ℝ,<\right)\in S$$
7	5 6	eqeltri	$$⊢R\in S$$
8		oveq2	$$⊢x=R\to N-x=N-R$$
9	8	breq2d	$$⊢x=R\to \left(D\parallel \left(N-x\right)\leftrightarrow D\parallel \left(N-R\right)\right)$$
10		oveq2	$$⊢r=x\to N-r=N-x$$
11	10	breq2d	$$⊢r=x\to \left(D\parallel \left(N-r\right)\leftrightarrow D\parallel \left(N-x\right)\right)$$
12	11	cbvrabv	$$⊢\left\{r\in {\mathbb{N}}_0|D\parallel \left(N-r\right)\right\}=\left\{x\in {\mathbb{N}}_0|D\parallel \left(N-x\right)\right\}$$
13	4 12	eqtri	$$⊢S=\left\{x\in {\mathbb{N}}_0|D\parallel \left(N-x\right)\right\}$$
14	9 13	elrab2	$$⊢R\in S\leftrightarrow \left(R\in {\mathbb{N}}_0\wedge D\parallel \left(N-R\right)\right)$$
15	7 14	mpbi	$$⊢\left(R\in {\mathbb{N}}_0\wedge D\parallel \left(N-R\right)\right)$$
16	15	simpli	$$⊢R\in {\mathbb{N}}_0$$
17	16	nn0ge0i	$$⊢0\le R$$
18		nnabscl	$$⊢\left(D\in \mathbb{Z}\wedge D\ne 0\right)\to \left|D\right|\in \mathbb{N}$$
19	2 3 18	mp2an	$$⊢\left|D\right|\in \mathbb{N}$$
20	19	nngt0i	$$⊢0<\left|D\right|$$
21		0re	$$⊢0\in ℝ$$
22		zcn	$$⊢D\in \mathbb{Z}\to D\in ℂ$$
23	2 22	ax-mp	$$⊢D\in ℂ$$
24	23	abscli	$$⊢\left|D\right|\in ℝ$$
25	21 24	ltnlei	$$⊢0<\left|D\right|\leftrightarrow \neg \left|D\right|\le 0$$
26	20 25	mpbi	$$⊢\neg \left|D\right|\le 0$$
27	4	ssrab3	$$⊢S\subseteq {\mathbb{N}}_0$$
28		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
29	27 28	sseqtri	$$⊢S\subseteq {\mathbb{Z}}_{\ge 0}$$
30		nn0abscl	$$⊢D\in \mathbb{Z}\to \left|D\right|\in {\mathbb{N}}_0$$
31	2 30	ax-mp	$$⊢\left|D\right|\in {\mathbb{N}}_0$$
32		nn0sub2	$$⊢\left(\left|D\right|\in {\mathbb{N}}_0\wedge R\in {\mathbb{N}}_0\wedge \left|D\right|\le R\right)\to R-\left|D\right|\in {\mathbb{N}}_0$$
33	31 16 32	mp3an12	$$⊢\left|D\right|\le R\to R-\left|D\right|\in {\mathbb{N}}_0$$
34	15	a1i	$$⊢\left|D\right|\le R\to \left(R\in {\mathbb{N}}_0\wedge D\parallel \left(N-R\right)\right)$$
35		nn0z	$$⊢R\in {\mathbb{N}}_0\to R\in \mathbb{Z}$$
36		1z	$$⊢1\in \mathbb{Z}$$
37	1 2	divalglem0	$$⊢\left(R\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left(D\parallel \left(N-R\right)\to D\parallel \left(N-\left(R-1\left|D\right|\right)\right)\right)$$
38	36 37	mpan2	$$⊢R\in \mathbb{Z}\to \left(D\parallel \left(N-R\right)\to D\parallel \left(N-\left(R-1\left|D\right|\right)\right)\right)$$
39	24	recni	$$⊢\left|D\right|\in ℂ$$
40	39	mullidi	$$⊢1\left|D\right|=\left|D\right|$$
41	40	oveq2i	$$⊢R-1\left|D\right|=R-\left|D\right|$$
42	41	oveq2i	$$⊢N-\left(R-1\left|D\right|\right)=N-\left(R-\left|D\right|\right)$$
43	42	breq2i	$$⊢D\parallel \left(N-\left(R-1\left|D\right|\right)\right)\leftrightarrow D\parallel \left(N-\left(R-\left|D\right|\right)\right)$$
44	38 43	imbitrdi	$$⊢R\in \mathbb{Z}\to \left(D\parallel \left(N-R\right)\to D\parallel \left(N-\left(R-\left|D\right|\right)\right)\right)$$
45	35 44	syl	$$⊢R\in {\mathbb{N}}_0\to \left(D\parallel \left(N-R\right)\to D\parallel \left(N-\left(R-\left|D\right|\right)\right)\right)$$
46	45	imp	$$⊢\left(R\in {\mathbb{N}}_0\wedge D\parallel \left(N-R\right)\right)\to D\parallel \left(N-\left(R-\left|D\right|\right)\right)$$
47	34 46	syl	$$⊢\left|D\right|\le R\to D\parallel \left(N-\left(R-\left|D\right|\right)\right)$$
48		oveq2	$$⊢x=R-\left|D\right|\to N-x=N-\left(R-\left|D\right|\right)$$
49	48	breq2d	$$⊢x=R-\left|D\right|\to \left(D\parallel \left(N-x\right)\leftrightarrow D\parallel \left(N-\left(R-\left|D\right|\right)\right)\right)$$
50	49 13	elrab2	$$⊢R-\left|D\right|\in S\leftrightarrow \left(R-\left|D\right|\in {\mathbb{N}}_0\wedge D\parallel \left(N-\left(R-\left|D\right|\right)\right)\right)$$
51	33 47 50	sylanbrc	$$⊢\left|D\right|\le R\to R-\left|D\right|\in S$$
52		infssuzle	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge 0}\wedge R-\left|D\right|\in S\right)\to sup\left(S,ℝ,<\right)\le R-\left|D\right|$$
53	29 51 52	sylancr	$$⊢\left|D\right|\le R\to sup\left(S,ℝ,<\right)\le R-\left|D\right|$$
54	5 53	eqbrtrid	$$⊢\left|D\right|\le R\to R\le R-\left|D\right|$$
55	34	simpld	$$⊢\left|D\right|\le R\to R\in {\mathbb{N}}_0$$
56	55	nn0red	$$⊢\left|D\right|\le R\to R\in ℝ$$
57		lesub	$$⊢\left(R\in ℝ\wedge R\in ℝ\wedge \left|D\right|\in ℝ\right)\to \left(R\le R-\left|D\right|\leftrightarrow \left|D\right|\le R-R\right)$$
58	24 57	mp3an3	$$⊢\left(R\in ℝ\wedge R\in ℝ\right)\to \left(R\le R-\left|D\right|\leftrightarrow \left|D\right|\le R-R\right)$$
59	56 56 58	syl2anc	$$⊢\left|D\right|\le R\to \left(R\le R-\left|D\right|\leftrightarrow \left|D\right|\le R-R\right)$$
60	56	recnd	$$⊢\left|D\right|\le R\to R\in ℂ$$
61	60	subidd	$$⊢\left|D\right|\le R\to R-R=0$$
62	61	breq2d	$$⊢\left|D\right|\le R\to \left(\left|D\right|\le R-R\leftrightarrow \left|D\right|\le 0\right)$$
63	59 62	bitrd	$$⊢\left|D\right|\le R\to \left(R\le R-\left|D\right|\leftrightarrow \left|D\right|\le 0\right)$$
64	54 63	mpbid	$$⊢\left|D\right|\le R\to \left|D\right|\le 0$$
65	26 64	mto	$$⊢\neg \left|D\right|\le R$$
66	16	nn0rei	$$⊢R\in ℝ$$
67	66 24	ltnlei	$$⊢R<\left|D\right|\leftrightarrow \neg \left|D\right|\le R$$
68	65 67	mpbir	$$⊢R<\left|D\right|$$
69	17 68	pm3.2i	$$⊢\left(0\le R\wedge R<\left|D\right|\right)$$