0cn - Intuitionistic Logic Explorer

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

Theorem 0cn 8099

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 8065	. 2
2		ax-icn 8055	. . . 4
3		mulcl 8087	. . . 4 $/\$
4	2, 2, 3	mp2an 426	. . 3
5		ax-1cn 8053	. . 3
6		addcl 8085	. . 3 $/\$
7	4, 5, 6	mp2an 426	. 2
8	1, 7	eqeltrri 2281	1

Colors of variables: wff set class

Syntax hints:

wcel 2178 (class class class)co 5967

cc 7958

cc0 7960

c1 7961

ci 7962

caddc 7963

cmul 7965

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1471 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-4 1534 ax-17 1550 ax-ial 1558 ax-ext 2189 ax-1cn 8053 ax-icn 8055 ax-addcl 8056 ax-mulcl 8058 ax-i2m1 8065

This theorem depends on definitions: df-bi 117 df-cleq 2200 df-clel 2203

This theorem is referenced by: 0cnd 8100 c0ex 8101 addlid 8246 00id 8248 cnegexlem2 8283 negcl 8307 subid 8326 subid1 8327 neg0 8353 negid 8354 negsub 8355 subneg 8356 negneg 8357 negeq0 8361 negsubdi 8363 renegcl 8368 mul02 8494 mul01 8496 mulneg1 8502 ixi 8691 negap0 8738 muleqadd 8776 divvalap 8782 div0ap 8810 recgt0 8958 0m0e0 9183 2muline0 9297 elznn0 9422 ser0 10715 0exp0e1 10726 expeq0 10752 0exp 10756 sq0 10812 bcval5 10945 shftval3 11253 shftidt2 11258 cjap0 11333 cjne0 11334 abs0 11484 abs2dif 11532 clim0 11711 climz 11718 serclim0 11731 sumrbdclem 11803 fsum3cvg 11804 summodclem3 11806 summodclem2a 11807 fisumss 11818 fsumrelem 11897 ef0 12098 eftlub 12116 sin0 12155 tan0 12157 4sqlem11 12839 cncrng 14446 cnfld0 14448 cnbl0 15121 cnblcld 15122 dvconst 15281 dvconstre 15283 dvconstss 15285 dvcnp2cntop 15286 dvrecap 15300 dveflem 15313 plyun0 15323 plycjlemc 15347 plycj 15348 dvply2g 15353 sinhalfpilem 15378 sin2kpi 15398 cos2kpi 15399 sinkpi 15434 1sgm2ppw 15582 dcapnconst 16202