Metamath Proof Explorer

Theorem efif1olem3

Description: Lemma for efif1o . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses efif1o.1 ⊢ F = w ∈ D ⟼ e i ⁢ w
efif1o.2 ⊢ C = abs -1 1
Assertion efif1olem3 ⊢ φ ∧ x ∈ C → ℑ ⁡ x ∈ − 1 1

Proof

Step Hyp Ref Expression
1 efif1o.1 ⊢ F = w ∈ D ⟼ e i ⁢ w
2 efif1o.2 ⊢ C = abs -1 1
3 simpr ⊢ φ ∧ x ∈ C → x ∈ C
4 3 2 eleqtrdi ⊢ φ ∧ x ∈ C → x ∈ abs -1 1
5 absf ⊢ abs : ℂ ⟶ ℝ
6 ffn ⊢ abs : ℂ ⟶ ℝ → abs Fn ℂ
7 fniniseg ⊢ abs Fn ℂ → x ∈ abs -1 1 ↔ x ∈ ℂ ∧ x = 1
8 5 6 7 mp2b ⊢ x ∈ abs -1 1 ↔ x ∈ ℂ ∧ x = 1
9 4 8 sylib ⊢ φ ∧ x ∈ C → x ∈ ℂ ∧ x = 1
10 9 simpld ⊢ φ ∧ x ∈ C → x ∈ ℂ
11 10 sqrtcld ⊢ φ ∧ x ∈ C → x ∈ ℂ
12 11 imcld ⊢ φ ∧ x ∈ C → ℑ ⁡ x ∈ ℝ
13 absimle ⊢ x ∈ ℂ → ℑ ⁡ x ≤ x
14 11 13 syl ⊢ φ ∧ x ∈ C → ℑ ⁡ x ≤ x
15 10 sqsqrtd ⊢ φ ∧ x ∈ C → x 2 = x
16 15 fveq2d ⊢ φ ∧ x ∈ C → x 2 = x
17 2nn0 ⊢ 2 ∈ ℕ 0
18 absexp ⊢ x ∈ ℂ ∧ 2 ∈ ℕ 0 → x 2 = x 2
19 11 17 18 sylancl ⊢ φ ∧ x ∈ C → x 2 = x 2
20 9 simprd ⊢ φ ∧ x ∈ C → x = 1
21 16 19 20 3eqtr3d ⊢ φ ∧ x ∈ C → x 2 = 1
22 sq1 ⊢ 1 2 = 1
23 21 22 syl6eqr ⊢ φ ∧ x ∈ C → x 2 = 1 2
24 11 abscld ⊢ φ ∧ x ∈ C → x ∈ ℝ
25 11 absge0d ⊢ φ ∧ x ∈ C → 0 ≤ x
26 1re ⊢ 1 ∈ ℝ
27 0le1 ⊢ 0 ≤ 1
28 sq11 ⊢ x ∈ ℝ ∧ 0 ≤ x ∧ 1 ∈ ℝ ∧ 0 ≤ 1 → x 2 = 1 2 ↔ x = 1
29 26 27 28 mpanr12 ⊢ x ∈ ℝ ∧ 0 ≤ x → x 2 = 1 2 ↔ x = 1
30 24 25 29 syl2anc ⊢ φ ∧ x ∈ C → x 2 = 1 2 ↔ x = 1
31 23 30 mpbid ⊢ φ ∧ x ∈ C → x = 1
32 14 31 breqtrd ⊢ φ ∧ x ∈ C → ℑ ⁡ x ≤ 1
33 absle ⊢ ℑ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ → ℑ ⁡ x ≤ 1 ↔ − 1 ≤ ℑ ⁡ x ∧ ℑ ⁡ x ≤ 1
34 12 26 33 sylancl ⊢ φ ∧ x ∈ C → ℑ ⁡ x ≤ 1 ↔ − 1 ≤ ℑ ⁡ x ∧ ℑ ⁡ x ≤ 1
35 32 34 mpbid ⊢ φ ∧ x ∈ C → − 1 ≤ ℑ ⁡ x ∧ ℑ ⁡ x ≤ 1
36 35 simpld ⊢ φ ∧ x ∈ C → − 1 ≤ ℑ ⁡ x
37 35 simprd ⊢ φ ∧ x ∈ C → ℑ ⁡ x ≤ 1
38 neg1rr ⊢ − 1 ∈ ℝ
39 38 26 elicc2i ⊢ ℑ ⁡ x ∈ − 1 1 ↔ ℑ ⁡ x ∈ ℝ ∧ − 1 ≤ ℑ ⁡ x ∧ ℑ ⁡ x ≤ 1
40 12 36 37 39 syl3anbrc ⊢ φ ∧ x ∈ C → ℑ ⁡ x ∈ − 1 1