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

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 mullidi ⊢ ( 1 · ( abs ‘ 𝐷 ) ) = ( abs ‘ 𝐷 )
41 40 oveq2i ⊢ ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) = ( 𝑅 − ( abs ‘ 𝐷 ) )
42 41 oveq2i ⊢ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) = ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) )
43 42 breq2i ⊢ ( 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ↔ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) )
44 38 43 imbitrdi ⊢ ( 𝑅 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 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 ‘ 𝐷 ) )