Metamath Proof Explorer

Theorem efif1olem1

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

Ref Expression
Hypothesis efif1olem1.1 ⊢ 𝐷 = ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) )
Assertion efif1olem1 ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )

Proof

Step Hyp Ref Expression
1 efif1olem1.1 ⊢ 𝐷 = ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) )
2 simprr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ∈ 𝐷 )
3 2 1 eleqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) )
4 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
5 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝐴 ∈ ℝ )
6 2re ⊢ 2 ∈ ℝ
7 pire ⊢ π ∈ ℝ
8 6 7 remulcli ⊢ ( 2 · π ) ∈ ℝ
9 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ ) → ( 𝐴 + ( 2 · π ) ) ∈ ℝ )
10 5 8 9 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝐴 + ( 2 · π ) ) ∈ ℝ )
11 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 + ( 2 · π ) ) ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 ≤ ( 𝐴 + ( 2 · π ) ) ) ) )
12 4 10 11 syl2an2r ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑦 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 ≤ ( 𝐴 + ( 2 · π ) ) ) ) )
13 3 12 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 ≤ ( 𝐴 + ( 2 · π ) ) ) )
14 13 simp1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ∈ ℝ )
15 simprl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ∈ 𝐷 )
16 15 1 eleqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) )
17 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 + ( 2 · π ) ) ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) ) ) )
18 4 10 17 syl2an2r ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) ) ) )
19 16 18 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) ) )
20 19 simp1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ∈ ℝ )
21 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ ) → ( 𝑥 + ( 2 · π ) ) ∈ ℝ )
22 20 8 21 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 + ( 2 · π ) ) ∈ ℝ )
23 13 simp3d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ≤ ( 𝐴 + ( 2 · π ) ) )
24 8 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 2 · π ) ∈ ℝ )
25 19 simp2d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝐴 < 𝑥 )
26 5 20 24 25 ltadd1dd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝐴 + ( 2 · π ) ) < ( 𝑥 + ( 2 · π ) ) )
27 14 10 22 23 26 lelttrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 < ( 𝑥 + ( 2 · π ) ) )
28 14 24 20 ltsubaddd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( 𝑦 − ( 2 · π ) ) < 𝑥 ↔ 𝑦 < ( 𝑥 + ( 2 · π ) ) ) )
29 27 28 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑦 − ( 2 · π ) ) < 𝑥 )
30 readdcl ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ ) → ( 𝑦 + ( 2 · π ) ) ∈ ℝ )
31 14 8 30 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑦 + ( 2 · π ) ) ∈ ℝ )
32 19 simp3d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) )
33 13 simp2d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝐴 < 𝑦 )
34 5 14 24 33 ltadd1dd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝐴 + ( 2 · π ) ) < ( 𝑦 + ( 2 · π ) ) )
35 20 10 31 32 34 lelttrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 < ( 𝑦 + ( 2 · π ) ) )
36 20 14 24 absdifltd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) ↔ ( ( 𝑦 − ( 2 · π ) ) < 𝑥 ∧ 𝑥 < ( 𝑦 + ( 2 · π ) ) ) ) )
37 29 35 36 mpbir2and ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )