0cn - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 0cn		Unicode version

Theorem 0cn 7912

Description: 0 is a complex number. (Contributed by NM, 19-Feb-2005.)

**Assertion**
Ref	Expression
0cn

**Proof of Theorem 0cn**
Step	Hyp	Ref	Expression
1		ax-i2m1 7879	. 2
2		ax-icn 7869	. . . 4
3		mulcl 7901	. . . 4 $/\$
4	2, 2, 3	mp2an 424	. . 3
5		ax-1cn 7867	. . 3
6		addcl 7899	. . 3 $/\$
7	4, 5, 6	mp2an 424	. 2
8	1, 7	eqeltrri 2244	1

Colors of variables: wff set class

Syntax hints:

wcel 2141 (class class class)co 5853

cc 7772

cc0 7774

c1 7775

ci 7776

caddc 7777

cmul 7779

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 ax-1cn 7867 ax-icn 7869 ax-addcl 7870 ax-mulcl 7872 ax-i2m1 7879

This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166

This theorem is referenced by: 0cnd 7913 c0ex 7914 addid2 8058 00id 8060 cnegexlem2 8095 negcl 8119 subid 8138 subid1 8139 neg0 8165 negid 8166 negsub 8167 subneg 8168 negneg 8169 negeq0 8173 negsubdi 8175 renegcl 8180 mul02 8306 mul01 8308 mulneg1 8314 ixi 8502 negap0 8549 muleqadd 8586 divvalap 8591 div0ap 8619 recgt0 8766 0m0e0 8990 2muline0 9103 elznn0 9227 ser0 10470 0exp0e1 10481 expeq0 10507 0exp 10511 sq0 10566 bcval5 10697 shftval3 10791 shftidt2 10796 cjap0 10871 cjne0 10872 abs0 11022 abs2dif 11070 clim0 11248 climz 11255 serclim0 11268 sumrbdclem 11340 fsum3cvg 11341 summodclem3 11343 summodclem2a 11344 fisumss 11355 fsumrelem 11434 ef0 11635 eftlub 11653 sin0 11692 tan0 11694 cnbl0 13328 cnblcld 13329 dvconst 13455 dvcnp2cntop 13457 dvrecap 13471 dveflem 13481 sinhalfpilem 13506 sin2kpi 13526 cos2kpi 13527 sinkpi 13562 dcapnconst 14092