Metamath Proof Explorer

Theorem irrapxlem2

Description: Lemma for irrapx1 . Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion irrapxlem2 ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 irrapxlem1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )
2 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
3 2 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ∈ ℝ )
4 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
5 4 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝐴 ∈ ℝ )
6 elfzelz ⊢ ( 𝑥 ∈ ( 0 ... 𝐵 ) → 𝑥 ∈ ℤ )
7 6 zred ⊢ ( 𝑥 ∈ ( 0 ... 𝐵 ) → 𝑥 ∈ ℝ )
8 7 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝑥 ∈ ℝ )
9 5 8 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐴 · 𝑥 ) ∈ ℝ )
10 1rp ⊢ 1 ∈ ℝ+
11 10 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 1 ∈ ℝ+ )
12 9 11 modcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐴 · 𝑥 ) mod 1 ) ∈ ℝ )
13 3 12 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ∈ ℝ )
14 intfrac ⊢ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ∈ ℝ → ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) = ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) )
15 13 14 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) = ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) )
16 elfzelz ⊢ ( 𝑦 ∈ ( 0 ... 𝐵 ) → 𝑦 ∈ ℤ )
17 16 zred ⊢ ( 𝑦 ∈ ( 0 ... 𝐵 ) → 𝑦 ∈ ℝ )
18 17 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝑦 ∈ ℝ )
19 5 18 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐴 · 𝑦 ) ∈ ℝ )
20 19 11 modcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐴 · 𝑦 ) mod 1 ) ∈ ℝ )
21 3 20 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ∈ ℝ )
22 intfrac ⊢ ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ∈ ℝ → ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) = ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) )
23 21 22 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) = ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) )
24 15 23 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) = ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) )
25 24 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) )
26 25 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) )
27 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) )
28 27 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) = ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) )
29 28 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) = ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) )
30 29 fveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) )
31 21 flcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ∈ ℤ )
32 31 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ∈ ℂ )
33 13 11 modcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ∈ ℝ )
34 33 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ∈ ℂ )
35 21 11 modcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ∈ ℝ )
36 35 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ∈ ℂ )
37 32 34 36 pnpcand ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) = ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) − ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) )
38 37 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) = ( abs ‘ ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) − ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) )
39 0red ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 0 ∈ ℝ )
40 1red ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 1 ∈ ℝ )
41 modelico ⊢ ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ+ ) → ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ∈ ( 0 [,) 1 ) )
42 13 10 41 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ∈ ( 0 [,) 1 ) )
43 modelico ⊢ ( ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ+ ) → ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ∈ ( 0 [,) 1 ) )
44 21 10 43 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ∈ ( 0 [,) 1 ) )
45 icodiamlt ⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ∈ ( 0 [,) 1 ) ∧ ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ∈ ( 0 [,) 1 ) ) ) → ( abs ‘ ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) − ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) < ( 1 − 0 ) )
46 39 40 42 44 45 syl22anc ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) − ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) < ( 1 − 0 ) )
47 1m0e1 ⊢ ( 1 − 0 ) = 1
48 46 47 breqtrdi ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) − ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) < 1 )
49 38 48 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) < 1 )
50 49 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) < 1 )
51 30 50 eqbrtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) mod 1 ) ) − ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) + ( ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) mod 1 ) ) ) ) < 1 )
52 26 51 eqbrtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < 1 )
53 52 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) → ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < 1 ) )
54 12 20 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ∈ ℝ )
55 54 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ∈ ℂ )
56 55 abscld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ∈ ℝ )
57 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
58 57 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 0 < 𝐵 )
59 58 gt0ne0d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ≠ 0 )
60 3 59 rereccld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 1 / 𝐵 ) ∈ ℝ )
61 ltmul2 ⊢ ( ( ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ∈ ℝ ∧ ( 1 / 𝐵 ) ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ↔ ( 𝐵 · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < ( 𝐵 · ( 1 / 𝐵 ) ) ) )
62 56 60 3 58 61 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ↔ ( 𝐵 · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < ( 𝐵 · ( 1 / 𝐵 ) ) ) )
63 nnnn0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
64 63 nn0ge0d ⊢ ( 𝐵 ∈ ℕ → 0 ≤ 𝐵 )
65 64 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ 𝐵 )
66 3 65 absidd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ 𝐵 ) = 𝐵 )
67 66 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝐵 = ( abs ‘ 𝐵 ) )
68 67 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) = ( ( abs ‘ 𝐵 ) · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )
69 3 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ∈ ℂ )
70 69 55 absmuld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( 𝐵 · ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) = ( ( abs ‘ 𝐵 ) · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )
71 12 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐴 · 𝑥 ) mod 1 ) ∈ ℂ )
72 20 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐴 · 𝑦 ) mod 1 ) ∈ ℂ )
73 69 71 72 subdid ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) = ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) )
74 73 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( abs ‘ ( 𝐵 · ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) = ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )
75 68 70 74 3eqtr2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) = ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )
76 69 59 recidd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( 1 / 𝐵 ) ) = 1 )
77 75 76 breq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < ( 𝐵 · ( 1 / 𝐵 ) ) ↔ ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < 1 ) )
78 62 77 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ↔ ( abs ‘ ( ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) − ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) < 1 ) )
79 53 78 sylibrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) → ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) )
80 79 anim2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) ∧ 𝑦 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝑥 < 𝑦 ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ( 𝑥 < 𝑦 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) )
81 80 reximdva ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ... 𝐵 ) ) → ( ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) )
82 81 reximdva ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) → ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) )
83 1 82 mpd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑥 ) mod 1 ) − ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) )