Metamath Proof Explorer

Theorem efif1olem2

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

Ref Expression
Hypothesis efif1olem1.1 ⊢D=AA+2⁢π
Assertion efif1olem2 ⊢A∈ℝ∧z∈ℝ→∃y∈Dz−y2⁢π∈ℤ

Proof

Step Hyp Ref Expression
1 efif1olem1.1 ⊢D=AA+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−zmod2⁢π∈ℝ
14 8 12 13 sylancl ⊢A∈ℝ∧z∈ℝ→A−zmod2⁢π∈ℝ
15 7 14 resubcld ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π∈ℝ
16 5 a1i ⊢A∈ℝ∧z∈ℝ→2⁢π∈ℝ
17 modlt ⊢A−z∈ℝ∧2⁢π∈ℝ+→A−zmod2⁢π<2⁢π
18 8 12 17 sylancl ⊢A∈ℝ∧z∈ℝ→A−zmod2⁢π<2⁢π
19 14 16 2 18 ltadd2dd ⊢A∈ℝ∧z∈ℝ→A+A−zmod2⁢π<A+2⁢π
20 2 14 7 ltaddsubd ⊢A∈ℝ∧z∈ℝ→A+A−zmod2⁢π<A+2⁢π↔A<A+2⁢π-A−zmod2⁢π
21 19 20 mpbid ⊢A∈ℝ∧z∈ℝ→A<A+2⁢π-A−zmod2⁢π
22 modge0 ⊢A−z∈ℝ∧2⁢π∈ℝ+→0≤A−zmod2⁢π
23 8 12 22 sylancl ⊢A∈ℝ∧z∈ℝ→0≤A−zmod2⁢π
24 7 14 subge02d ⊢A∈ℝ∧z∈ℝ→0≤A−zmod2⁢π↔A+2⁢π-A−zmod2⁢π≤A+2⁢π
25 23 24 mpbid ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π≤A+2⁢π
26 rexr ⊢A∈ℝ→A∈ℝ*
27 elioc2 ⊢A∈ℝ*∧A+2⁢π∈ℝ→A+2⁢π-A−zmod2⁢π∈AA+2⁢π↔A+2⁢π-A−zmod2⁢π∈ℝ∧A<A+2⁢π-A−zmod2⁢π∧A+2⁢π-A−zmod2⁢π≤A+2⁢π
28 26 7 27 syl2an2r ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π∈AA+2⁢π↔A+2⁢π-A−zmod2⁢π∈ℝ∧A<A+2⁢π-A−zmod2⁢π∧A+2⁢π-A−zmod2⁢π≤A+2⁢π
29 15 21 25 28 mpbir3and ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π∈AA+2⁢π
30 29 1 eleqtrrdi ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π∈D
31 modval ⊢A−z∈ℝ∧2⁢π∈ℝ+→A−zmod2⁢π=A-z-2⁢π⁢A−z2⁢π
32 8 12 31 sylancl ⊢A∈ℝ∧z∈ℝ→A−zmod2⁢π=A-z-2⁢π⁢A−z2⁢π
33 32 oveq2d ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π=A+2⁢π-A-z-2⁢π⁢A−z2⁢π
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−z2⁢π∈ℝ
38 5 36 37 mp3an23 ⊢A−z∈ℝ→A−z2⁢π∈ℝ
39 8 38 syl ⊢A∈ℝ∧z∈ℝ→A−z2⁢π∈ℝ
40 39 flcld ⊢A∈ℝ∧z∈ℝ→A−z2⁢π∈ℤ
41 40 zred ⊢A∈ℝ∧z∈ℝ→A−z2⁢π∈ℝ
42 remulcl ⊢2⁢π∈ℝ∧A−z2⁢π∈ℝ→2⁢π⁢A−z2⁢π∈ℝ
43 5 41 42 sylancr ⊢A∈ℝ∧z∈ℝ→2⁢π⁢A−z2⁢π∈ℝ
44 43 recnd ⊢A∈ℝ∧z∈ℝ→2⁢π⁢A−z2⁢π∈ℂ
45 34 35 44 subsubd ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A-z-2⁢π⁢A−z2⁢π=A+2⁢π-A−z+2⁢π⁢A−z2⁢π
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−z2⁢π=2⁢π+z+2⁢π⁢A−z2⁢π
53 33 45 52 3eqtrd ⊢A∈ℝ∧z∈ℝ→A+2⁢π-A−zmod2⁢π=2⁢π+z+2⁢π⁢A−z2⁢π
54 53 oveq2d ⊢A∈ℝ∧z∈ℝ→z−A+2⁢π-A−zmod2⁢π=z−2⁢π+z+2⁢π⁢A−z2⁢π
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−z2⁢π=z−2⁢π+z+2⁢π⁢A−z2⁢π
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−z2⁢π=2⁢π⁢-1−2⁢π⁢A−z2⁢π
67 62 a1i ⊢A∈ℝ∧z∈ℝ→−1∈ℂ
68 40 zcnd ⊢A∈ℝ∧z∈ℝ→A−z2⁢π∈ℂ
69 48 67 68 subdid ⊢A∈ℝ∧z∈ℝ→2⁢π⁢-1-A−z2⁢π=2⁢π⁢-1−2⁢π⁢A−z2⁢π
70 66 69 eqtr4d ⊢A∈ℝ∧z∈ℝ→z-2⁢π+z-2⁢π⁢A−z2⁢π=2⁢π⁢-1-A−z2⁢π
71 54 57 70 3eqtr2d ⊢A∈ℝ∧z∈ℝ→z−A+2⁢π-A−zmod2⁢π=2⁢π⁢-1-A−z2⁢π
72 71 oveq1d ⊢A∈ℝ∧z∈ℝ→z−A+2⁢π-A−zmod2⁢π2⁢π=2⁢π⁢-1-A−z2⁢π2⁢π
73 neg1z ⊢−1∈ℤ
74 zsubcl ⊢−1∈ℤ∧A−z2⁢π∈ℤ→-1-A−z2⁢π∈ℤ
75 73 40 74 sylancr ⊢A∈ℝ∧z∈ℝ→-1-A−z2⁢π∈ℤ
76 75 zcnd ⊢A∈ℝ∧z∈ℝ→-1-A−z2⁢π∈ℂ
77 divcan3 ⊢-1-A−z2⁢π∈ℂ∧2⁢π∈ℂ∧2⁢π≠0→2⁢π⁢-1-A−z2⁢π2⁢π=-1-A−z2⁢π
78 47 36 77 mp3an23 ⊢-1-A−z2⁢π∈ℂ→2⁢π⁢-1-A−z2⁢π2⁢π=-1-A−z2⁢π
79 76 78 syl ⊢A∈ℝ∧z∈ℝ→2⁢π⁢-1-A−z2⁢π2⁢π=-1-A−z2⁢π
80 72 79 eqtrd ⊢A∈ℝ∧z∈ℝ→z−A+2⁢π-A−zmod2⁢π2⁢π=-1-A−z2⁢π
81 80 75 eqeltrd ⊢A∈ℝ∧z∈ℝ→z−A+2⁢π-A−zmod2⁢π2⁢π∈ℤ
82 oveq2 ⊢y=A+2⁢π-A−zmod2⁢π→z−y=z−A+2⁢π-A−zmod2⁢π
83 82 oveq1d ⊢y=A+2⁢π-A−zmod2⁢π→z−y2⁢π=z−A+2⁢π-A−zmod2⁢π2⁢π
84 83 eleq1d ⊢y=A+2⁢π-A−zmod2⁢π→z−y2⁢π∈ℤ↔z−A+2⁢π-A−zmod2⁢π2⁢π∈ℤ
85 84 rspcev ⊢A+2⁢π-A−zmod2⁢π∈D∧z−A+2⁢π-A−zmod2⁢π2⁢π∈ℤ→∃y∈Dz−y2⁢π∈ℤ
86 30 81 85 syl2anc ⊢A∈ℝ∧z∈ℝ→∃y∈Dz−y2⁢π∈ℤ