Metamath Proof Explorer

Theorem efif1olem2

Description: Lemma for efif1o . (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Hypothesis efif1olem1.1 
|- D = ( A (,] ( A + ( 2 x. _pi ) ) )
Assertion efif1olem2 
|- ( ( A e. RR /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 efif1olem1.1 
 |-  D = ( A (,] ( A + ( 2 x. _pi ) ) )
2 simpl 
 |-  ( ( A e. RR /\ z e. RR ) -> A e. RR )
3 2re 
 |-  2 e. RR
4 pire 
 |-  _pi e. RR
5 3 4 remulcli 
 |-  ( 2 x. _pi ) e. RR
6 readdcl 
 |-  ( ( A e. RR /\ ( 2 x. _pi ) e. RR ) -> ( A + ( 2 x. _pi ) ) e. RR )
7 2 5 6 sylancl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( A + ( 2 x. _pi ) ) e. RR )
8 resubcl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( A - z ) e. RR )
9 2pos 
 |-  0 < 2
10 pipos 
 |-  0 < _pi
11 3 4 9 10 mulgt0ii 
 |-  0 < ( 2 x. _pi )
12 5 11 elrpii 
 |-  ( 2 x. _pi ) e. RR+
13 modcl 
 |-  ( ( ( A - z ) e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( A - z ) mod ( 2 x. _pi ) ) e. RR )
14 8 12 13 sylancl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A - z ) mod ( 2 x. _pi ) ) e. RR )
15 7 14 resubcld 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. RR )
16 5 a1i 
 |-  ( ( A e. RR /\ z e. RR ) -> ( 2 x. _pi ) e. RR )
17 modlt 
 |-  ( ( ( A - z ) e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( A - z ) mod ( 2 x. _pi ) ) < ( 2 x. _pi ) )
18 8 12 17 sylancl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A - z ) mod ( 2 x. _pi ) ) < ( 2 x. _pi ) )
19 14 16 2 18 ltadd2dd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( A + ( ( A - z ) mod ( 2 x. _pi ) ) ) < ( A + ( 2 x. _pi ) ) )
20 2 14 7 ltaddsubd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( ( A - z ) mod ( 2 x. _pi ) ) ) < ( A + ( 2 x. _pi ) ) <-> A < ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) )
21 19 20 mpbid 
 |-  ( ( A e. RR /\ z e. RR ) -> A < ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) )
22 modge0 
 |-  ( ( ( A - z ) e. RR /\ ( 2 x. _pi ) e. RR+ ) -> 0 <_ ( ( A - z ) mod ( 2 x. _pi ) ) )
23 8 12 22 sylancl 
 |-  ( ( A e. RR /\ z e. RR ) -> 0 <_ ( ( A - z ) mod ( 2 x. _pi ) ) )
24 7 14 subge02d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( 0 <_ ( ( A - z ) mod ( 2 x. _pi ) ) <-> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) <_ ( A + ( 2 x. _pi ) ) ) )
25 23 24 mpbid 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) <_ ( A + ( 2 x. _pi ) ) )
26 rexr 
 |-  ( A e. RR -> A e. RR* )
27 elioc2 
 |-  ( ( A e. RR* /\ ( A + ( 2 x. _pi ) ) e. RR ) -> ( ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. RR /\ A < ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) /\ ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) <_ ( A + ( 2 x. _pi ) ) ) ) )
28 26 7 27 syl2an2r 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. RR /\ A < ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) /\ ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) <_ ( A + ( 2 x. _pi ) ) ) ) )
29 15 21 25 28 mpbir3and 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. ( A (,] ( A + ( 2 x. _pi ) ) ) )
30 29 1 eleqtrrdi 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. D )
31 modval 
 |-  ( ( ( A - z ) e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( A - z ) mod ( 2 x. _pi ) ) = ( ( A - z ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
32 8 12 31 sylancl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A - z ) mod ( 2 x. _pi ) ) = ( ( A - z ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
33 32 oveq2d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) = ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) ) )
34 7 recnd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( A + ( 2 x. _pi ) ) e. CC )
35 8 recnd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( A - z ) e. CC )
36 5 11 gt0ne0ii 
 |-  ( 2 x. _pi ) =/= 0
37 redivcl 
 |-  ( ( ( A - z ) e. RR /\ ( 2 x. _pi ) e. RR /\ ( 2 x. _pi ) =/= 0 ) -> ( ( A - z ) / ( 2 x. _pi ) ) e. RR )
38 5 36 37 mp3an23 
 |-  ( ( A - z ) e. RR -> ( ( A - z ) / ( 2 x. _pi ) ) e. RR )
39 8 38 syl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A - z ) / ( 2 x. _pi ) ) e. RR )
40 39 flcld 
 |-  ( ( A e. RR /\ z e. RR ) -> ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) e. ZZ )
41 40 zred 
 |-  ( ( A e. RR /\ z e. RR ) -> ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) e. RR )
42 remulcl 
 |-  ( ( ( 2 x. _pi ) e. RR /\ ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) e. RR ) -> ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. RR )
43 5 41 42 sylancr 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. RR )
44 43 recnd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. CC )
45 34 35 44 subsubd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) ) = ( ( ( A + ( 2 x. _pi ) ) - ( A - z ) ) + ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
46 2 recnd 
 |-  ( ( A e. RR /\ z e. RR ) -> A e. CC )
47 5 recni 
 |-  ( 2 x. _pi ) e. CC
48 47 a1i 
 |-  ( ( A e. RR /\ z e. RR ) -> ( 2 x. _pi ) e. CC )
49 simpr 
 |-  ( ( A e. RR /\ z e. RR ) -> z e. RR )
50 49 recnd 
 |-  ( ( A e. RR /\ z e. RR ) -> z e. CC )
51 46 48 50 pnncand 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( A - z ) ) = ( ( 2 x. _pi ) + z ) )
52 51 oveq1d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( ( A + ( 2 x. _pi ) ) - ( A - z ) ) + ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) = ( ( ( 2 x. _pi ) + z ) + ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
53 33 45 52 3eqtrd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) = ( ( ( 2 x. _pi ) + z ) + ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
54 53 oveq2d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) = ( z - ( ( ( 2 x. _pi ) + z ) + ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) ) )
55 addcl 
 |-  ( ( ( 2 x. _pi ) e. CC /\ z e. CC ) -> ( ( 2 x. _pi ) + z ) e. CC )
56 47 50 55 sylancr 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( 2 x. _pi ) + z ) e. CC )
57 50 56 44 subsub4d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( z - ( ( 2 x. _pi ) + z ) ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) = ( z - ( ( ( 2 x. _pi ) + z ) + ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) ) )
58 56 50 negsubdi2d 
 |-  ( ( A e. RR /\ z e. RR ) -> -u ( ( ( 2 x. _pi ) + z ) - z ) = ( z - ( ( 2 x. _pi ) + z ) ) )
59 48 50 pncand 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( ( 2 x. _pi ) + z ) - z ) = ( 2 x. _pi ) )
60 59 negeqd 
 |-  ( ( A e. RR /\ z e. RR ) -> -u ( ( ( 2 x. _pi ) + z ) - z ) = -u ( 2 x. _pi ) )
61 58 60 eqtr3d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( z - ( ( 2 x. _pi ) + z ) ) = -u ( 2 x. _pi ) )
62 neg1cn 
 |-  -u 1 e. CC
63 47 mulm1i 
 |-  ( -u 1 x. ( 2 x. _pi ) ) = -u ( 2 x. _pi )
64 62 47 63 mulcomli 
 |-  ( ( 2 x. _pi ) x. -u 1 ) = -u ( 2 x. _pi )
65 61 64 eqtr4di 
 |-  ( ( A e. RR /\ z e. RR ) -> ( z - ( ( 2 x. _pi ) + z ) ) = ( ( 2 x. _pi ) x. -u 1 ) )
66 65 oveq1d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( z - ( ( 2 x. _pi ) + z ) ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) = ( ( ( 2 x. _pi ) x. -u 1 ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
67 62 a1i 
 |-  ( ( A e. RR /\ z e. RR ) -> -u 1 e. CC )
68 40 zcnd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) e. CC )
69 48 67 68 subdid 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) = ( ( ( 2 x. _pi ) x. -u 1 ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
70 66 69 eqtr4d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( z - ( ( 2 x. _pi ) + z ) ) - ( ( 2 x. _pi ) x. ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) = ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
71 54 57 70 3eqtr2d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) = ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) )
72 71 oveq1d 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) / ( 2 x. _pi ) ) = ( ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) / ( 2 x. _pi ) ) )
73 neg1z 
 |-  -u 1 e. ZZ
74 zsubcl 
 |-  ( ( -u 1 e. ZZ /\ ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) e. ZZ ) -> ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. ZZ )
75 73 40 74 sylancr 
 |-  ( ( A e. RR /\ z e. RR ) -> ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. ZZ )
76 75 zcnd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. CC )
77 divcan3 
 |-  ( ( ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. CC /\ ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) -> ( ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) / ( 2 x. _pi ) ) = ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) )
78 47 36 77 mp3an23 
 |-  ( ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) e. CC -> ( ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) / ( 2 x. _pi ) ) = ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) )
79 76 78 syl 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( ( 2 x. _pi ) x. ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) ) / ( 2 x. _pi ) ) = ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) )
80 72 79 eqtrd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) / ( 2 x. _pi ) ) = ( -u 1 - ( |_ ` ( ( A - z ) / ( 2 x. _pi ) ) ) ) )
81 80 75 eqeltrd 
 |-  ( ( A e. RR /\ z e. RR ) -> ( ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) / ( 2 x. _pi ) ) e. ZZ )
82 oveq2 
 |-  ( y = ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) -> ( z - y ) = ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) )
83 82 oveq1d 
 |-  ( y = ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) -> ( ( z - y ) / ( 2 x. _pi ) ) = ( ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) / ( 2 x. _pi ) ) )
84 83 eleq1d 
 |-  ( y = ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) -> ( ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ <-> ( ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) / ( 2 x. _pi ) ) e. ZZ ) )
85 84 rspcev 
 |-  ( ( ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) e. D /\ ( ( z - ( ( A + ( 2 x. _pi ) ) - ( ( A - z ) mod ( 2 x. _pi ) ) ) ) / ( 2 x. _pi ) ) e. ZZ ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
86 30 81 85 syl2anc 
 |-  ( ( A e. RR /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )