efif1olem1

		Ref	Expression
	Hypothesis	efif1olem1.1	$⊢ D = (A, A + 2 π]$
	Assertion	efif1olem1	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$

Proof

Step	Hyp	Ref	Expression
1		efif1olem1.1	$⊢ D = (A, A + 2 π]$
2		simprr	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y \in D$
3	2 1	eleqtrdi	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y \in (A, A + 2 π]$
4		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
5		simpl	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to A \in ℝ$
6		2re	$⊢ 2 \in ℝ$
7		pire	$⊢ π \in ℝ$
8	6 7	remulcli	$⊢ 2 π \in ℝ$
9		readdcl	$⊢ (A \in ℝ \land 2 π \in ℝ) \to A + 2 π \in ℝ$
10	5 8 9	sylancl	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to A + 2 π \in ℝ$
11		elioc2	$⊢ (A \in ℝ^{*} \land A + 2 π \in ℝ) \to (y \in (A, A + 2 π] \leftrightarrow (y \in ℝ \land A < y \land y \leq A + 2 π))$
12	4 10 11	syl2an2r	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to (y \in (A, A + 2 π] \leftrightarrow (y \in ℝ \land A < y \land y \leq A + 2 π))$
13	3 12	mpbid	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to (y \in ℝ \land A < y \land y \leq A + 2 π)$
14	13	simp1d	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y \in ℝ$
15		simprl	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to x \in D$
16	15 1	eleqtrdi	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to x \in (A, A + 2 π]$
17		elioc2	$⊢ (A \in ℝ^{*} \land A + 2 π \in ℝ) \to (x \in (A, A + 2 π] \leftrightarrow (x \in ℝ \land A < x \land x \leq A + 2 π))$
18	4 10 17	syl2an2r	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to (x \in (A, A + 2 π] \leftrightarrow (x \in ℝ \land A < x \land x \leq A + 2 π))$
19	16 18	mpbid	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to (x \in ℝ \land A < x \land x \leq A + 2 π)$
20	19	simp1d	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to x \in ℝ$
21		readdcl	$⊢ (x \in ℝ \land 2 π \in ℝ) \to x + 2 π \in ℝ$
22	20 8 21	sylancl	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to x + 2 π \in ℝ$
23	13	simp3d	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y \leq A + 2 π$
24	8	a1i	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to 2 π \in ℝ$
25	19	simp2d	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to A < x$
26	5 20 24 25	ltadd1dd	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to A + 2 π < x + 2 π$
27	14 10 22 23 26	lelttrd	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y < x + 2 π$
28	14 24 20	ltsubaddd	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to (y - 2 π < x \leftrightarrow y < x + 2 π)$
29	27 28	mpbird	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y - 2 π < x$
30		readdcl	$⊢ (y \in ℝ \land 2 π \in ℝ) \to y + 2 π \in ℝ$
31	14 8 30	sylancl	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to y + 2 π \in ℝ$
32	19	simp3d	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to x \leq A + 2 π$
33	13	simp2d	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to A < y$
34	5 14 24 33	ltadd1dd	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to A + 2 π < y + 2 π$
35	20 10 31 32 34	lelttrd	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to x < y + 2 π$
36	20 14 24	absdifltd	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to (\|x - y\| < 2 π \leftrightarrow (y - 2 π < x \land x < y + 2 π))$
37	29 35 36	mpbir2and	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$

Metamath Proof Explorer

Theorem efif1olem1

Proof