0cn - Intuitionistic Logic Explorer

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

Theorem 0cn 8064

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 8030	. 2
2		ax-icn 8020	. . . 4
3		mulcl 8052	. . . 4 $/\$
4	2, 2, 3	mp2an 426	. . 3
5		ax-1cn 8018	. . 3
6		addcl 8050	. . 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 5944

cc 7923

cc0 7925

c1 7926

ci 7927

caddc 7928

cmul 7930

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 8018 ax-icn 8020 ax-addcl 8021 ax-mulcl 8023 ax-i2m1 8030

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

This theorem is referenced by: 0cnd 8065 c0ex 8066 addlid 8211 00id 8213 cnegexlem2 8248 negcl 8272 subid 8291 subid1 8292 neg0 8318 negid 8319 negsub 8320 subneg 8321 negneg 8322 negeq0 8326 negsubdi 8328 renegcl 8333 mul02 8459 mul01 8461 mulneg1 8467 ixi 8656 negap0 8703 muleqadd 8741 divvalap 8747 div0ap 8775 recgt0 8923 0m0e0 9148 2muline0 9262 elznn0 9387 ser0 10678 0exp0e1 10689 expeq0 10715 0exp 10719 sq0 10775 bcval5 10908 shftval3 11138 shftidt2 11143 cjap0 11218 cjne0 11219 abs0 11369 abs2dif 11417 clim0 11596 climz 11603 serclim0 11616 sumrbdclem 11688 fsum3cvg 11689 summodclem3 11691 summodclem2a 11692 fisumss 11703 fsumrelem 11782 ef0 11983 eftlub 12001 sin0 12040 tan0 12042 4sqlem11 12724 cncrng 14331 cnfld0 14333 cnbl0 15006 cnblcld 15007 dvconst 15166 dvconstre 15168 dvconstss 15170 dvcnp2cntop 15171 dvrecap 15185 dveflem 15198 plyun0 15208 plycjlemc 15232 plycj 15233 dvply2g 15238 sinhalfpilem 15263 sin2kpi 15283 cos2kpi 15284 sinkpi 15319 1sgm2ppw 15467 dcapnconst 16000