This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efif1olem1

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

Ref Expression
Hypothesis efif1olem1.1 
|- D = ( A (,] ( A + ( 2 x. _pi ) ) )
Assertion efif1olem1 
|- ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )

Proof

Step Hyp Ref Expression
1 efif1olem1.1 
 |-  D = ( A (,] ( A + ( 2 x. _pi ) ) )
2 simprr 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> y e. D )
3 2 1 eleqtrdi 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> y e. ( A (,] ( A + ( 2 x. _pi ) ) ) )
4 rexr 
 |-  ( A e. RR -> A e. RR* )
5 simpl 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> A e. RR )
6 2re 
 |-  2 e. RR
7 pire 
 |-  _pi e. RR
8 6 7 remulcli 
 |-  ( 2 x. _pi ) e. RR
9 readdcl 
 |-  ( ( A e. RR /\ ( 2 x. _pi ) e. RR ) -> ( A + ( 2 x. _pi ) ) e. RR )
10 5 8 9 sylancl 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( A + ( 2 x. _pi ) ) e. RR )
11 elioc2 
 |-  ( ( A e. RR* /\ ( A + ( 2 x. _pi ) ) e. RR ) -> ( y e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( y e. RR /\ A < y /\ y <_ ( A + ( 2 x. _pi ) ) ) ) )
12 4 10 11 syl2an2r 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( y e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( y e. RR /\ A < y /\ y <_ ( A + ( 2 x. _pi ) ) ) ) )
13 3 12 mpbid 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( y e. RR /\ A < y /\ y <_ ( A + ( 2 x. _pi ) ) ) )
14 13 simp1d 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> y e. RR )
15 simprl 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> x e. D )
16 15 1 eleqtrdi 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> x e. ( A (,] ( A + ( 2 x. _pi ) ) ) )
17 elioc2 
 |-  ( ( A e. RR* /\ ( A + ( 2 x. _pi ) ) e. RR ) -> ( x e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( x e. RR /\ A < x /\ x <_ ( A + ( 2 x. _pi ) ) ) ) )
18 4 10 17 syl2an2r 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( x e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( x e. RR /\ A < x /\ x <_ ( A + ( 2 x. _pi ) ) ) ) )
19 16 18 mpbid 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( x e. RR /\ A < x /\ x <_ ( A + ( 2 x. _pi ) ) ) )
20 19 simp1d 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> x e. RR )
21 readdcl 
 |-  ( ( x e. RR /\ ( 2 x. _pi ) e. RR ) -> ( x + ( 2 x. _pi ) ) e. RR )
22 20 8 21 sylancl 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( x + ( 2 x. _pi ) ) e. RR )
23 13 simp3d 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> y <_ ( A + ( 2 x. _pi ) ) )
24 8 a1i 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( 2 x. _pi ) e. RR )
25 19 simp2d 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> A < x )
26 5 20 24 25 ltadd1dd 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( A + ( 2 x. _pi ) ) < ( x + ( 2 x. _pi ) ) )
27 14 10 22 23 26 lelttrd 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> y < ( x + ( 2 x. _pi ) ) )
28 14 24 20 ltsubaddd 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( ( y - ( 2 x. _pi ) ) < x <-> y < ( x + ( 2 x. _pi ) ) ) )
29 27 28 mpbird 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( y - ( 2 x. _pi ) ) < x )
30 readdcl 
 |-  ( ( y e. RR /\ ( 2 x. _pi ) e. RR ) -> ( y + ( 2 x. _pi ) ) e. RR )
31 14 8 30 sylancl 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( y + ( 2 x. _pi ) ) e. RR )
32 19 simp3d 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> x <_ ( A + ( 2 x. _pi ) ) )
33 13 simp2d 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> A < y )
34 5 14 24 33 ltadd1dd 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( A + ( 2 x. _pi ) ) < ( y + ( 2 x. _pi ) ) )
35 20 10 31 32 34 lelttrd 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> x < ( y + ( 2 x. _pi ) ) )
36 20 14 24 absdifltd 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( ( abs ` ( x - y ) ) < ( 2 x. _pi ) <-> ( ( y - ( 2 x. _pi ) ) < x /\ x < ( y + ( 2 x. _pi ) ) ) ) )
37 29 35 36 mpbir2and 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )