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 
|- ( ( 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fzssuz 
 |-  ( 0 ... B ) C_ ( ZZ>= ` 0 )
2 uzssz 
 |-  ( ZZ>= ` 0 ) C_ ZZ
3 zssre 
 |-  ZZ C_ RR
4 2 3 sstri 
 |-  ( ZZ>= ` 0 ) C_ RR
5 1 4 sstri 
 |-  ( 0 ... B ) C_ RR
6 5 a1i 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( 0 ... B ) C_ RR )
7 ovexd 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( 0 ... ( B - 1 ) ) e. _V )
8 nnm1nn0 
 |-  ( B e. NN -> ( B - 1 ) e. NN0 )
9 8 adantl 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( B - 1 ) e. NN0 )
10 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
11 9 10 eleqtrdi 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( B - 1 ) e. ( ZZ>= ` 0 ) )
12 nnz 
 |-  ( B e. NN -> B e. ZZ )
13 12 adantl 
 |-  ( ( A e. RR+ /\ B e. NN ) -> B e. ZZ )
14 nnre 
 |-  ( B e. NN -> B e. RR )
15 14 adantl 
 |-  ( ( A e. RR+ /\ B e. NN ) -> B e. RR )
16 15 ltm1d 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( B - 1 ) < B )
17 fzsdom2 
 |-  ( ( ( ( B - 1 ) e. ( ZZ>= ` 0 ) /\ B e. ZZ ) /\ ( B - 1 ) < B ) -> ( 0 ... ( B - 1 ) ) ~< ( 0 ... B ) )
18 11 13 16 17 syl21anc 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( 0 ... ( B - 1 ) ) ~< ( 0 ... B ) )
19 14 ad2antlr 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> B e. RR )
20 rpre 
 |-  ( A e. RR+ -> A e. RR )
21 20 ad2antrr 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> A e. RR )
22 elfzelz 
 |-  ( a e. ( 0 ... B ) -> a e. ZZ )
23 22 zred 
 |-  ( a e. ( 0 ... B ) -> a e. RR )
24 23 adantl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> a e. RR )
25 21 24 remulcld 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( A x. a ) e. RR )
26 1rp 
 |-  1 e. RR+
27 modcl 
 |-  ( ( ( A x. a ) e. RR /\ 1 e. RR+ ) -> ( ( A x. a ) mod 1 ) e. RR )
28 25 26 27 sylancl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( ( A x. a ) mod 1 ) e. RR )
29 19 28 remulcld 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B x. ( ( A x. a ) mod 1 ) ) e. RR )
30 29 flcld 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. ZZ )
31 19 recnd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> B e. CC )
32 31 mul01d 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B x. 0 ) = 0 )
33 modge0 
 |-  ( ( ( A x. a ) e. RR /\ 1 e. RR+ ) -> 0 <_ ( ( A x. a ) mod 1 ) )
34 25 26 33 sylancl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> 0 <_ ( ( A x. a ) mod 1 ) )
35 0red 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> 0 e. RR )
36 nngt0 
 |-  ( B e. NN -> 0 < B )
37 36 ad2antlr 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> 0 < B )
38 lemul2 
 |-  ( ( 0 e. RR /\ ( ( A x. a ) mod 1 ) e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( 0 <_ ( ( A x. a ) mod 1 ) <-> ( B x. 0 ) <_ ( B x. ( ( A x. a ) mod 1 ) ) ) )
39 35 28 19 37 38 syl112anc 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( 0 <_ ( ( A x. a ) mod 1 ) <-> ( B x. 0 ) <_ ( B x. ( ( A x. a ) mod 1 ) ) ) )
40 34 39 mpbid 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B x. 0 ) <_ ( B x. ( ( A x. a ) mod 1 ) ) )
41 32 40 eqbrtrrd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> 0 <_ ( B x. ( ( A x. a ) mod 1 ) ) )
42 35 29 lenltd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( 0 <_ ( B x. ( ( A x. a ) mod 1 ) ) <-> -. ( B x. ( ( A x. a ) mod 1 ) ) < 0 ) )
43 41 42 mpbid 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> -. ( B x. ( ( A x. a ) mod 1 ) ) < 0 )
44 0z 
 |-  0 e. ZZ
45 fllt 
 |-  ( ( ( B x. ( ( A x. a ) mod 1 ) ) e. RR /\ 0 e. ZZ ) -> ( ( B x. ( ( A x. a ) mod 1 ) ) < 0 <-> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < 0 ) )
46 29 44 45 sylancl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( ( B x. ( ( A x. a ) mod 1 ) ) < 0 <-> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < 0 ) )
47 43 46 mtbid 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> -. ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < 0 )
48 30 zred 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. RR )
49 35 48 lenltd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( 0 <_ ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <-> -. ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < 0 ) )
50 47 49 mpbird 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> 0 <_ ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) )
51 elnn0z 
 |-  ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. NN0 <-> ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) ) )
52 30 50 51 sylanbrc 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. NN0 )
53 8 ad2antlr 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B - 1 ) e. NN0 )
54 flle 
 |-  ( ( B x. ( ( A x. a ) mod 1 ) ) e. RR -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <_ ( B x. ( ( A x. a ) mod 1 ) ) )
55 29 54 syl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <_ ( B x. ( ( A x. a ) mod 1 ) ) )
56 modlt 
 |-  ( ( ( A x. a ) e. RR /\ 1 e. RR+ ) -> ( ( A x. a ) mod 1 ) < 1 )
57 25 26 56 sylancl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( ( A x. a ) mod 1 ) < 1 )
58 1red 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> 1 e. RR )
59 ltmul2 
 |-  ( ( ( ( A x. a ) mod 1 ) e. RR /\ 1 e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( ( A x. a ) mod 1 ) < 1 <-> ( B x. ( ( A x. a ) mod 1 ) ) < ( B x. 1 ) ) )
60 28 58 19 37 59 syl112anc 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( ( ( A x. a ) mod 1 ) < 1 <-> ( B x. ( ( A x. a ) mod 1 ) ) < ( B x. 1 ) ) )
61 57 60 mpbid 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B x. ( ( A x. a ) mod 1 ) ) < ( B x. 1 ) )
62 31 mulridd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B x. 1 ) = B )
63 61 62 breqtrd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B x. ( ( A x. a ) mod 1 ) ) < B )
64 48 29 19 55 63 lelttrd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < B )
65 nncn 
 |-  ( B e. NN -> B e. CC )
66 ax-1cn 
 |-  1 e. CC
67 npcan 
 |-  ( ( B e. CC /\ 1 e. CC ) -> ( ( B - 1 ) + 1 ) = B )
68 65 66 67 sylancl 
 |-  ( B e. NN -> ( ( B - 1 ) + 1 ) = B )
69 68 ad2antlr 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( ( B - 1 ) + 1 ) = B )
70 64 69 breqtrrd 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < ( ( B - 1 ) + 1 ) )
71 12 ad2antlr 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> B e. ZZ )
72 1z 
 |-  1 e. ZZ
73 zsubcl 
 |-  ( ( B e. ZZ /\ 1 e. ZZ ) -> ( B - 1 ) e. ZZ )
74 71 72 73 sylancl 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( B - 1 ) e. ZZ )
75 zleltp1 
 |-  ( ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. ZZ /\ ( B - 1 ) e. ZZ ) -> ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <_ ( B - 1 ) <-> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < ( ( B - 1 ) + 1 ) ) )
76 30 74 75 syl2anc 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <_ ( B - 1 ) <-> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) < ( ( B - 1 ) + 1 ) ) )
77 70 76 mpbird 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <_ ( B - 1 ) )
78 elfz2nn0 
 |-  ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. ( 0 ... ( B - 1 ) ) <-> ( ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. NN0 /\ ( B - 1 ) e. NN0 /\ ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) <_ ( B - 1 ) ) )
79 52 53 77 78 syl3anbrc 
 |-  ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 0 ... B ) ) -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) e. ( 0 ... ( B - 1 ) ) )
80 oveq2 
 |-  ( a = x -> ( A x. a ) = ( A x. x ) )
81 80 oveq1d 
 |-  ( a = x -> ( ( A x. a ) mod 1 ) = ( ( A x. x ) mod 1 ) )
82 81 oveq2d 
 |-  ( a = x -> ( B x. ( ( A x. a ) mod 1 ) ) = ( B x. ( ( A x. x ) mod 1 ) ) )
83 82 fveq2d 
 |-  ( a = x -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) = ( |_ ` ( B x. ( ( A x. x ) mod 1 ) ) ) )
84 oveq2 
 |-  ( a = y -> ( A x. a ) = ( A x. y ) )
85 84 oveq1d 
 |-  ( a = y -> ( ( A x. a ) mod 1 ) = ( ( A x. y ) mod 1 ) )
86 85 oveq2d 
 |-  ( a = y -> ( B x. ( ( A x. a ) mod 1 ) ) = ( B x. ( ( A x. y ) mod 1 ) ) )
87 86 fveq2d 
 |-  ( a = y -> ( |_ ` ( B x. ( ( A x. a ) mod 1 ) ) ) = ( |_ ` ( B x. ( ( A x. y ) mod 1 ) ) ) )
88 6 7 18 79 83 87 fphpdo 
 |-  ( ( 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 ) ) ) ) )