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

Proof

Step Hyp Ref Expression
1 irrapxlem2 
 |-  ( ( A e. RR+ /\ B e. NN ) -> E. a e. ( 0 ... B ) E. b e. ( 0 ... B ) ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) )
2 1z 
 |-  1 e. ZZ
3 2 a1i 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 1 e. ZZ )
4 simpllr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> B e. NN )
5 4 nnzd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> B e. ZZ )
6 simplrr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> b e. ( 0 ... B ) )
7 6 elfzelzd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> b e. ZZ )
8 simplrl 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> a e. ( 0 ... B ) )
9 8 elfzelzd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> a e. ZZ )
10 7 9 zsubcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - a ) e. ZZ )
11 1m1e0 
 |-  ( 1 - 1 ) = 0
12 elfzelz 
 |-  ( a e. ( 0 ... B ) -> a e. ZZ )
13 12 ad2antrl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) -> a e. ZZ )
14 13 zred 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) -> a e. RR )
15 elfzelz 
 |-  ( b e. ( 0 ... B ) -> b e. ZZ )
16 15 ad2antll 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) -> b e. ZZ )
17 16 zred 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) -> b e. RR )
18 14 17 posdifd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) -> ( a < b <-> 0 < ( b - a ) ) )
19 18 biimpa 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 0 < ( b - a ) )
20 11 19 eqbrtrid 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( 1 - 1 ) < ( b - a ) )
21 zlem1lt 
 |-  ( ( 1 e. ZZ /\ ( b - a ) e. ZZ ) -> ( 1 <_ ( b - a ) <-> ( 1 - 1 ) < ( b - a ) ) )
22 2 10 21 sylancr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( 1 <_ ( b - a ) <-> ( 1 - 1 ) < ( b - a ) ) )
23 20 22 mpbird 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 1 <_ ( b - a ) )
24 7 zred 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> b e. RR )
25 9 zred 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> a e. RR )
26 24 25 resubcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - a ) e. RR )
27 0red 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 0 e. RR )
28 24 27 resubcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - 0 ) e. RR )
29 4 nnred 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> B e. RR )
30 elfzle1 
 |-  ( a e. ( 0 ... B ) -> 0 <_ a )
31 8 30 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 0 <_ a )
32 27 25 24 31 lesub2dd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - a ) <_ ( b - 0 ) )
33 24 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> b e. CC )
34 33 subid1d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - 0 ) = b )
35 elfzle2 
 |-  ( b e. ( 0 ... B ) -> b <_ B )
36 6 35 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> b <_ B )
37 34 36 eqbrtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - 0 ) <_ B )
38 26 28 29 32 37 letrd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - a ) <_ B )
39 3 5 10 23 38 elfzd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( b - a ) e. ( 1 ... B ) )
40 39 adantrr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) ) -> ( b - a ) e. ( 1 ... B ) )
41 rpre 
 |-  ( A e. RR+ -> A e. RR )
42 41 ad3antrrr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> A e. RR )
43 42 25 remulcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( A x. a ) e. RR )
44 42 24 remulcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( A x. b ) e. RR )
45 simpr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> a < b )
46 25 24 45 ltled 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> a <_ b )
47 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
48 47 ad3antrrr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 0 < A )
49 lemul2 
 |-  ( ( a e. RR /\ b e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( a <_ b <-> ( A x. a ) <_ ( A x. b ) ) )
50 25 24 42 48 49 syl112anc 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( a <_ b <-> ( A x. a ) <_ ( A x. b ) ) )
51 46 50 mpbid 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( A x. a ) <_ ( A x. b ) )
52 flword2 
 |-  ( ( ( A x. a ) e. RR /\ ( A x. b ) e. RR /\ ( A x. a ) <_ ( A x. b ) ) -> ( |_ ` ( A x. b ) ) e. ( ZZ>= ` ( |_ ` ( A x. a ) ) ) )
53 43 44 51 52 syl3anc 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( |_ ` ( A x. b ) ) e. ( ZZ>= ` ( |_ ` ( A x. a ) ) ) )
54 uznn0sub 
 |-  ( ( |_ ` ( A x. b ) ) e. ( ZZ>= ` ( |_ ` ( A x. a ) ) ) -> ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) e. NN0 )
55 53 54 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) e. NN0 )
56 55 adantrr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) ) -> ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) e. NN0 )
57 42 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> A e. CC )
58 25 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> a e. CC )
59 57 33 58 subdid 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( A x. ( b - a ) ) = ( ( A x. b ) - ( A x. a ) ) )
60 59 oveq1d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) = ( ( ( A x. b ) - ( A x. a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) )
61 44 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( A x. b ) e. CC )
62 43 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( A x. a ) e. CC )
63 44 flcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( |_ ` ( A x. b ) ) e. ZZ )
64 63 zcnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( |_ ` ( A x. b ) ) e. CC )
65 43 flcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( |_ ` ( A x. a ) ) e. ZZ )
66 65 zcnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( |_ ` ( A x. a ) ) e. CC )
67 61 62 64 66 sub4d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( ( A x. b ) - ( A x. a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) = ( ( ( A x. b ) - ( |_ ` ( A x. b ) ) ) - ( ( A x. a ) - ( |_ ` ( A x. a ) ) ) ) )
68 modfrac 
 |-  ( ( A x. b ) e. RR -> ( ( A x. b ) mod 1 ) = ( ( A x. b ) - ( |_ ` ( A x. b ) ) ) )
69 44 68 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. b ) mod 1 ) = ( ( A x. b ) - ( |_ ` ( A x. b ) ) ) )
70 69 eqcomd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. b ) - ( |_ ` ( A x. b ) ) ) = ( ( A x. b ) mod 1 ) )
71 modfrac 
 |-  ( ( A x. a ) e. RR -> ( ( A x. a ) mod 1 ) = ( ( A x. a ) - ( |_ ` ( A x. a ) ) ) )
72 43 71 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. a ) mod 1 ) = ( ( A x. a ) - ( |_ ` ( A x. a ) ) ) )
73 72 eqcomd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. a ) - ( |_ ` ( A x. a ) ) ) = ( ( A x. a ) mod 1 ) )
74 70 73 oveq12d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( ( A x. b ) - ( |_ ` ( A x. b ) ) ) - ( ( A x. a ) - ( |_ ` ( A x. a ) ) ) ) = ( ( ( A x. b ) mod 1 ) - ( ( A x. a ) mod 1 ) ) )
75 60 67 74 3eqtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) = ( ( ( A x. b ) mod 1 ) - ( ( A x. a ) mod 1 ) ) )
76 75 fveq2d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) = ( abs ` ( ( ( A x. b ) mod 1 ) - ( ( A x. a ) mod 1 ) ) ) )
77 1rp 
 |-  1 e. RR+
78 77 a1i 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> 1 e. RR+ )
79 44 78 modcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. b ) mod 1 ) e. RR )
80 79 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. b ) mod 1 ) e. CC )
81 43 78 modcld 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. a ) mod 1 ) e. RR )
82 81 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( A x. a ) mod 1 ) e. CC )
83 80 82 abssubd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( abs ` ( ( ( A x. b ) mod 1 ) - ( ( A x. a ) mod 1 ) ) ) = ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) )
84 76 83 eqtr2d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) = ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) )
85 84 breq1d 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) <-> ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) < ( 1 / B ) ) )
86 85 biimpd 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ a < b ) -> ( ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) -> ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) < ( 1 / B ) ) )
87 86 impr 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) ) -> ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) < ( 1 / B ) )
88 oveq2 
 |-  ( x = ( b - a ) -> ( A x. x ) = ( A x. ( b - a ) ) )
89 88 fvoveq1d 
 |-  ( x = ( b - a ) -> ( abs ` ( ( A x. x ) - y ) ) = ( abs ` ( ( A x. ( b - a ) ) - y ) ) )
90 89 breq1d 
 |-  ( x = ( b - a ) -> ( ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) <-> ( abs ` ( ( A x. ( b - a ) ) - y ) ) < ( 1 / B ) ) )
91 oveq2 
 |-  ( y = ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) -> ( ( A x. ( b - a ) ) - y ) = ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) )
92 91 fveq2d 
 |-  ( y = ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) -> ( abs ` ( ( A x. ( b - a ) ) - y ) ) = ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) )
93 92 breq1d 
 |-  ( y = ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) -> ( ( abs ` ( ( A x. ( b - a ) ) - y ) ) < ( 1 / B ) <-> ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) < ( 1 / B ) ) )
94 90 93 rspc2ev 
 |-  ( ( ( b - a ) e. ( 1 ... B ) /\ ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) e. NN0 /\ ( abs ` ( ( A x. ( b - a ) ) - ( ( |_ ` ( A x. b ) ) - ( |_ ` ( A x. a ) ) ) ) ) < ( 1 / B ) ) -> E. x e. ( 1 ... B ) E. y e. NN0 ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) )
95 40 56 87 94 syl3anc 
 |-  ( ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) /\ ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) ) -> E. x e. ( 1 ... B ) E. y e. NN0 ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) )
96 95 ex 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ ( a e. ( 0 ... B ) /\ b e. ( 0 ... B ) ) ) -> ( ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) -> E. x e. ( 1 ... B ) E. y e. NN0 ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) ) )
97 96 rexlimdvva 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( E. a e. ( 0 ... B ) E. b e. ( 0 ... B ) ( a < b /\ ( abs ` ( ( ( A x. a ) mod 1 ) - ( ( A x. b ) mod 1 ) ) ) < ( 1 / B ) ) -> E. x e. ( 1 ... B ) E. y e. NN0 ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) ) )
98 1 97 mpd 
 |-  ( ( A e. RR+ /\ B e. NN ) -> E. x e. ( 1 ... B ) E. y e. NN0 ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) )