Theorem absefi

Description: The absolute value of the exponential of an imaginary number is one. Equation 48 of Rudin p. 167. (Contributed by Jason Orendorff, 9-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		efival	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
4	3	fveq2d	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( abs ‘ ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ) )
5		recoscl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
6		resincl	⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) ∈ ℝ )
7		absreim	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ∈ ℝ ) → ( abs ‘ ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ) = ( √ ‘ ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
8	5 6 7	syl2anc	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ) = ( √ ‘ ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
9	5	resqcld	⊢ ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
10	9	recnd	⊢ ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
11	6	resqcld	⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
12	11	recnd	⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
13	10 12	addcomd	⊢ ( 𝐴 ∈ ℝ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
14		sincossq	⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
15	1 14	syl	⊢ ( 𝐴 ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
16	13 15	eqtrd	⊢ ( 𝐴 ∈ ℝ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = 1 )
17	16	fveq2d	⊢ ( 𝐴 ∈ ℝ → ( √ ‘ ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) = ( √ ‘ 1 ) )
18		sqrt1	⊢ ( √ ‘ 1 ) = 1
19	17 18	eqtrdi	⊢ ( 𝐴 ∈ ℝ → ( √ ‘ ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) = 1 )
20	8 19	eqtrd	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ) = 1 )
21	4 20	eqtrd	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 )