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 syl6eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑧 − ( ( 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 · π ) ) ∈ ℤ )