Theorem divalglem1

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$$
Assertion	divalglem1	$$⊢0\le N+\left|ND\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	1	zrei	$$⊢N\in ℝ$$
5		0re	$$⊢0\in ℝ$$
6	4 5	letrii	$$⊢\left(N\le 0\vee 0\le N\right)$$
7		nnabscl	$$⊢\left(D\in \mathbb{Z}\wedge D\ne 0\right)\to \left|D\right|\in \mathbb{N}$$
8	2 3 7	mp2an	$$⊢\left|D\right|\in \mathbb{N}$$
9		nnge1	$$⊢\left|D\right|\in \mathbb{N}\to 1\le \left|D\right|$$
10	8 9	ax-mp	$$⊢1\le \left|D\right|$$
11		le0neg1	$$⊢N\in ℝ\to \left(N\le 0\leftrightarrow 0\le -N\right)$$
12	4 11	ax-mp	$$⊢N\le 0\leftrightarrow 0\le -N$$
13	4	renegcli	$$⊢-N\in ℝ$$
14	2	zrei	$$⊢D\in ℝ$$
15	14	recni	$$⊢D\in ℂ$$
16	15	abscli	$$⊢\left|D\right|\in ℝ$$
17		lemulge11	$$⊢\left(\left(-N\in ℝ\wedge \left|D\right|\in ℝ\right)\wedge \left(0\le -N\wedge 1\le \left|D\right|\right)\right)\to -N\le \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\left|D\right|$$
18	13 16 17	mpanl12	$$⊢\left(0\le -N\wedge 1\le \left|D\right|\right)\to -N\le \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\left|D\right|$$
19	12 18	sylanb	$$⊢\left(N\le 0\wedge 1\le \left|D\right|\right)\to -N\le \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\left|D\right|$$
20	10 19	mpan2	$$⊢N\le 0\to -N\le \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\left|D\right|$$
21	4	recni	$$⊢N\in ℂ$$
22	21 15	absmuli	$$⊢\left|ND\right|=\left|N\right|\left|D\right|$$
23	4	absnidi	$$⊢N\le 0\to \left|N\right|=-N$$
24	23	oveq1d	$$⊢N\le 0\to \left|N\right|\left|D\right|=\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\left|D\right|$$
25	22 24	eqtrid	$$⊢N\le 0\to \left|ND\right|=\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\left|D\right|$$
26	20 25	breqtrrd	$$⊢N\le 0\to -N\le \left|ND\right|$$
27		le0neg2	$$⊢N\in ℝ\to \left(0\le N\leftrightarrow -N\le 0\right)$$
28	4 27	ax-mp	$$⊢0\le N\leftrightarrow -N\le 0$$
29	4 14	remulcli	$$⊢ND\in ℝ$$
30	29	recni	$$⊢ND\in ℂ$$
31	30	absge0i	$$⊢0\le \left|ND\right|$$
32	30	abscli	$$⊢\left|ND\right|\in ℝ$$
33	13 5 32	letri	$$⊢\left(-N\le 0\wedge 0\le \left|ND\right|\right)\to -N\le \left|ND\right|$$
34	31 33	mpan2	$$⊢-N\le 0\to -N\le \left|ND\right|$$
35	28 34	sylbi	$$⊢0\le N\to -N\le \left|ND\right|$$
36	26 35	jaoi	$$⊢\left(N\le 0\vee 0\le N\right)\to -N\le \left|ND\right|$$
37	6 36	ax-mp	$$⊢-N\le \left|ND\right|$$
38		df-neg	$$⊢-N=0-N$$
39	38	breq1i	$$⊢-N\le \left|ND\right|\leftrightarrow 0-N\le \left|ND\right|$$
40	5 4 32	lesubadd2i	$$⊢0-N\le \left|ND\right|\leftrightarrow 0\le N+\left|ND\right|$$
41	39 40	bitri	$$⊢-N\le \left|ND\right|\leftrightarrow 0\le N+\left|ND\right|$$
42	37 41	mpbi	$$⊢0\le N+\left|ND\right|$$