Metamath Proof Explorer


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 )