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 · π ) ) ∈ ℤ )