This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efhalfpi

Description: The exponential of _ipi / 2 is i . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion efhalfpi ( exp ‘ ( i · ( π / 2 ) ) ) = i

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 halfcl ⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
3 efival ⊢ ( ( π / 2 ) ∈ ℂ → ( exp ‘ ( i · ( π / 2 ) ) ) = ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) ) )
4 1 2 3 mp2b ⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) )
5 coshalfpi ⊢ ( cos ‘ ( π / 2 ) ) = 0
6 sinhalfpi ⊢ ( sin ‘ ( π / 2 ) ) = 1
7 6 oveq2i ⊢ ( i · ( sin ‘ ( π / 2 ) ) ) = ( i · 1 )
8 ax-icn ⊢ i ∈ ℂ
9 8 mulridi ⊢ ( i · 1 ) = i
10 7 9 eqtri ⊢ ( i · ( sin ‘ ( π / 2 ) ) ) = i
11 5 10 oveq12i ⊢ ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) ) = ( 0 + i )
12 8 addlidi ⊢ ( 0 + i ) = i
13 11 12 eqtri ⊢ ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) ) = i
14 4 13 eqtri ⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = i