This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efif1olem3

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

Ref Expression
Hypotheses efif1o.1 ⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
efif1o.2 ⊢ 𝐶 = ( ◡ abs “ { 1 } )
Assertion efif1olem3 ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 efif1o.1 ⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
2 efif1o.2 ⊢ 𝐶 = ( ◡ abs “ { 1 } )
3 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
4 3 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( ◡ abs “ { 1 } ) )
5 absf ⊢ abs : ℂ ⟶ ℝ
6 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
7 fniniseg ⊢ ( abs Fn ℂ → ( 𝑥 ∈ ( ◡ abs “ { 1 } ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 1 ) ) )
8 5 6 7 mp2b ⊢ ( 𝑥 ∈ ( ◡ abs “ { 1 } ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 1 ) )
9 4 8 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 1 ) )
10 9 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℂ )
11 10 sqrtcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( √ ‘ 𝑥 ) ∈ ℂ )
12 11 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ )
13 absimle ⊢ ( ( √ ‘ 𝑥 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( √ ‘ 𝑥 ) ) )
14 11 13 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( √ ‘ 𝑥 ) ) )
15 10 sqsqrtd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 )
16 15 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( abs ‘ 𝑥 ) )
17 2nn0 ⊢ 2 ∈ ℕ0
18 absexp ⊢ ( ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( abs ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
19 11 17 18 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
20 9 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ 𝑥 ) = 1 )
21 16 19 20 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = 1 )
22 sq1 ⊢ ( 1 ↑ 2 ) = 1
23 21 22 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
24 11 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ )
25 11 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 0 ≤ ( abs ‘ ( √ ‘ 𝑥 ) ) )
26 1re ⊢ 1 ∈ ℝ
27 0le1 ⊢ 0 ≤ 1
28 sq11 ⊢ ( ( ( ( abs ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( √ ‘ 𝑥 ) ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( abs ‘ ( √ ‘ 𝑥 ) ) = 1 ) )
29 26 27 28 mpanr12 ⊢ ( ( ( abs ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( √ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( abs ‘ ( √ ‘ 𝑥 ) ) = 1 ) )
30 24 25 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( abs ‘ ( √ ‘ 𝑥 ) ) = 1 ) )
31 23 30 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( √ ‘ 𝑥 ) ) = 1 )
32 14 31 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ≤ 1 )
33 absle ⊢ ( ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ≤ 1 ↔ ( - 1 ≤ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ≤ 1 ) ) )
34 12 26 33 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( abs ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ≤ 1 ↔ ( - 1 ≤ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ≤ 1 ) ) )
35 32 34 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( - 1 ≤ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ≤ 1 ) )
36 35 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → - 1 ≤ ( ℑ ‘ ( √ ‘ 𝑥 ) ) )
37 35 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℑ ‘ ( √ ‘ 𝑥 ) ) ≤ 1 )
38 neg1rr ⊢ - 1 ∈ ℝ
39 38 26 elicc2i ⊢ ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) ↔ ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ ∧ - 1 ≤ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ≤ 1 ) )
40 12 36 37 39 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) )