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 )