0cn - Intuitionistic Logic Explorer

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

Theorem 0cn 7979

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 7946	. 2
2		ax-icn 7936	. . . 4
3		mulcl 7968	. . . 4 $/\$
4	2, 2, 3	mp2an 426	. . 3
5		ax-1cn 7934	. . 3
6		addcl 7966	. . 3 $/\$
7	4, 5, 6	mp2an 426	. 2
8	1, 7	eqeltrri 2263	1

Colors of variables: wff set class

Syntax hints:

wcel 2160 (class class class)co 5896

cc 7839

cc0 7841

c1 7842

ci 7843

caddc 7844

cmul 7846

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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 ax-1cn 7934 ax-icn 7936 ax-addcl 7937 ax-mulcl 7939 ax-i2m1 7946

This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185

This theorem is referenced by: 0cnd 7980 c0ex 7981 addlid 8126 00id 8128 cnegexlem2 8163 negcl 8187 subid 8206 subid1 8207 neg0 8233 negid 8234 negsub 8235 subneg 8236 negneg 8237 negeq0 8241 negsubdi 8243 renegcl 8248 mul02 8374 mul01 8376 mulneg1 8382 ixi 8570 negap0 8617 muleqadd 8655 divvalap 8661 div0ap 8689 recgt0 8837 0m0e0 9061 2muline0 9174 elznn0 9298 ser0 10545 0exp0e1 10556 expeq0 10582 0exp 10586 sq0 10642 bcval5 10775 shftval3 10868 shftidt2 10873 cjap0 10948 cjne0 10949 abs0 11099 abs2dif 11147 clim0 11325 climz 11332 serclim0 11345 sumrbdclem 11417 fsum3cvg 11418 summodclem3 11420 summodclem2a 11421 fisumss 11432 fsumrelem 11511 ef0 11712 eftlub 11730 sin0 11769 tan0 11771 4sqlem11 12433 cncrng 13872 cnfld0 13874 cnbl0 14491 cnblcld 14492 dvconst 14618 dvcnp2cntop 14620 dvrecap 14634 dveflem 14644 sinhalfpilem 14669 sin2kpi 14689 cos2kpi 14690 sinkpi 14725 dcapnconst 15268