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 ( 𝑆 , ℝ , < ) ∈ 𝑆