Theorem divalglem5

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 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
	divalglem5.5	⊢ 𝑅 = inf ( 𝑆 , ℝ , < )
Assertion	divalglem5	⊢ ( 0 ≤ 𝑅 ∧ 𝑅 < ( abs ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		divalglem0.1	⊢ 𝑁 ∈ ℤ
2		divalglem0.2	⊢ 𝐷 ∈ ℤ
3		divalglem1.3	⊢ 𝐷 ≠ 0
4		divalglem2.4	⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
5		divalglem5.5	⊢ 𝑅 = inf ( 𝑆 , ℝ , < )
6	1 2 3 4	divalglem2	⊢ inf ( 𝑆 , ℝ , < ) ∈ 𝑆
7	5 6	eqeltri	⊢ 𝑅 ∈ 𝑆
8		oveq2	⊢ ( 𝑥 = 𝑅 → ( 𝑁 − 𝑥 ) = ( 𝑁 − 𝑅 ) )
9	8	breq2d	⊢ ( 𝑥 = 𝑅 → ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) )
10		oveq2	⊢ ( 𝑟 = 𝑥 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝑥 ) )
11	10	breq2d	⊢ ( 𝑟 = 𝑥 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) )
12	11	cbvrabv	⊢ { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) } = { 𝑥 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑥 ) }
13	4 12	eqtri	⊢ 𝑆 = { 𝑥 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑥 ) }
14	9 13	elrab2	⊢ ( 𝑅 ∈ 𝑆 ↔ ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) )
15	7 14	mpbi	⊢ ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) )
16	15	simpli	⊢ 𝑅 ∈ ℕ0
17	16	nn0ge0i	⊢ 0 ≤ 𝑅
18		nnabscl	⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ )
19	2 3 18	mp2an	⊢ ( abs ‘ 𝐷 ) ∈ ℕ
20	19	nngt0i	⊢ 0 < ( abs ‘ 𝐷 )
21		0re	⊢ 0 ∈ ℝ
22		zcn	⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
23	2 22	ax-mp	⊢ 𝐷 ∈ ℂ
24	23	abscli	⊢ ( abs ‘ 𝐷 ) ∈ ℝ
25	21 24	ltnlei	⊢ ( 0 < ( abs ‘ 𝐷 ) ↔ ¬ ( abs ‘ 𝐷 ) ≤ 0 )
26	20 25	mpbi	⊢ ¬ ( abs ‘ 𝐷 ) ≤ 0
27	4	ssrab3	⊢ 𝑆 ⊆ ℕ0
28		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
29	27 28	sseqtri	⊢ 𝑆 ⊆ ( ℤ≥ ‘ 0 )
30		nn0abscl	⊢ ( 𝐷 ∈ ℤ → ( abs ‘ 𝐷 ) ∈ ℕ0 )
31	2 30	ax-mp	⊢ ( abs ‘ 𝐷 ) ∈ ℕ0
32		nn0sub2	⊢ ( ( ( abs ‘ 𝐷 ) ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ ( abs ‘ 𝐷 ) ≤ 𝑅 ) → ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ ℕ0 )
33	31 16 32	mp3an12	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ ℕ0 )
34	15	a1i	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) )
35		nn0z	⊢ ( 𝑅 ∈ ℕ0 → 𝑅 ∈ ℤ )
36		1z	⊢ 1 ∈ ℤ
37	1 2	divalglem0	⊢ ( ( 𝑅 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ) )
38	36 37	mpan2	⊢ ( 𝑅 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ) )
39	24	recni	⊢ ( abs ‘ 𝐷 ) ∈ ℂ
40	39	mulid2i	⊢ ( 1 · ( abs ‘ 𝐷 ) ) = ( abs ‘ 𝐷 )
41	40	oveq2i	⊢ ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) = ( 𝑅 − ( abs ‘ 𝐷 ) )
42	41	oveq2i	⊢ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) = ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) )
43	42	breq2i	⊢ ( 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ↔ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) )
44	38 43	syl6ib	⊢ ( 𝑅 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) )
45	35 44	syl	⊢ ( 𝑅 ∈ ℕ0 → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) )
46	45	imp	⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) )
47	34 46	syl	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) )
48		oveq2	⊢ ( 𝑥 = ( 𝑅 − ( abs ‘ 𝐷 ) ) → ( 𝑁 − 𝑥 ) = ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) )
49	48	breq2d	⊢ ( 𝑥 = ( 𝑅 − ( abs ‘ 𝐷 ) ) → ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ↔ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) )
50	49 13	elrab2	⊢ ( ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ 𝑆 ↔ ( ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) )
51	33 47 50	sylanbrc	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ 𝑆 )
52		infssuzle	⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 0 ) ∧ ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) )
53	29 51 52	sylancr	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → inf ( 𝑆 , ℝ , < ) ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) )
54	5 53	eqbrtrid	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) )
55	34	simpld	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ∈ ℕ0 )
56	55	nn0red	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ∈ ℝ )
57		lesub	⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( abs ‘ 𝐷 ) ∈ ℝ ) → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ) )
58	24 57	mp3an3	⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ) )
59	56 56 58	syl2anc	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ) )
60	56	recnd	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ∈ ℂ )
61	60	subidd	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 − 𝑅 ) = 0 )
62	61	breq2d	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ↔ ( abs ‘ 𝐷 ) ≤ 0 ) )
63	59 62	bitrd	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ 0 ) )
64	54 63	mpbid	⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( abs ‘ 𝐷 ) ≤ 0 )
65	26 64	mto	⊢ ¬ ( abs ‘ 𝐷 ) ≤ 𝑅
66	16	nn0rei	⊢ 𝑅 ∈ ℝ
67	66 24	ltnlei	⊢ ( 𝑅 < ( abs ‘ 𝐷 ) ↔ ¬ ( abs ‘ 𝐷 ) ≤ 𝑅 )
68	65 67	mpbir	⊢ 𝑅 < ( abs ‘ 𝐷 )
69	17 68	pm3.2i	⊢ ( 0 ≤ 𝑅 ∧ 𝑅 < ( abs ‘ 𝐷 ) )