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

Theorem efival 15937
Description: The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
Assertion
Ref Expression
efival (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))

Proof of Theorem efival
StepHypRef Expression
1 ax-icn 11009 . . . . . 6 i ∈ ℂ
2 mulcl 11034 . . . . . 6 ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
31, 2mpan 687 . . . . 5 (𝐴 ∈ ℂ → (i · 𝐴) ∈ ℂ)
4 efcl 15868 . . . . 5 ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
53, 4syl 17 . . . 4 (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
6 negicn 11301 . . . . . 6 -i ∈ ℂ
7 mulcl 11034 . . . . . 6 ((-i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (-i · 𝐴) ∈ ℂ)
86, 7mpan 687 . . . . 5 (𝐴 ∈ ℂ → (-i · 𝐴) ∈ ℂ)
9 efcl 15868 . . . . 5 ((-i · 𝐴) ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
108, 9syl 17 . . . 4 (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
115, 10addcld 11073 . . 3 (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ)
125, 10subcld 11411 . . 3 (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ)
13 2cn 12127 . . . . 5 2 ∈ ℂ
14 2ne0 12156 . . . . 5 2 ≠ 0
1513, 14pm3.2i 471 . . . 4 (2 ∈ ℂ ∧ 2 ≠ 0)
16 divdir 11737 . . . 4 ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ ∧ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) / 2) = ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2)))
1715, 16mp3an3 1449 . . 3 ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ ∧ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ) → ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) / 2) = ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2)))
1811, 12, 17syl2anc 584 . 2 (𝐴 ∈ ℂ → ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) / 2) = ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2)))
1910, 5pncan3d 11414 . . . . . 6 (𝐴 ∈ ℂ → ((exp‘(-i · 𝐴)) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) = (exp‘(i · 𝐴)))
2019oveq2d 7332 . . . . 5 (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) + ((exp‘(-i · 𝐴)) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))))) = ((exp‘(i · 𝐴)) + (exp‘(i · 𝐴))))
215, 10, 12addassd 11076 . . . . 5 (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) = ((exp‘(i · 𝐴)) + ((exp‘(-i · 𝐴)) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))))))
2252timesd 12295 . . . . 5 (𝐴 ∈ ℂ → (2 · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) + (exp‘(i · 𝐴))))
2320, 21, 223eqtr4d 2786 . . . 4 (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) = (2 · (exp‘(i · 𝐴))))
2423oveq1d 7331 . . 3 (𝐴 ∈ ℂ → ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) / 2) = ((2 · (exp‘(i · 𝐴))) / 2))
25 divcan3 11738 . . . . 5 (((exp‘(i · 𝐴)) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (exp‘(i · 𝐴))) / 2) = (exp‘(i · 𝐴)))
2613, 14, 25mp3an23 1452 . . . 4 ((exp‘(i · 𝐴)) ∈ ℂ → ((2 · (exp‘(i · 𝐴))) / 2) = (exp‘(i · 𝐴)))
275, 26syl 17 . . 3 (𝐴 ∈ ℂ → ((2 · (exp‘(i · 𝐴))) / 2) = (exp‘(i · 𝐴)))
2824, 27eqtr2d 2777 . 2 (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴)))) / 2))
29 cosval 15908 . . 3 (𝐴 ∈ ℂ → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2))
30 2mulicn 12275 . . . . . . 7 (2 · i) ∈ ℂ
31 2muline0 12276 . . . . . . 7 (2 · i) ≠ 0
3230, 31pm3.2i 471 . . . . . 6 ((2 · i) ∈ ℂ ∧ (2 · i) ≠ 0)
33 div12 11734 . . . . . 6 ((i ∈ ℂ ∧ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ ∧ ((2 · i) ∈ ℂ ∧ (2 · i) ≠ 0)) → (i · (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 · i))))
341, 32, 33mp3an13 1451 . . . . 5 (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ → (i · (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 · i))))
3512, 34syl 17 . . . 4 (𝐴 ∈ ℂ → (i · (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 · i))))
36 sinval 15907 . . . . 5 (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)))
3736oveq2d 7332 . . . 4 (𝐴 ∈ ℂ → (i · (sin‘𝐴)) = (i · (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))))
38 divrec 11728 . . . . . . 7 ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (1 / 2)))
3913, 14, 38mp3an23 1452 . . . . . 6 (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (1 / 2)))
4012, 39syl 17 . . . . 5 (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (1 / 2)))
411mulid2i 11059 . . . . . . . 8 (1 · i) = i
4241oveq1i 7326 . . . . . . 7 ((1 · i) / (2 · i)) = (i / (2 · i))
43 ine0 11489 . . . . . . . . . . 11 i ≠ 0
441, 43dividi 11787 . . . . . . . . . 10 (i / i) = 1
4544oveq2i 7327 . . . . . . . . 9 ((1 / 2) · (i / i)) = ((1 / 2) · 1)
46 ax-1cn 11008 . . . . . . . . . 10 1 ∈ ℂ
4746, 13, 1, 1, 14, 43divmuldivi 11814 . . . . . . . . 9 ((1 / 2) · (i / i)) = ((1 · i) / (2 · i))
4845, 47eqtr3i 2766 . . . . . . . 8 ((1 / 2) · 1) = ((1 · i) / (2 · i))
49 halfcn 12267 . . . . . . . . 9 (1 / 2) ∈ ℂ
5049mulid1i 11058 . . . . . . . 8 ((1 / 2) · 1) = (1 / 2)
5148, 50eqtr3i 2766 . . . . . . 7 ((1 · i) / (2 · i)) = (1 / 2)
5242, 51eqtr3i 2766 . . . . . 6 (i / (2 · i)) = (1 / 2)
5352oveq2i 7327 . . . . 5 (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 · i))) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (1 / 2))
5440, 53eqtr4di 2794 . . . 4 (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 · i))))
5535, 37, 543eqtr4d 2786 . . 3 (𝐴 ∈ ℂ → (i · (sin‘𝐴)) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2))
5629, 55oveq12d 7334 . 2 (𝐴 ∈ ℂ → ((cos‘𝐴) + (i · (sin‘𝐴))) = ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2)))
5718, 28, 563eqtr4d 2786 1 (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wne 2940  cfv 6465  (class class class)co 7316  cc 10948  0cc0 10950  1c1 10951  ici 10952   + caddc 10953   · cmul 10955  cmin 11284  -cneg 11285   / cdiv 11711  2c2 12107  expce 15847  sincsin 15849  cosccos 15850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-inf2 9476  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027  ax-pre-sup 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-om 7759  df-1st 7877  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-er 8547  df-pm 8667  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-sup 9277  df-inf 9278  df-oi 9345  df-card 9774  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-div 11712  df-nn 12053  df-2 12115  df-3 12116  df-n0 12313  df-z 12399  df-uz 12662  df-rp 12810  df-ico 13164  df-fz 13319  df-fzo 13462  df-fl 13591  df-seq 13801  df-exp 13862  df-fac 14067  df-hash 14124  df-shft 14854  df-cj 14886  df-re 14887  df-im 14888  df-sqrt 15022  df-abs 15023  df-limsup 15256  df-clim 15273  df-rlim 15274  df-sum 15474  df-ef 15853  df-sin 15855  df-cos 15856
This theorem is referenced by:  efmival  15938  efeul  15947  efieq  15948  sinadd  15949  cosadd  15950  absefi  15981  demoivre  15985  efhalfpi  25708  efipi  25710  ef2pi  25714  efimpi  25728  efif1olem4  25781  1cubrlem  26071  asinsin  26122  atantan  26153
  Copyright terms: Public domain W3C validator