This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑁 ∈ ℤ
divalglem0.2 ⊢ 𝐷 ∈ ℤ
divalglem1.3 ⊢ 𝐷 ≠ 0
divalglem2.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
Assertion divalglem2 inf ( 𝑆 , ℝ , < ) ∈ 𝑆

Proof

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