![]() |
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 7511 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-icn 7501 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | mulcl 7530 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 2, 3 | mp2an 418 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | ax-1cn 7499 |
. . 3
![]() ![]() ![]() ![]() | |
6 | addcl 7528 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | mp2an 418 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | eqeltrri 2162 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 ax-ext 2071 ax-1cn 7499 ax-icn 7501 ax-addcl 7502 ax-mulcl 7504 ax-i2m1 7511 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 df-clel 2085 |
This theorem is referenced by: 0cnd 7542 c0ex 7543 addid2 7682 00id 7684 cnegexlem2 7719 negcl 7743 subid 7762 subid1 7763 neg0 7789 negid 7790 negsub 7791 subneg 7792 negneg 7793 negeq0 7797 negsubdi 7799 renegcl 7804 mul02 7926 mul01 7928 mulneg1 7934 ixi 8121 negap0 8167 muleqadd 8198 divvalap 8202 div0ap 8230 recgt0 8372 0m0e0 8595 2muline0 8702 elznn0 8826 iser0 10008 ser0 10010 0exp0e1 10021 expeq0 10047 0exp 10051 sq0 10106 ibcval5 10232 shftval3 10322 shftidt2 10327 cjap0 10402 cjne0 10403 abs0 10552 abs00 10558 abs2dif 10600 clim0 10734 climz 10741 serclim0 10754 iserclim0 10755 isumrblem 10826 fisumcvg 10827 fsum3cvg 10828 isummolem3 10831 isummolem2a 10832 fisumss 10845 fsumrelem 10926 ef0 11023 eftlub 11041 sin0 11081 tan0 11083 |
Copyright terms: Public domain | W3C validator |