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 
|- ( ( A e. RR+ /\ B e. NN ) -> E. x e. ( 0 ... B ) E. y e. ( 0 ... B ) ( x < y /\ ( abs ` ( ( ( A x. x ) mod 1 ) - ( ( A x. y ) mod 1 ) ) ) < ( 1 / B ) ) )

Proof

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