Metamath Proof Explorer

Theorem divalglem2

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

Ref Expression
Hypotheses divalglem0.1 ⊢ N ∈ ℤ
divalglem0.2 ⊢ D ∈ ℤ
divalglem1.3 ⊢ D ≠ 0
divalglem2.4 ⊢ S = r ∈ ℕ 0 | D ∥ N − r
Assertion divalglem2 ⊢ sup S ℝ < ∈ S

Proof

Step Hyp Ref Expression
1 divalglem0.1 ⊢ N ∈ ℤ
2 divalglem0.2 ⊢ D ∈ ℤ
3 divalglem1.3 ⊢ D ≠ 0
4 divalglem2.4 ⊢ S = r ∈ ℕ 0 | D ∥ N − r
5 4 ssrab3 ⊢ S ⊆ ℕ 0
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 5 6 sseqtri ⊢ S ⊆ ℤ ≥ 0
8 zmulcl ⊢ N ∈ ℤ ∧ D ∈ ℤ → N ⁢ D ∈ ℤ
9 1 2 8 mp2an ⊢ N ⁢ D ∈ ℤ
10 nn0abscl ⊢ N ⁢ D ∈ ℤ → N ⁢ D ∈ ℕ 0
11 9 10 ax-mp ⊢ N ⁢ D ∈ ℕ 0
12 11 nn0zi ⊢ N ⁢ D ∈ ℤ
13 zaddcl ⊢ N ∈ ℤ ∧ N ⁢ D ∈ ℤ → N + N ⁢ D ∈ ℤ
14 1 12 13 mp2an ⊢ N + N ⁢ D ∈ ℤ
15 1 2 3 divalglem1 ⊢ 0 ≤ N + N ⁢ D
16 elnn0z ⊢ N + N ⁢ D ∈ ℕ 0 ↔ N + N ⁢ D ∈ ℤ ∧ 0 ≤ N + N ⁢ D
17 14 15 16 mpbir2an ⊢ N + N ⁢ D ∈ ℕ 0
18 iddvds ⊢ D ∈ ℤ → D ∥ D
19 dvdsabsb ⊢ D ∈ ℤ ∧ D ∈ ℤ → D ∥ D ↔ D ∥ D
20 19 anidms ⊢ D ∈ ℤ → D ∥ D ↔ D ∥ D
21 18 20 mpbid ⊢ D ∈ ℤ → D ∥ D
22 2 21 ax-mp ⊢ D ∥ D
23 nn0abscl ⊢ N ∈ ℤ → N ∈ ℕ 0
24 1 23 ax-mp ⊢ N ∈ ℕ 0
25 24 nn0negzi ⊢ − N ∈ ℤ
26 nn0abscl ⊢ D ∈ ℤ → D ∈ ℕ 0
27 2 26 ax-mp ⊢ D ∈ ℕ 0
28 27 nn0zi ⊢ D ∈ ℤ
29 dvdsmultr2 ⊢ D ∈ ℤ ∧ − N ∈ ℤ ∧ D ∈ ℤ → D ∥ D → D ∥ − N ⁢ D
30 2 25 28 29 mp3an ⊢ D ∥ D → D ∥ − N ⁢ D
31 22 30 ax-mp ⊢ D ∥ − N ⁢ D
32 zcn ⊢ N ∈ ℤ → N ∈ ℂ
33 1 32 ax-mp ⊢ N ∈ ℂ
34 zcn ⊢ D ∈ ℤ → D ∈ ℂ
35 2 34 ax-mp ⊢ D ∈ ℂ
36 33 35 absmuli ⊢ N ⁢ D = N ⁢ D
37 36 negeqi ⊢ − N ⁢ D = − N ⁢ D
38 df-neg ⊢ − N ⁢ D = 0 − N ⁢ D
39 33 subidi ⊢ N − N = 0
40 39 oveq1i ⊢ N - N - N ⁢ D = 0 − N ⁢ D
41 11 nn0cni ⊢ N ⁢ D ∈ ℂ
42 subsub4 ⊢ N ∈ ℂ ∧ N ∈ ℂ ∧ N ⁢ D ∈ ℂ → N - N - N ⁢ D = N − N + N ⁢ D
43 33 33 41 42 mp3an ⊢ N - N - N ⁢ D = N − N + N ⁢ D
44 38 40 43 3eqtr2ri ⊢ N − N + N ⁢ D = − N ⁢ D
45 33 abscli ⊢ N ∈ ℝ
46 45 recni ⊢ N ∈ ℂ
47 35 abscli ⊢ D ∈ ℝ
48 47 recni ⊢ D ∈ ℂ
49 46 48 mulneg1i ⊢ − N ⁢ D = − N ⁢ D
50 37 44 49 3eqtr4i ⊢ N − N + N ⁢ D = − N ⁢ D
51 31 50 breqtrri ⊢ D ∥ N − N + N ⁢ D
52 oveq2 ⊢ r = N + N ⁢ D → N − r = N − N + N ⁢ D
53 52 breq2d ⊢ r = N + N ⁢ D → D ∥ N − r ↔ D ∥ N − N + N ⁢ D
54 53 4 elrab2 ⊢ N + N ⁢ D ∈ S ↔ N + N ⁢ D ∈ ℕ 0 ∧ D ∥ N − N + N ⁢ D
55 17 51 54 mpbir2an ⊢ N + N ⁢ D ∈ S
56 55 ne0ii ⊢ S ≠ ∅
57 infssuzcl ⊢ S ⊆ ℤ ≥ 0 ∧ S ≠ ∅ → sup S ℝ < ∈ S
58 7 56 57 mp2an ⊢ sup S ℝ < ∈ S