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 ) )