![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax-icn | Structured version Visualization version GIF version |
Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 10009. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 9976 | . 2 class i | |
2 | cc 9972 | . 2 class ℂ | |
3 | 1, 2 | wcel 2030 | 1 wff i ∈ ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: 0cn 10070 mulid1 10075 mul02lem2 10251 mul02 10252 addid1 10254 cnegex 10255 cnegex2 10256 0cnALT 10308 negicn 10320 ine0 10503 ixi 10694 recextlem1 10695 recextlem2 10696 recex 10697 rimul 11049 cru 11050 crne0 11051 cju 11054 it0e0 11292 2mulicn 11293 2muline0 11294 cnref1o 11865 irec 13004 i2 13005 i3 13006 i4 13007 iexpcyc 13009 crreczi 13029 imre 13892 reim 13893 crre 13898 crim 13899 remim 13901 mulre 13905 cjreb 13907 recj 13908 reneg 13909 readd 13910 remullem 13912 imcj 13916 imneg 13917 imadd 13918 cjadd 13925 cjneg 13931 imval2 13935 rei 13940 imi 13941 cji 13943 cjreim 13944 cjreim2 13945 rennim 14023 cnpart 14024 sqrtneglem 14051 sqrtneg 14052 sqrtm1 14060 absi 14070 absreimsq 14076 absreim 14077 absimle 14093 abs1m 14119 sqreulem 14143 sqreu 14144 caucvgr 14450 sinf 14898 cosf 14899 tanval2 14907 tanval3 14908 resinval 14909 recosval 14910 efi4p 14911 resin4p 14912 recos4p 14913 resincl 14914 recoscl 14915 sinneg 14920 cosneg 14921 efival 14926 efmival 14927 sinhval 14928 coshval 14929 retanhcl 14933 tanhlt1 14934 tanhbnd 14935 efeul 14936 sinadd 14938 cosadd 14939 ef01bndlem 14958 sin01bnd 14959 cos01bnd 14960 absef 14971 absefib 14972 efieq1re 14973 demoivre 14974 demoivreALT 14975 nthruc 15025 igz 15685 4sqlem17 15712 cnsubrg 19854 cnrehmeo 22799 cmodscexp 22967 ncvspi 23002 cphipval2 23086 4cphipval2 23087 cphipval 23088 itg0 23591 itgz 23592 itgcl 23595 ibl0 23598 iblcnlem1 23599 itgcnlem 23601 itgneg 23615 iblss 23616 iblss2 23617 itgss 23623 itgeqa 23625 iblconst 23629 itgconst 23630 itgadd 23636 iblabs 23640 iblabsr 23641 iblmulc2 23642 itgmulc2 23645 itgsplit 23647 dvsincos 23789 iaa 24125 sincn 24243 coscn 24244 efhalfpi 24268 ef2kpi 24275 efper 24276 sinperlem 24277 efimpi 24288 pige3 24314 sineq0 24318 efeq1 24320 tanregt0 24330 efif1olem4 24336 efifo 24338 eff1olem 24339 circgrp 24343 circsubm 24344 logneg 24379 logm1 24380 lognegb 24381 eflogeq 24393 efiarg 24398 cosargd 24399 logimul 24405 logneg2 24406 abslogle 24409 tanarg 24410 logcn 24438 logf1o2 24441 cxpsqrtlem 24493 cxpsqrt 24494 root1eq1 24541 cxpeq 24543 ang180lem1 24584 ang180lem2 24585 ang180lem3 24586 ang180lem4 24587 1cubrlem 24613 1cubr 24614 asinlem 24640 asinlem2 24641 asinlem3a 24642 asinlem3 24643 asinf 24644 atandm2 24649 atandm3 24650 atanf 24652 asinneg 24658 efiasin 24660 sinasin 24661 asinsinlem 24663 asinsin 24664 asin1 24666 asinbnd 24671 cosasin 24676 atanneg 24679 atancj 24682 efiatan 24684 atanlogaddlem 24685 atanlogadd 24686 atanlogsublem 24687 atanlogsub 24688 efiatan2 24689 2efiatan 24690 tanatan 24691 cosatan 24693 atantan 24695 atanbndlem 24697 atans2 24703 dvatan 24707 atantayl 24709 atantayl2 24710 log2cnv 24716 basellem3 24854 2sqlem2 25188 nvpi 27650 ipval2 27690 4ipval2 27691 ipval3 27692 ipidsq 27693 dipcl 27695 dipcj 27697 dip0r 27700 dipcn 27703 ip1ilem 27809 ipasslem10 27822 ipasslem11 27823 polid2i 28142 polidi 28143 lnopeq0lem1 28992 lnopeq0i 28994 lnophmlem2 29004 bhmafibid1 29772 cnre2csqima 30085 efmul2picn 30802 itgexpif 30812 vtscl 30844 vtsprod 30845 circlemeth 30846 logi 31746 iexpire 31747 itgaddnc 33600 iblabsnc 33604 iblmulc2nc 33605 itgmulc2nc 33608 ftc1anclem3 33617 ftc1anclem6 33620 ftc1anclem7 33621 ftc1anclem8 33622 ftc1anc 33623 dvasin 33626 areacirclem4 33633 cntotbnd 33725 proot1ex 38096 sineq0ALT 39487 iblsplit 40500 sinh-conventional 42808 |
Copyright terms: Public domain | W3C validator |