Metamath Proof Explorer


Theorem efif1olem2

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

Ref Expression
Hypothesis efif1olem1.1 𝐷 = ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) )
Assertion efif1olem2 ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦𝐷 ( ( 𝑧𝑦 ) / ( 2 · π ) ) ∈ ℤ )

Proof

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