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