# Metamath Proof Explorer

## Theorem divalglem1

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

Ref Expression
Hypotheses divalglem0.1 ${⊢}{N}\in ℤ$
divalglem0.2 ${⊢}{D}\in ℤ$
divalglem1.3 ${⊢}{D}\ne 0$
Assertion divalglem1 ${⊢}0\le {N}+\left|{N}{D}\right|$

### Proof

Step Hyp Ref Expression
1 divalglem0.1 ${⊢}{N}\in ℤ$
2 divalglem0.2 ${⊢}{D}\in ℤ$
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 ℤ\wedge {D}\ne 0\right)\to \left|{D}\right|\in ℕ$
8 2 3 7 mp2an ${⊢}\left|{D}\right|\in ℕ$
9 nnge1 ${⊢}\left|{D}\right|\in ℕ\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↔0\le -{N}\right)$
12 4 11 ax-mp ${⊢}{N}\le 0↔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 -{N}\left|{D}\right|$
18 13 16 17 mpanl12 ${⊢}\left(0\le -{N}\wedge 1\le \left|{D}\right|\right)\to -{N}\le -{N}\left|{D}\right|$
19 12 18 sylanb ${⊢}\left({N}\le 0\wedge 1\le \left|{D}\right|\right)\to -{N}\le -{N}\left|{D}\right|$
20 10 19 mpan2 ${⊢}{N}\le 0\to -{N}\le -{N}\left|{D}\right|$
21 4 recni ${⊢}{N}\in ℂ$
22 21 15 absmuli ${⊢}\left|{N}{D}\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|=-{N}\left|{D}\right|$
25 22 24 syl5eq ${⊢}{N}\le 0\to \left|{N}{D}\right|=-{N}\left|{D}\right|$
26 20 25 breqtrrd ${⊢}{N}\le 0\to -{N}\le \left|{N}{D}\right|$
27 le0neg2 ${⊢}{N}\in ℝ\to \left(0\le {N}↔-{N}\le 0\right)$
28 4 27 ax-mp ${⊢}0\le {N}↔-{N}\le 0$
29 4 14 remulcli ${⊢}{N}{D}\in ℝ$
30 29 recni ${⊢}{N}{D}\in ℂ$
31 30 absge0i ${⊢}0\le \left|{N}{D}\right|$
32 30 abscli ${⊢}\left|{N}{D}\right|\in ℝ$
33 13 5 32 letri ${⊢}\left(-{N}\le 0\wedge 0\le \left|{N}{D}\right|\right)\to -{N}\le \left|{N}{D}\right|$
34 31 33 mpan2 ${⊢}-{N}\le 0\to -{N}\le \left|{N}{D}\right|$
35 28 34 sylbi ${⊢}0\le {N}\to -{N}\le \left|{N}{D}\right|$
36 26 35 jaoi ${⊢}\left({N}\le 0\vee 0\le {N}\right)\to -{N}\le \left|{N}{D}\right|$
37 6 36 ax-mp ${⊢}-{N}\le \left|{N}{D}\right|$
38 df-neg ${⊢}-{N}=0-{N}$
39 38 breq1i ${⊢}-{N}\le \left|{N}{D}\right|↔0-{N}\le \left|{N}{D}\right|$
40 5 4 32 lesubadd2i ${⊢}0-{N}\le \left|{N}{D}\right|↔0\le {N}+\left|{N}{D}\right|$
41 39 40 bitri ${⊢}-{N}\le \left|{N}{D}\right|↔0\le {N}+\left|{N}{D}\right|$
42 37 41 mpbi ${⊢}0\le {N}+\left|{N}{D}\right|$