efif1olem2

		Ref	Expression
	Hypothesis	efif1olem1.1	$⊢ D = (A, A + 2 π]$
	Assertion	efif1olem2	$⊢ (A \in ℝ \land z \in ℝ) \to \exists y \in D \frac{z - y}{2 π} \in ℤ$

Proof

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

Metamath Proof Explorer

Theorem efif1olem2

Proof