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 π
Assertion efif1olem2 A z y D z y 2 π

Proof

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