Theorem absefib

Description: A complex number is real iff the exponential of its product with _i has absolute value one. (Contributed by NM, 21-Aug-2008)

	Ref	Expression
Assertion	absefib	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		ef0	⊢ ( exp ‘ 0 ) = 1
2	1	eqeq2i	⊢ ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 )
3		imcl	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
4	3	renegcld	⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ 𝐴 ) ∈ ℝ )
5		0re	⊢ 0 ∈ ℝ
6		reef11	⊢ ( ( - ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
7	4 5 6	sylancl	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
8	2 7	bitr3id	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
9	3	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
10	9	negeq0d	⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) = 0 ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
11	8 10	bitr4d	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
12		ax-icn	⊢ i ∈ ℂ
13		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
14	12 13	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
15		absef	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) )
16	14 15	syl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) )
17		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
18	17	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
19		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
20	12 9 19	sylancr	⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
21		replim	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
22	18 20 21	comraddd	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) )
23	22	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) = ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) )
24		adddi	⊢ ( ( i ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) = ( ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
25	12 20 18 24	mp3an2i	⊢ ( 𝐴 ∈ ℂ → ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) = ( ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
26		ixi	⊢ ( i · i ) = - 1
27	26	oveq1i	⊢ ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( - 1 · ( ℑ ‘ 𝐴 ) )
28		mulass	⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) )
29	12 12 9 28	mp3an12i	⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) )
30	9	mulm1d	⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( ℑ ‘ 𝐴 ) ) = - ( ℑ ‘ 𝐴 ) )
31	27 29 30	3eqtr3a	⊢ ( 𝐴 ∈ ℂ → ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) = - ( ℑ ‘ 𝐴 ) )
32	31	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) + ( i · ( ℜ ‘ 𝐴 ) ) ) = ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
33	25 32	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) = ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
34	23 33	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) = ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
35	34	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) ) )
36	4 17	crred	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) ) = - ( ℑ ‘ 𝐴 ) )
37	35 36	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( i · 𝐴 ) ) = - ( ℑ ‘ 𝐴 ) )
38	37	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) = ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
39	16 38	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
40	39	eqeq1d	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 ↔ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 ) )
41		reim0b	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
42	11 40 41	3bitr4rd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 ) )