This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 9-May-2014)
|
|
Ref |
Expression |
|
Assertion |
eulerid |
⊢ ( ( exp ‘ ( i · π ) ) + 1 ) = 0 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
efipi |
⊢ ( exp ‘ ( i · π ) ) = - 1 |
| 2 |
1
|
oveq1i |
⊢ ( ( exp ‘ ( i · π ) ) + 1 ) = ( - 1 + 1 ) |
| 3 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 4 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
| 5 |
|
1pneg1e0 |
⊢ ( 1 + - 1 ) = 0 |
| 6 |
3 4 5
|
addcomli |
⊢ ( - 1 + 1 ) = 0 |
| 7 |
2 6
|
eqtri |
⊢ ( ( exp ‘ ( i · π ) ) + 1 ) = 0 |