Metamath Proof Explorer

Theorem divalglem1

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

Ref Expression
Hypotheses divalglem0.1 ⊢ 𝑁 ∈ ℤ
divalglem0.2 ⊢ 𝐷 ∈ ℤ
divalglem1.3 ⊢ 𝐷 ≠ 0
Assertion divalglem1 0 ≤ ( 𝑁 + ( abs ‘ ( 𝑁 · 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 divalglem0.1 ⊢ 𝑁 ∈ ℤ
2 divalglem0.2 ⊢ 𝐷 ∈ ℤ
3 divalglem1.3 ⊢ 𝐷 ≠ 0
4 1 zrei ⊢ 𝑁 ∈ ℝ
5 0re ⊢ 0 ∈ ℝ
6 4 5 letrii ⊢ ( 𝑁 ≤ 0 ∨ 0 ≤ 𝑁 )
7 nnabscl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ )
8 2 3 7 mp2an ⊢ ( abs ‘ 𝐷 ) ∈ ℕ
9 nnge1 ⊢ ( ( abs ‘ 𝐷 ) ∈ ℕ → 1 ≤ ( abs ‘ 𝐷 ) )
10 8 9 ax-mp ⊢ 1 ≤ ( abs ‘ 𝐷 )
11 le0neg1 ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 ≤ 0 ↔ 0 ≤ - 𝑁 ) )
12 4 11 ax-mp ⊢ ( 𝑁 ≤ 0 ↔ 0 ≤ - 𝑁 )
13 4 renegcli ⊢ - 𝑁 ∈ ℝ
14 2 zrei ⊢ 𝐷 ∈ ℝ
15 14 recni ⊢ 𝐷 ∈ ℂ
16 15 abscli ⊢ ( abs ‘ 𝐷 ) ∈ ℝ
17 lemulge11 ⊢ ( ( ( - 𝑁 ∈ ℝ ∧ ( abs ‘ 𝐷 ) ∈ ℝ ) ∧ ( 0 ≤ - 𝑁 ∧ 1 ≤ ( abs ‘ 𝐷 ) ) ) → - 𝑁 ≤ ( - 𝑁 · ( abs ‘ 𝐷 ) ) )
18 13 16 17 mpanl12 ⊢ ( ( 0 ≤ - 𝑁 ∧ 1 ≤ ( abs ‘ 𝐷 ) ) → - 𝑁 ≤ ( - 𝑁 · ( abs ‘ 𝐷 ) ) )
19 12 18 sylanb ⊢ ( ( 𝑁 ≤ 0 ∧ 1 ≤ ( abs ‘ 𝐷 ) ) → - 𝑁 ≤ ( - 𝑁 · ( abs ‘ 𝐷 ) ) )
20 10 19 mpan2 ⊢ ( 𝑁 ≤ 0 → - 𝑁 ≤ ( - 𝑁 · ( abs ‘ 𝐷 ) ) )
21 4 recni ⊢ 𝑁 ∈ ℂ
22 21 15 absmuli ⊢ ( abs ‘ ( 𝑁 · 𝐷 ) ) = ( ( abs ‘ 𝑁 ) · ( abs ‘ 𝐷 ) )
23 4 absnidi ⊢ ( 𝑁 ≤ 0 → ( abs ‘ 𝑁 ) = - 𝑁 )
24 23 oveq1d ⊢ ( 𝑁 ≤ 0 → ( ( abs ‘ 𝑁 ) · ( abs ‘ 𝐷 ) ) = ( - 𝑁 · ( abs ‘ 𝐷 ) ) )
25 22 24 syl5eq ⊢ ( 𝑁 ≤ 0 → ( abs ‘ ( 𝑁 · 𝐷 ) ) = ( - 𝑁 · ( abs ‘ 𝐷 ) ) )
26 20 25 breqtrrd ⊢ ( 𝑁 ≤ 0 → - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) )
27 le0neg2 ⊢ ( 𝑁 ∈ ℝ → ( 0 ≤ 𝑁 ↔ - 𝑁 ≤ 0 ) )
28 4 27 ax-mp ⊢ ( 0 ≤ 𝑁 ↔ - 𝑁 ≤ 0 )
29 4 14 remulcli ⊢ ( 𝑁 · 𝐷 ) ∈ ℝ
30 29 recni ⊢ ( 𝑁 · 𝐷 ) ∈ ℂ
31 30 absge0i ⊢ 0 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) )
32 30 abscli ⊢ ( abs ‘ ( 𝑁 · 𝐷 ) ) ∈ ℝ
33 13 5 32 letri ⊢ ( ( - 𝑁 ≤ 0 ∧ 0 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) ) → - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) )
34 31 33 mpan2 ⊢ ( - 𝑁 ≤ 0 → - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) )
35 28 34 sylbi ⊢ ( 0 ≤ 𝑁 → - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) )
36 26 35 jaoi ⊢ ( ( 𝑁 ≤ 0 ∨ 0 ≤ 𝑁 ) → - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) )
37 6 36 ax-mp ⊢ - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) )
38 df-neg ⊢ - 𝑁 = ( 0 − 𝑁 )
39 38 breq1i ⊢ ( - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) ↔ ( 0 − 𝑁 ) ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) )
40 5 4 32 lesubadd2i ⊢ ( ( 0 − 𝑁 ) ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) ↔ 0 ≤ ( 𝑁 + ( abs ‘ ( 𝑁 · 𝐷 ) ) ) )
41 39 40 bitri ⊢ ( - 𝑁 ≤ ( abs ‘ ( 𝑁 · 𝐷 ) ) ↔ 0 ≤ ( 𝑁 + ( abs ‘ ( 𝑁 · 𝐷 ) ) ) )
42 37 41 mpbi ⊢ 0 ≤ ( 𝑁 + ( abs ‘ ( 𝑁 · 𝐷 ) ) )