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 / ๐ต ) ) )