Metamath Proof Explorer


Theorem irrapxlem3

Description: Lemma for irrapx1 . By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem3 ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( 1 ... ๐ต ) โˆƒ ๐‘ฆ โˆˆ โ„•0 ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) )

Proof

Step Hyp Ref Expression
1 irrapxlem2 โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โ†’ โˆƒ ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆƒ ๐‘ โˆˆ ( 0 ... ๐ต ) ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) )
2 1z โŠข 1 โˆˆ โ„ค
3 2 a1i โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 1 โˆˆ โ„ค )
4 simpllr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐ต โˆˆ โ„• )
5 4 nnzd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐ต โˆˆ โ„ค )
6 simplrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘ โˆˆ ( 0 ... ๐ต ) )
7 6 elfzelzd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘ โˆˆ โ„ค )
8 simplrl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘Ž โˆˆ ( 0 ... ๐ต ) )
9 8 elfzelzd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘Ž โˆˆ โ„ค )
10 7 9 zsubcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ ๐‘Ž ) โˆˆ โ„ค )
11 1m1e0 โŠข ( 1 โˆ’ 1 ) = 0
12 elfzelz โŠข ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โ†’ ๐‘Ž โˆˆ โ„ค )
13 12 ad2antrl โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โ†’ ๐‘Ž โˆˆ โ„ค )
14 13 zred โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โ†’ ๐‘Ž โˆˆ โ„ )
15 elfzelz โŠข ( ๐‘ โˆˆ ( 0 ... ๐ต ) โ†’ ๐‘ โˆˆ โ„ค )
16 15 ad2antll โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โ†’ ๐‘ โˆˆ โ„ค )
17 16 zred โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โ†’ ๐‘ โˆˆ โ„ )
18 14 17 posdifd โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โ†’ ( ๐‘Ž < ๐‘ โ†” 0 < ( ๐‘ โˆ’ ๐‘Ž ) ) )
19 18 biimpa โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 0 < ( ๐‘ โˆ’ ๐‘Ž ) )
20 11 19 eqbrtrid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( 1 โˆ’ 1 ) < ( ๐‘ โˆ’ ๐‘Ž ) )
21 zlem1lt โŠข ( ( 1 โˆˆ โ„ค โˆง ( ๐‘ โˆ’ ๐‘Ž ) โˆˆ โ„ค ) โ†’ ( 1 โ‰ค ( ๐‘ โˆ’ ๐‘Ž ) โ†” ( 1 โˆ’ 1 ) < ( ๐‘ โˆ’ ๐‘Ž ) ) )
22 2 10 21 sylancr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( 1 โ‰ค ( ๐‘ โˆ’ ๐‘Ž ) โ†” ( 1 โˆ’ 1 ) < ( ๐‘ โˆ’ ๐‘Ž ) ) )
23 20 22 mpbird โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 1 โ‰ค ( ๐‘ โˆ’ ๐‘Ž ) )
24 7 zred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘ โˆˆ โ„ )
25 9 zred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘Ž โˆˆ โ„ )
26 24 25 resubcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ ๐‘Ž ) โˆˆ โ„ )
27 0red โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 0 โˆˆ โ„ )
28 24 27 resubcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ 0 ) โˆˆ โ„ )
29 4 nnred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐ต โˆˆ โ„ )
30 elfzle1 โŠข ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โ†’ 0 โ‰ค ๐‘Ž )
31 8 30 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 0 โ‰ค ๐‘Ž )
32 27 25 24 31 lesub2dd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ ๐‘Ž ) โ‰ค ( ๐‘ โˆ’ 0 ) )
33 24 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘ โˆˆ โ„‚ )
34 33 subid1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ 0 ) = ๐‘ )
35 elfzle2 โŠข ( ๐‘ โˆˆ ( 0 ... ๐ต ) โ†’ ๐‘ โ‰ค ๐ต )
36 6 35 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘ โ‰ค ๐ต )
37 34 36 eqbrtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ 0 ) โ‰ค ๐ต )
38 26 28 29 32 37 letrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ ๐‘Ž ) โ‰ค ๐ต )
39 3 5 10 23 38 elfzd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘ โˆ’ ๐‘Ž ) โˆˆ ( 1 ... ๐ต ) )
40 39 adantrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) ) โ†’ ( ๐‘ โˆ’ ๐‘Ž ) โˆˆ ( 1 ... ๐ต ) )
41 rpre โŠข ( ๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„ )
42 41 ad3antrrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐ด โˆˆ โ„ )
43 42 25 remulcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐ด ยท ๐‘Ž ) โˆˆ โ„ )
44 42 24 remulcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐ด ยท ๐‘ ) โˆˆ โ„ )
45 simpr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘Ž < ๐‘ )
46 25 24 45 ltled โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘Ž โ‰ค ๐‘ )
47 rpgt0 โŠข ( ๐ด โˆˆ โ„+ โ†’ 0 < ๐ด )
48 47 ad3antrrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 0 < ๐ด )
49 lemul2 โŠข ( ( ๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ( ๐ด โˆˆ โ„ โˆง 0 < ๐ด ) ) โ†’ ( ๐‘Ž โ‰ค ๐‘ โ†” ( ๐ด ยท ๐‘Ž ) โ‰ค ( ๐ด ยท ๐‘ ) ) )
50 25 24 42 48 49 syl112anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐‘Ž โ‰ค ๐‘ โ†” ( ๐ด ยท ๐‘Ž ) โ‰ค ( ๐ด ยท ๐‘ ) ) )
51 46 50 mpbid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐ด ยท ๐‘Ž ) โ‰ค ( ๐ด ยท ๐‘ ) )
52 flword2 โŠข ( ( ( ๐ด ยท ๐‘Ž ) โˆˆ โ„ โˆง ( ๐ด ยท ๐‘ ) โˆˆ โ„ โˆง ( ๐ด ยท ๐‘Ž ) โ‰ค ( ๐ด ยท ๐‘ ) ) โ†’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) )
53 43 44 51 52 syl3anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) )
54 uznn0sub โŠข ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โˆˆ โ„•0 )
55 53 54 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โˆˆ โ„•0 )
56 55 adantrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โˆˆ โ„•0 )
57 42 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐ด โˆˆ โ„‚ )
58 25 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ๐‘Ž โˆˆ โ„‚ )
59 57 33 58 subdid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) = ( ( ๐ด ยท ๐‘ ) โˆ’ ( ๐ด ยท ๐‘Ž ) ) )
60 59 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) = ( ( ( ๐ด ยท ๐‘ ) โˆ’ ( ๐ด ยท ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) )
61 44 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐ด ยท ๐‘ ) โˆˆ โ„‚ )
62 43 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ๐ด ยท ๐‘Ž ) โˆˆ โ„‚ )
63 44 flcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆˆ โ„ค )
64 63 zcnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆˆ โ„‚ )
65 43 flcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) โˆˆ โ„ค )
66 65 zcnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) โˆˆ โ„‚ )
67 61 62 64 66 sub4d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ( ๐ด ยท ๐‘ ) โˆ’ ( ๐ด ยท ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) = ( ( ( ๐ด ยท ๐‘ ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) ) โˆ’ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) )
68 modfrac โŠข ( ( ๐ด ยท ๐‘ ) โˆˆ โ„ โ†’ ( ( ๐ด ยท ๐‘ ) mod 1 ) = ( ( ๐ด ยท ๐‘ ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) ) )
69 44 68 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘ ) mod 1 ) = ( ( ๐ด ยท ๐‘ ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) ) )
70 69 eqcomd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘ ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) ) = ( ( ๐ด ยท ๐‘ ) mod 1 ) )
71 modfrac โŠข ( ( ๐ด ยท ๐‘Ž ) โˆˆ โ„ โ†’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) = ( ( ๐ด ยท ๐‘Ž ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) )
72 43 71 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) = ( ( ๐ด ยท ๐‘Ž ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) )
73 72 eqcomd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) = ( ( ๐ด ยท ๐‘Ž ) mod 1 ) )
74 70 73 oveq12d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ( ๐ด ยท ๐‘ ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) ) โˆ’ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) = ( ( ( ๐ด ยท ๐‘ ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) ) )
75 60 67 74 3eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) = ( ( ( ๐ด ยท ๐‘ ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) ) )
76 75 fveq2d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) = ( abs โ€˜ ( ( ( ๐ด ยท ๐‘ ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) ) ) )
77 1rp โŠข 1 โˆˆ โ„+
78 77 a1i โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ 1 โˆˆ โ„+ )
79 44 78 modcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘ ) mod 1 ) โˆˆ โ„ )
80 79 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘ ) mod 1 ) โˆˆ โ„‚ )
81 43 78 modcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆˆ โ„ )
82 81 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆˆ โ„‚ )
83 80 82 abssubd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( abs โ€˜ ( ( ( ๐ด ยท ๐‘ ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘Ž ) mod 1 ) ) ) = ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) )
84 76 83 eqtr2d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) = ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) )
85 84 breq1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) โ†” ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) < ( 1 / ๐ต ) ) )
86 85 biimpd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ๐‘Ž < ๐‘ ) โ†’ ( ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) < ( 1 / ๐ต ) ) )
87 86 impr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) < ( 1 / ๐ต ) )
88 oveq2 โŠข ( ๐‘ฅ = ( ๐‘ โˆ’ ๐‘Ž ) โ†’ ( ๐ด ยท ๐‘ฅ ) = ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) )
89 88 fvoveq1d โŠข ( ๐‘ฅ = ( ๐‘ โˆ’ ๐‘Ž ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) = ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ๐‘ฆ ) ) )
90 89 breq1d โŠข ( ๐‘ฅ = ( ๐‘ โˆ’ ๐‘Ž ) โ†’ ( ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) โ†” ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) ) )
91 oveq2 โŠข ( ๐‘ฆ = ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โ†’ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ๐‘ฆ ) = ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) )
92 91 fveq2d โŠข ( ๐‘ฆ = ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ๐‘ฆ ) ) = ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) )
93 92 breq1d โŠข ( ๐‘ฆ = ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โ†’ ( ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) โ†” ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) < ( 1 / ๐ต ) ) )
94 90 93 rspc2ev โŠข ( ( ( ๐‘ โˆ’ ๐‘Ž ) โˆˆ ( 1 ... ๐ต ) โˆง ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) โˆˆ โ„•0 โˆง ( abs โ€˜ ( ( ๐ด ยท ( ๐‘ โˆ’ ๐‘Ž ) ) โˆ’ ( ( โŒŠ โ€˜ ( ๐ด ยท ๐‘ ) ) โˆ’ ( โŒŠ โ€˜ ( ๐ด ยท ๐‘Ž ) ) ) ) ) < ( 1 / ๐ต ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( 1 ... ๐ต ) โˆƒ ๐‘ฆ โˆˆ โ„•0 ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) )
95 40 56 87 94 syl3anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โˆง ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( 1 ... ๐ต ) โˆƒ ๐‘ฆ โˆˆ โ„•0 ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) )
96 95 ex โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โˆง ( ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆง ๐‘ โˆˆ ( 0 ... ๐ต ) ) ) โ†’ ( ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( 1 ... ๐ต ) โˆƒ ๐‘ฆ โˆˆ โ„•0 ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) ) )
97 96 rexlimdvva โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘Ž โˆˆ ( 0 ... ๐ต ) โˆƒ ๐‘ โˆˆ ( 0 ... ๐ต ) ( ๐‘Ž < ๐‘ โˆง ( abs โ€˜ ( ( ( ๐ด ยท ๐‘Ž ) mod 1 ) โˆ’ ( ( ๐ด ยท ๐‘ ) mod 1 ) ) ) < ( 1 / ๐ต ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( 1 ... ๐ต ) โˆƒ ๐‘ฆ โˆˆ โ„•0 ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) ) )
98 1 97 mpd โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„• ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( 1 ... ๐ต ) โˆƒ ๐‘ฆ โˆˆ โ„•0 ( abs โ€˜ ( ( ๐ด ยท ๐‘ฅ ) โˆ’ ๐‘ฆ ) ) < ( 1 / ๐ต ) )