MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eulerid Structured version   Visualization version   GIF version

Theorem eulerid 23590
Description: Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
Assertion
Ref Expression
eulerid ((exp‘(i · π)) + 1) = 0

Proof of Theorem eulerid
StepHypRef Expression
1 efipi 23589 . . 3 (exp‘(i · π)) = -1
21oveq1i 6373 . 2 ((exp‘(i · π)) + 1) = (-1 + 1)
3 ax-1cn 9682 . . 3 1 ∈ ℂ
4 neg1cn 10802 . . 3 -1 ∈ ℂ
5 1pneg1e0 10807 . . 3 (1 + -1) = 0
63, 4, 5addcomli 9910 . 2 (-1 + 1) = 0
72, 6eqtri 2527 1 ((exp‘(i · π)) + 1) = 0
Colors of variables: wff setvar class
Syntax hints:   = wceq 1468  cfv 5633  (class class class)co 6363  0cc0 9624  1c1 9625  ici 9626   + caddc 9627   · cmul 9629  -cneg 9948  expce 14274  πcpi 14279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-rep 4548  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-inf2 8231  ax-cnex 9680  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-mulcom 9688  ax-addass 9689  ax-mulass 9690  ax-distr 9691  ax-i2m1 9692  ax-1ne0 9693  ax-1rid 9694  ax-rnegex 9695  ax-rrecex 9696  ax-cnre 9697  ax-pre-lttri 9698  ax-pre-lttrn 9699  ax-pre-ltadd 9700  ax-pre-mulgt0 9701  ax-pre-sup 9702  ax-addf 9703  ax-mulf 9704
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-fal 1474  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-nel 2678  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-int 4265  df-iun 4309  df-iin 4310  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-se 4840  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-isom 5642  df-riota 6325  df-ov 6366  df-oprab 6367  df-mpt2 6368  df-of 6607  df-om 6770  df-1st 6870  df-2nd 6871  df-supp 6994  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-1o 7259  df-2o 7260  df-oadd 7263  df-er 7440  df-map 7557  df-pm 7558  df-ixp 7606  df-en 7653  df-dom 7654  df-sdom 7655  df-fin 7656  df-fsupp 7969  df-fi 8010  df-sup 8041  df-inf 8042  df-oi 8108  df-card 8458  df-cda 8683  df-pnf 9762  df-mnf 9763  df-xr 9764  df-ltxr 9765  df-le 9766  df-sub 9949  df-neg 9950  df-div 10359  df-nn 10699  df-2 10757  df-3 10758  df-4 10759  df-5 10760  df-6 10761  df-7 10762  df-8 10763  df-9 10764  df-10 10765  df-n0 10961  df-z 11029  df-dec 11142  df-uz 11250  df-q 11356  df-rp 11394  df-xneg 11500  df-xadd 11501  df-xmul 11502  df-ioo 11734  df-ioc 11735  df-ico 11736  df-icc 11737  df-fz 11881  df-fzo 12017  df-fl 12136  df-seq 12328  df-exp 12387  df-fac 12574  df-bc 12602  df-hash 12630  df-shft 13290  df-cj 13322  df-re 13323  df-im 13324  df-sqrt 13458  df-abs 13459  df-limsup 13686  df-clim 13712  df-rlim 13713  df-sum 13913  df-ef 14281  df-sin 14283  df-cos 14284  df-pi 14286  df-struct 15284  df-ndx 15285  df-slot 15286  df-base 15287  df-sets 15288  df-ress 15289  df-plusg 15368  df-mulr 15369  df-starv 15370  df-sca 15371  df-vsca 15372  df-ip 15373  df-tset 15374  df-ple 15375  df-ds 15377  df-unif 15378  df-hom 15379  df-cco 15380  df-rest 15486  df-topn 15487  df-0g 15505  df-gsum 15506  df-topgen 15507  df-pt 15508  df-prds 15511  df-xrs 15565  df-qtop 15571  df-imas 15572  df-xps 15575  df-mre 15657  df-mrc 15658  df-acs 15660  df-mgm 16653  df-sgrp 16692  df-mnd 16702  df-submnd 16743  df-mulg 16836  df-cntz 17132  df-cmn 17593  df-psmet 19120  df-xmet 19121  df-met 19122  df-bl 19123  df-mopn 19124  df-fbas 19125  df-fg 19126  df-cnfld 19129  df-top 20079  df-bases 20080  df-topon 20081  df-topsp 20082  df-cld 20191  df-ntr 20192  df-cls 20193  df-nei 20271  df-lp 20309  df-perf 20310  df-cn 20400  df-cnp 20401  df-haus 20488  df-tx 20734  df-hmeo 20927  df-fil 21019  df-fm 21111  df-flim 21112  df-flf 21113  df-xms 21493  df-ms 21494  df-tms 21495  df-cncf 22068  df-limc 22982  df-dv 22983
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator