![]() |
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 10173. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 10140 | . 2 class i | |
2 | cc 10136 | . 2 class ℂ | |
3 | 1, 2 | wcel 2145 | 1 wff i ∈ ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: 0cn 10234 mulid1 10239 mul02lem2 10415 mul02 10416 addid1 10418 cnegex 10419 cnegex2 10420 0cnALT 10472 negicn 10484 ine0 10667 ixi 10858 recextlem1 10859 recextlem2 10860 recex 10861 rimul 11213 cru 11214 crne0 11215 cju 11218 it0e0 11456 2mulicn 11457 2muline0 11458 cnref1o 12030 irec 13171 i2 13172 i3 13173 i4 13174 iexpcyc 13176 crreczi 13196 imre 14056 reim 14057 crre 14062 crim 14063 remim 14065 mulre 14069 cjreb 14071 recj 14072 reneg 14073 readd 14074 remullem 14076 imcj 14080 imneg 14081 imadd 14082 cjadd 14089 cjneg 14095 imval2 14099 rei 14104 imi 14105 cji 14107 cjreim 14108 cjreim2 14109 rennim 14187 cnpart 14188 sqrtneglem 14215 sqrtneg 14216 sqrtm1 14224 absi 14234 absreimsq 14240 absreim 14241 absimle 14257 abs1m 14283 sqreulem 14307 sqreu 14308 caucvgr 14614 sinf 15060 cosf 15061 tanval2 15069 tanval3 15070 resinval 15071 recosval 15072 efi4p 15073 resin4p 15074 recos4p 15075 resincl 15076 recoscl 15077 sinneg 15082 cosneg 15083 efival 15088 efmival 15089 sinhval 15090 coshval 15091 retanhcl 15095 tanhlt1 15096 tanhbnd 15097 efeul 15098 sinadd 15100 cosadd 15101 ef01bndlem 15120 sin01bnd 15121 cos01bnd 15122 absef 15133 absefib 15134 efieq1re 15135 demoivre 15136 demoivreALT 15137 nthruc 15187 igz 15845 4sqlem17 15872 cnsubrg 20021 cnrehmeo 22972 cmodscexp 23140 ncvspi 23175 cphipval2 23259 4cphipval2 23260 cphipval 23261 itg0 23766 itgz 23767 itgcl 23770 ibl0 23773 iblcnlem1 23774 itgcnlem 23776 itgneg 23790 iblss 23791 iblss2 23792 itgss 23798 itgeqa 23800 iblconst 23804 itgconst 23805 itgadd 23811 iblabs 23815 iblabsr 23816 iblmulc2 23817 itgmulc2 23820 itgsplit 23822 dvsincos 23964 iaa 24300 sincn 24418 coscn 24419 efhalfpi 24444 ef2kpi 24451 efper 24452 sinperlem 24453 efimpi 24464 pige3 24490 sineq0 24494 efeq1 24496 tanregt0 24506 efif1olem4 24512 efifo 24514 eff1olem 24515 circgrp 24519 circsubm 24520 logneg 24555 logm1 24556 lognegb 24557 eflogeq 24569 efiarg 24574 cosargd 24575 logimul 24581 logneg2 24582 abslogle 24585 tanarg 24586 logcn 24614 logf1o2 24617 cxpsqrtlem 24669 cxpsqrt 24670 root1eq1 24717 cxpeq 24719 ang180lem1 24760 ang180lem2 24761 ang180lem3 24762 ang180lem4 24763 1cubrlem 24789 1cubr 24790 asinlem 24816 asinlem2 24817 asinlem3a 24818 asinlem3 24819 asinf 24820 atandm2 24825 atandm3 24826 atanf 24828 asinneg 24834 efiasin 24836 sinasin 24837 asinsinlem 24839 asinsin 24840 asin1 24842 asinbnd 24847 cosasin 24852 atanneg 24855 atancj 24858 efiatan 24860 atanlogaddlem 24861 atanlogadd 24862 atanlogsublem 24863 atanlogsub 24864 efiatan2 24865 2efiatan 24866 tanatan 24867 cosatan 24869 atantan 24871 atanbndlem 24873 atans2 24879 dvatan 24883 atantayl 24885 atantayl2 24886 log2cnv 24892 basellem3 25030 2sqlem2 25364 nvpi 27862 ipval2 27902 4ipval2 27903 ipval3 27904 ipidsq 27905 dipcl 27907 dipcj 27909 dip0r 27912 dipcn 27915 ip1ilem 28021 ipasslem10 28034 ipasslem11 28035 polid2i 28354 polidi 28355 lnopeq0lem1 29204 lnopeq0i 29206 lnophmlem2 29216 bhmafibid1 29984 cnre2csqima 30297 efmul2picn 31014 itgexpif 31024 vtscl 31056 vtsprod 31057 circlemeth 31058 logi 31958 iexpire 31959 itgaddnc 33802 iblabsnc 33806 iblmulc2nc 33807 itgmulc2nc 33810 ftc1anclem3 33819 ftc1anclem6 33822 ftc1anclem7 33823 ftc1anclem8 33824 ftc1anc 33825 dvasin 33828 areacirclem4 33835 cntotbnd 33927 proot1ex 38305 sineq0ALT 39695 iblsplit 40699 sinh-conventional 43011 |
Copyright terms: Public domain | W3C validator |