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 9850. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 9817 | . 2 class i | |
2 | cc 9813 | . 2 class ℂ | |
3 | 1, 2 | wcel 1977 | 1 wff i ∈ ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: 0cn 9911 mulid1 9916 mul02lem2 10092 mul02 10093 addid1 10095 cnegex 10096 cnegex2 10097 0cnALT 10149 negicn 10161 ine0 10344 ixi 10535 recextlem1 10536 recextlem2 10537 recex 10538 rimul 10888 cru 10889 crne0 10890 cju 10893 it0e0 11131 2mulicn 11132 2muline0 11133 cnref1o 11703 irec 12826 i2 12827 i3 12828 i4 12829 iexpcyc 12831 crreczi 12851 imre 13696 reim 13697 crre 13702 crim 13703 remim 13705 mulre 13709 cjreb 13711 recj 13712 reneg 13713 readd 13714 remullem 13716 imcj 13720 imneg 13721 imadd 13722 cjadd 13729 cjneg 13735 imval2 13739 rei 13744 imi 13745 cji 13747 cjreim 13748 cjreim2 13749 rennim 13827 cnpart 13828 sqrtneglem 13855 sqrtneg 13856 sqrtm1 13864 absi 13874 absreimsq 13880 absreim 13881 absimle 13897 abs1m 13923 sqreulem 13947 sqreu 13948 caucvgr 14254 sinf 14693 cosf 14694 tanval2 14702 tanval3 14703 resinval 14704 recosval 14705 efi4p 14706 resin4p 14707 recos4p 14708 resincl 14709 recoscl 14710 sinneg 14715 cosneg 14716 efival 14721 efmival 14722 sinhval 14723 coshval 14724 retanhcl 14728 tanhlt1 14729 tanhbnd 14730 efeul 14731 sinadd 14733 cosadd 14734 ef01bndlem 14753 sin01bnd 14754 cos01bnd 14755 absef 14766 absefib 14767 efieq1re 14768 demoivre 14769 demoivreALT 14770 nthruc 14819 igz 15476 4sqlem17 15503 cnsubrg 19625 cnrehmeo 22560 cmodscexp 22729 ncvspi 22764 cphipval2 22848 4cphipval2 22849 cphipval 22850 itg0 23352 itgz 23353 itgcl 23356 ibl0 23359 iblcnlem1 23360 itgcnlem 23362 itgneg 23376 iblss 23377 iblss2 23378 itgss 23384 itgeqa 23386 iblconst 23390 itgconst 23391 itgadd 23397 iblabs 23401 iblabsr 23402 iblmulc2 23403 itgmulc2 23406 itgsplit 23408 dvsincos 23548 iaa 23884 sincn 24002 coscn 24003 efhalfpi 24027 ef2kpi 24034 efper 24035 sinperlem 24036 efimpi 24047 pige3 24073 sineq0 24077 efeq1 24079 tanregt0 24089 efif1olem4 24095 efifo 24097 eff1olem 24098 circgrp 24102 circsubm 24103 logneg 24138 logm1 24139 lognegb 24140 eflogeq 24152 efiarg 24157 cosargd 24158 logimul 24164 logneg2 24165 abslogle 24168 tanarg 24169 logcn 24193 logf1o2 24196 cxpsqrtlem 24248 cxpsqrt 24249 root1eq1 24296 cxpeq 24298 ang180lem1 24339 ang180lem2 24340 ang180lem3 24341 ang180lem4 24342 1cubrlem 24368 1cubr 24369 asinlem 24395 asinlem2 24396 asinlem3a 24397 asinlem3 24398 asinf 24399 atandm2 24404 atandm3 24405 atanf 24407 asinneg 24413 efiasin 24415 sinasin 24416 asinsinlem 24418 asinsin 24419 asin1 24421 asinbnd 24426 cosasin 24431 atanneg 24434 atancj 24437 efiatan 24439 atanlogaddlem 24440 atanlogadd 24441 atanlogsublem 24442 atanlogsub 24443 efiatan2 24444 2efiatan 24445 tanatan 24446 cosatan 24448 atantan 24450 atanbndlem 24452 atans2 24458 dvatan 24462 atantayl 24464 atantayl2 24465 log2cnv 24471 basellem3 24609 2sqlem2 24943 nvpi 26906 ipval2 26946 4ipval2 26947 ipval3 26948 ipidsq 26949 dipcl 26951 dipcj 26953 dip0r 26956 dipcn 26959 ip1ilem 27065 ipasslem10 27078 ipasslem11 27079 polid2i 27398 polidi 27399 lnopeq0lem1 28248 lnopeq0i 28250 lnophmlem2 28260 bhmafibid1 28975 cnre2csqima 29285 logi 30873 iexpire 30874 itgaddnc 32640 iblabsnc 32644 iblmulc2nc 32645 itgmulc2nc 32648 ftc1anclem3 32657 ftc1anclem6 32660 ftc1anclem7 32661 ftc1anclem8 32662 ftc1anc 32663 dvasin 32666 areacirclem4 32673 cntotbnd 32765 proot1ex 36798 sineq0ALT 38195 iblsplit 38858 sinh-conventional 42279 |
Copyright terms: Public domain | W3C validator |