| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 0cn | Structured version Visualization version GIF version | ||
| Description: Zero is a complex number. See also 0cnALT 11496. (Contributed by NM, 19-Feb-2005.) |
| Ref | Expression |
|---|---|
| 0cn | ⊢ 0 ∈ ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-i2m1 11223 | . 2 ⊢ ((i · i) + 1) = 0 | |
| 2 | ax-icn 11214 | . . . 4 ⊢ i ∈ ℂ | |
| 3 | mulcl 11239 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
| 4 | 2, 2, 3 | mp2an 692 | . . 3 ⊢ (i · i) ∈ ℂ |
| 5 | ax-1cn 11213 | . . 3 ⊢ 1 ∈ ℂ | |
| 6 | addcl 11237 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
| 7 | 4, 5, 6 | mp2an 692 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
| 8 | 1, 7 | eqeltrri 2838 | 1 ⊢ 0 ∈ ℂ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 0cc0 11155 1c1 11156 ici 11157 + caddc 11158 · cmul 11160 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-mulcl 11217 ax-i2m1 11223 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: 0cnd 11254 c0ex 11255 1re 11261 00id 11436 mul02lem1 11437 mul02 11439 mul01 11440 addrid 11441 addlid 11444 negcl 11508 subid 11528 subid1 11529 neg0 11555 negid 11556 negsub 11557 subneg 11558 negneg 11559 negeq0 11563 negsubdi 11565 renegcli 11570 mulneg1 11699 msqge0 11784 ixi 11892 muleqadd 11907 diveq0 11932 div0 11955 div0OLD 11956 ofsubge0 12265 0m0e0 12386 nn0sscn 12531 elznn0 12628 ser0 14095 0exp0e1 14107 0exp 14138 sq0 14231 sqeqor 14255 binom2 14256 bcval5 14357 s1co 14872 shftval3 15115 shftidt2 15120 cjne0 15202 sqrt0 15280 abs0 15324 abs00bd 15330 abs2dif 15371 clim0 15542 climz 15585 serclim0 15613 rlimneg 15683 sumrblem 15747 fsumcvg 15748 summolem2a 15751 sumss 15760 fsumss 15761 fsumcvg2 15763 fsumsplit 15777 sumsplit 15804 fsumrelem 15843 fsumrlim 15847 fsumo1 15848 0fallfac 16073 0risefac 16074 binomfallfac 16077 fsumcube 16096 ef0 16127 eftlub 16145 sin0 16185 tan0 16187 divalglem9 16438 sadadd2lem2 16487 sadadd3 16498 bezout 16580 pcmpt2 16931 4sqlem11 16993 ramcl 17067 4001lem2 17179 odadd1 19866 cnaddablx 19886 cnaddabl 19887 cnaddid 19888 frgpnabllem1 19891 cncrng 21401 cncrngOLD 21402 cnfld0 21405 pzriprnglem5 21496 pzriprnglem6 21497 psdmplcl 22166 cnbl0 24794 cnblcld 24795 cnfldnm 24799 cnn0opn 24808 xrge0gsumle 24855 xrge0tsms 24856 cnheibor 24987 cnlmod 25173 csscld 25283 clsocv 25284 cnflduss 25390 cnfldcusp 25391 rrxmvallem 25438 rrxmval 25439 mbfss 25681 mbfmulc2lem 25682 0plef 25707 0pledm 25708 itg1ge0 25721 itg1addlem4 25734 itg2splitlem 25783 itg2addlem 25793 ibl0 25822 iblcnlem 25824 iblss2 25841 itgss3 25850 dvconst 25952 dvcnp2 25955 dvcnp2OLD 25956 dveflem 26017 dv11cn 26040 lhop1lem 26052 plyun0 26236 plyeq0lem 26249 coeeulem 26263 coeeu 26264 coef3 26271 dgrle 26282 0dgrb 26285 coefv0 26287 coemulc 26294 coe1termlem 26297 coe1term 26298 dgr0 26302 dgrmulc 26311 dgrcolem2 26314 vieta1lem2 26353 iaa 26367 aareccl 26368 aalioulem3 26376 taylthlem2 26416 taylthlem2OLD 26417 psercn 26470 pserdvlem2 26472 abelthlem2 26476 abelthlem3 26477 abelthlem5 26479 abelthlem7 26482 abelth 26485 sin2kpi 26525 cos2kpi 26526 sinkpi 26564 efopn 26700 logtayl 26702 cxpval 26706 0cxp 26708 cxpexp 26710 cxpcl 26716 cxpge0 26725 mulcxplem 26726 mulcxp 26727 cxpmul2 26731 dvsqrt 26784 dvcnsqrt 26786 cxpcn3 26791 abscxpbnd 26796 efrlim 27012 efrlimOLD 27013 ftalem2 27117 ftalem3 27118 ftalem4 27119 ftalem5 27120 ftalem7 27122 prmorcht 27221 muinv 27236 1sgm2ppw 27244 logfacbnd3 27267 logexprlim 27269 dchrelbas2 27281 dchrmullid 27296 dchrfi 27299 dchrinv 27305 lgsdir2 27374 lgsdir 27376 addsqnreup 27487 dchrvmasumiflem1 27545 dchrvmasumiflem2 27546 rpvmasum2 27556 log2sumbnd 27588 selberg2lem 27594 logdivbnd 27600 ax5seglem8 28951 axlowdimlem6 28962 axlowdimlem13 28969 ex-co 30457 avril1 30482 vc0 30593 vcz 30594 cnaddabloOLD 30600 cnidOLD 30601 ipasslem8 30856 siilem2 30871 hvmul0 31043 hi01 31115 norm-iii 31159 h1de2ctlem 31574 pjmuli 31708 pjneli 31742 eigre 31854 eigorth 31857 elnlfn 31947 0cnfn 31999 0lnfn 32004 lnopunilem2 32030 xrge0tsmsd 33065 constrsscn 33781 qqh0 33985 qqhcn 33992 eulerpartlemgs2 34382 sgnneg 34543 breprexpnat 34649 hgt750lem2 34667 subfacp1lem6 35190 sinccvglem 35677 abs2sqle 35685 abs2sqlt 35686 tan2h 37619 poimirlem16 37643 poimirlem19 37646 poimirlem31 37658 mblfinlem2 37665 ovoliunnfl 37669 voliunnfl 37671 ftc1anclem5 37704 cntotbnd 37803 60lcm7e420 42011 lcmineqlem10 42039 3lexlogpow5ineq1 42055 sn-1ne2 42300 0tie0 42350 sn-it0e0 42445 addinvcom 42461 sn-0tie0 42469 fltnltalem 42672 flcidc 43182 dvconstbi 44353 expgrowth 44354 dvradcnv2 44366 binomcxplemdvbinom 44372 binomcxplemnotnn0 44375 xralrple3 45385 negcncfg 45896 ioodvbdlimc1 45948 ioodvbdlimc2 45950 itgsinexplem1 45969 stoweidlem26 46041 stoweidlem36 46051 stoweidlem55 46070 stirlinglem8 46096 fourierdlem103 46224 sqwvfoura 46243 sqwvfourb 46244 ovn0lem 46580 nn0sumshdiglemA 48540 nn0sumshdiglemB 48541 nn0sumshdiglem1 48542 sec0 49279 |
| Copyright terms: Public domain | W3C validator |