# Metamath Proof Explorer

## Theorem irrapxlem1

Description: Lemma for irrapx1 . Divides the unit interval into B half-open sections and using the pigeonhole principle fphpdo finds two multiples of A in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion irrapxlem1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)$

### Proof

Step Hyp Ref Expression
1 fzssuz ${⊢}\left(0\dots {B}\right)\subseteq {ℤ}_{\ge 0}$
2 uzssz ${⊢}{ℤ}_{\ge 0}\subseteq ℤ$
3 zssre ${⊢}ℤ\subseteq ℝ$
4 2 3 sstri ${⊢}{ℤ}_{\ge 0}\subseteq ℝ$
5 1 4 sstri ${⊢}\left(0\dots {B}\right)\subseteq ℝ$
6 5 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \left(0\dots {B}\right)\subseteq ℝ$
7 ovexd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \left(0\dots {B}-1\right)\in \mathrm{V}$
8 nnm1nn0 ${⊢}{B}\in ℕ\to {B}-1\in {ℕ}_{0}$
9 8 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {B}-1\in {ℕ}_{0}$
10 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
11 9 10 eleqtrdi ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {B}-1\in {ℤ}_{\ge 0}$
12 nnz ${⊢}{B}\in ℕ\to {B}\in ℤ$
13 12 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {B}\in ℤ$
14 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
15 14 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {B}\in ℝ$
16 15 ltm1d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {B}-1<{B}$
17 fzsdom2 ${⊢}\left(\left({B}-1\in {ℤ}_{\ge 0}\wedge {B}\in ℤ\right)\wedge {B}-1<{B}\right)\to \left(0\dots {B}-1\right)\prec \left(0\dots {B}\right)$
18 11 13 16 17 syl21anc ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \left(0\dots {B}-1\right)\prec \left(0\dots {B}\right)$
19 14 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\in ℝ$
20 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
21 20 ad2antrr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {A}\in ℝ$
22 elfzelz ${⊢}{a}\in \left(0\dots {B}\right)\to {a}\in ℤ$
23 22 zred ${⊢}{a}\in \left(0\dots {B}\right)\to {a}\in ℝ$
24 23 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {a}\in ℝ$
25 21 24 remulcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {A}{a}\in ℝ$
26 1rp ${⊢}1\in {ℝ}^{+}$
27 modcl ${⊢}\left({A}{a}\in ℝ\wedge 1\in {ℝ}^{+}\right)\to {A}{a}\mathrm{mod}1\in ℝ$
28 25 26 27 sylancl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {A}{a}\mathrm{mod}1\in ℝ$
29 19 28 remulcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{a}\mathrm{mod}1\right)\in ℝ$
30 29 flcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in ℤ$
31 19 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\in ℂ$
32 31 mul01d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\cdot 0=0$
33 modge0 ${⊢}\left({A}{a}\in ℝ\wedge 1\in {ℝ}^{+}\right)\to 0\le {A}{a}\mathrm{mod}1$
34 25 26 33 sylancl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to 0\le {A}{a}\mathrm{mod}1$
35 0red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to 0\in ℝ$
36 nngt0 ${⊢}{B}\in ℕ\to 0<{B}$
37 36 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to 0<{B}$
38 lemul2 ${⊢}\left(0\in ℝ\wedge {A}{a}\mathrm{mod}1\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(0\le {A}{a}\mathrm{mod}1↔{B}\cdot 0\le {B}\left({A}{a}\mathrm{mod}1\right)\right)$
39 35 28 19 37 38 syl112anc ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to \left(0\le {A}{a}\mathrm{mod}1↔{B}\cdot 0\le {B}\left({A}{a}\mathrm{mod}1\right)\right)$
40 34 39 mpbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\cdot 0\le {B}\left({A}{a}\mathrm{mod}1\right)$
41 32 40 eqbrtrrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to 0\le {B}\left({A}{a}\mathrm{mod}1\right)$
42 35 29 lenltd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to \left(0\le {B}\left({A}{a}\mathrm{mod}1\right)↔¬{B}\left({A}{a}\mathrm{mod}1\right)<0\right)$
43 41 42 mpbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ¬{B}\left({A}{a}\mathrm{mod}1\right)<0$
44 0z ${⊢}0\in ℤ$
45 fllt ${⊢}\left({B}\left({A}{a}\mathrm{mod}1\right)\in ℝ\wedge 0\in ℤ\right)\to \left({B}\left({A}{a}\mathrm{mod}1\right)<0↔⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<0\right)$
46 29 44 45 sylancl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to \left({B}\left({A}{a}\mathrm{mod}1\right)<0↔⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<0\right)$
47 43 46 mtbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ¬⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<0$
48 30 zred ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in ℝ$
49 35 48 lenltd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to \left(0\le ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋↔¬⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<0\right)$
50 47 49 mpbird ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to 0\le ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋$
51 elnn0z ${⊢}⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in {ℕ}_{0}↔\left(⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in ℤ\wedge 0\le ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\right)$
52 30 50 51 sylanbrc ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in {ℕ}_{0}$
53 8 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}-1\in {ℕ}_{0}$
54 flle ${⊢}{B}\left({A}{a}\mathrm{mod}1\right)\in ℝ\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\le {B}\left({A}{a}\mathrm{mod}1\right)$
55 29 54 syl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\le {B}\left({A}{a}\mathrm{mod}1\right)$
56 modlt ${⊢}\left({A}{a}\in ℝ\wedge 1\in {ℝ}^{+}\right)\to {A}{a}\mathrm{mod}1<1$
57 25 26 56 sylancl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {A}{a}\mathrm{mod}1<1$
58 1red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to 1\in ℝ$
59 ltmul2 ${⊢}\left({A}{a}\mathrm{mod}1\in ℝ\wedge 1\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}{a}\mathrm{mod}1<1↔{B}\left({A}{a}\mathrm{mod}1\right)<{B}\cdot 1\right)$
60 28 58 19 37 59 syl112anc ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to \left({A}{a}\mathrm{mod}1<1↔{B}\left({A}{a}\mathrm{mod}1\right)<{B}\cdot 1\right)$
61 57 60 mpbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{a}\mathrm{mod}1\right)<{B}\cdot 1$
62 31 mulid1d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\cdot 1={B}$
63 61 62 breqtrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{a}\mathrm{mod}1\right)<{B}$
64 48 29 19 55 63 lelttrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<{B}$
65 nncn ${⊢}{B}\in ℕ\to {B}\in ℂ$
66 ax-1cn ${⊢}1\in ℂ$
67 npcan ${⊢}\left({B}\in ℂ\wedge 1\in ℂ\right)\to {B}-1+1={B}$
68 65 66 67 sylancl ${⊢}{B}\in ℕ\to {B}-1+1={B}$
69 68 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}-1+1={B}$
70 64 69 breqtrrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<{B}-1+1$
71 12 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}\in ℤ$
72 1z ${⊢}1\in ℤ$
73 zsubcl ${⊢}\left({B}\in ℤ\wedge 1\in ℤ\right)\to {B}-1\in ℤ$
74 71 72 73 sylancl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to {B}-1\in ℤ$
75 zleltp1 ${⊢}\left(⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in ℤ\wedge {B}-1\in ℤ\right)\to \left(⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\le {B}-1↔⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<{B}-1+1\right)$
76 30 74 75 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to \left(⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\le {B}-1↔⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋<{B}-1+1\right)$
77 70 76 mpbird ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\le {B}-1$
78 elfz2nn0 ${⊢}⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in \left(0\dots {B}-1\right)↔\left(⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in {ℕ}_{0}\wedge {B}-1\in {ℕ}_{0}\wedge ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\le {B}-1\right)$
79 52 53 77 78 syl3anbrc ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋\in \left(0\dots {B}-1\right)$
80 oveq2 ${⊢}{a}={x}\to {A}{a}={A}{x}$
81 80 oveq1d ${⊢}{a}={x}\to {A}{a}\mathrm{mod}1={A}{x}\mathrm{mod}1$
82 81 oveq2d ${⊢}{a}={x}\to {B}\left({A}{a}\mathrm{mod}1\right)={B}\left({A}{x}\mathrm{mod}1\right)$
83 82 fveq2d ${⊢}{a}={x}\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋$
84 oveq2 ${⊢}{a}={y}\to {A}{a}={A}{y}$
85 84 oveq1d ${⊢}{a}={y}\to {A}{a}\mathrm{mod}1={A}{y}\mathrm{mod}1$
86 85 oveq2d ${⊢}{a}={y}\to {B}\left({A}{a}\mathrm{mod}1\right)={B}\left({A}{y}\mathrm{mod}1\right)$
87 86 fveq2d ${⊢}{a}={y}\to ⌊{B}\left({A}{a}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋$
88 6 7 18 79 83 87 fphpdo ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)$