Metamath Proof Explorer

Theorem efif1olem3

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

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

Proof

Step Hyp Ref Expression
1 efif1o.1 ⊢F=w∈D⟼ei⁢w
2 efif1o.2 ⊢C=abs-11
3 simpr ⊢φ∧x∈C→x∈C
4 3 2 eleqtrdi ⊢φ∧x∈C→x∈abs-11
5 absf ⊢abs:ℂ⟶ℝ
6 ffn ⊢abs:ℂ⟶ℝ→absFnℂ
7 fniniseg ⊢absFnℂ→x∈abs-11↔x∈ℂ∧x=1
8 5 6 7 mp2b ⊢x∈abs-11↔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→x2=x
16 15 fveq2d ⊢φ∧x∈C→x2=x
17 2nn0 ⊢2∈ℕ0
18 absexp ⊢x∈ℂ∧2∈ℕ0→x2=x2
19 11 17 18 sylancl ⊢φ∧x∈C→x2=x2
20 9 simprd ⊢φ∧x∈C→x=1
21 16 19 20 3eqtr3d ⊢φ∧x∈C→x2=1
22 sq1 ⊢12=1
23 21 22 eqtr4di ⊢φ∧x∈C→x2=12
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→x2=12↔x=1
29 26 27 28 mpanr12 ⊢x∈ℝ∧0≤x→x2=12↔x=1
30 24 25 29 syl2anc ⊢φ∧x∈C→x2=12↔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∈−11↔ℑ⁡x∈ℝ∧−1≤ℑ⁡x∧ℑ⁡x≤1
40 12 36 37 39 syl3anbrc ⊢φ∧x∈C→ℑ⁡x∈−11