Metamath Proof Explorer


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 ‘ 𝐷 ) )