![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0cn | Unicode version |
Description: 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 7894 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-icn 7884 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | mulcl 7916 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 2, 3 | mp2an 426 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | ax-1cn 7882 |
. . 3
![]() ![]() ![]() ![]() | |
6 | addcl 7914 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | mp2an 426 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | eqeltrri 2251 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1cn 7882 ax-icn 7884 ax-addcl 7885 ax-mulcl 7887 ax-i2m1 7894 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: 0cnd 7928 c0ex 7929 addid2 8073 00id 8075 cnegexlem2 8110 negcl 8134 subid 8153 subid1 8154 neg0 8180 negid 8181 negsub 8182 subneg 8183 negneg 8184 negeq0 8188 negsubdi 8190 renegcl 8195 mul02 8321 mul01 8323 mulneg1 8329 ixi 8517 negap0 8564 muleqadd 8601 divvalap 8607 div0ap 8635 recgt0 8783 0m0e0 9007 2muline0 9120 elznn0 9244 ser0 10487 0exp0e1 10498 expeq0 10524 0exp 10528 sq0 10583 bcval5 10714 shftval3 10807 shftidt2 10812 cjap0 10887 cjne0 10888 abs0 11038 abs2dif 11086 clim0 11264 climz 11271 serclim0 11284 sumrbdclem 11356 fsum3cvg 11357 summodclem3 11359 summodclem2a 11360 fisumss 11371 fsumrelem 11450 ef0 11651 eftlub 11669 sin0 11708 tan0 11710 cnbl0 13667 cnblcld 13668 dvconst 13794 dvcnp2cntop 13796 dvrecap 13810 dveflem 13820 sinhalfpilem 13845 sin2kpi 13865 cos2kpi 13866 sinkpi 13901 dcapnconst 14431 |
Copyright terms: Public domain | W3C validator |