0cn - Intuitionistic Logic Explorer

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

Theorem 0cn 8066

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 8032	. 2
2		ax-icn 8022	. . . 4
3		mulcl 8054	. . . 4 $/\$
4	2, 2, 3	mp2an 426	. . 3
5		ax-1cn 8020	. . 3
6		addcl 8052	. . 3 $/\$
7	4, 5, 6	mp2an 426	. 2
8	1, 7	eqeltrri 2279	1

Colors of variables: wff set class

Syntax hints:

wcel 2176 (class class class)co 5946

cc 7925

cc0 7927

c1 7928

ci 7929

caddc 7930

cmul 7932

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 1470 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-4 1533 ax-17 1549 ax-ial 1557 ax-ext 2187 ax-1cn 8020 ax-icn 8022 ax-addcl 8023 ax-mulcl 8025 ax-i2m1 8032

This theorem depends on definitions: df-bi 117 df-cleq 2198 df-clel 2201

This theorem is referenced by: 0cnd 8067 c0ex 8068 addlid 8213 00id 8215 cnegexlem2 8250 negcl 8274 subid 8293 subid1 8294 neg0 8320 negid 8321 negsub 8322 subneg 8323 negneg 8324 negeq0 8328 negsubdi 8330 renegcl 8335 mul02 8461 mul01 8463 mulneg1 8469 ixi 8658 negap0 8705 muleqadd 8743 divvalap 8749 div0ap 8777 recgt0 8925 0m0e0 9150 2muline0 9264 elznn0 9389 ser0 10680 0exp0e1 10691 expeq0 10717 0exp 10721 sq0 10777 bcval5 10910 shftval3 11171 shftidt2 11176 cjap0 11251 cjne0 11252 abs0 11402 abs2dif 11450 clim0 11629 climz 11636 serclim0 11649 sumrbdclem 11721 fsum3cvg 11722 summodclem3 11724 summodclem2a 11725 fisumss 11736 fsumrelem 11815 ef0 12016 eftlub 12034 sin0 12073 tan0 12075 4sqlem11 12757 cncrng 14364 cnfld0 14366 cnbl0 15039 cnblcld 15040 dvconst 15199 dvconstre 15201 dvconstss 15203 dvcnp2cntop 15204 dvrecap 15218 dveflem 15231 plyun0 15241 plycjlemc 15265 plycj 15266 dvply2g 15271 sinhalfpilem 15296 sin2kpi 15316 cos2kpi 15317 sinkpi 15352 1sgm2ppw 15500 dcapnconst 16037