![]() |
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 7749 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-icn 7739 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | mulcl 7771 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 2, 3 | mp2an 423 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | ax-1cn 7737 |
. . 3
![]() ![]() ![]() ![]() | |
6 | addcl 7769 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | mp2an 423 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | eqeltrri 2214 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 ax-1cn 7737 ax-icn 7739 ax-addcl 7740 ax-mulcl 7742 ax-i2m1 7749 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 |
This theorem is referenced by: 0cnd 7783 c0ex 7784 addid2 7925 00id 7927 cnegexlem2 7962 negcl 7986 subid 8005 subid1 8006 neg0 8032 negid 8033 negsub 8034 subneg 8035 negneg 8036 negeq0 8040 negsubdi 8042 renegcl 8047 mul02 8173 mul01 8175 mulneg1 8181 ixi 8369 negap0 8416 muleqadd 8453 divvalap 8458 div0ap 8486 recgt0 8632 0m0e0 8856 2muline0 8969 elznn0 9093 ser0 10318 0exp0e1 10329 expeq0 10355 0exp 10359 sq0 10414 bcval5 10541 shftval3 10631 shftidt2 10636 cjap0 10711 cjne0 10712 abs0 10862 abs2dif 10910 clim0 11086 climz 11093 serclim0 11106 sumrbdclem 11178 fsum3cvg 11179 summodclem3 11181 summodclem2a 11182 fisumss 11193 fsumrelem 11272 ef0 11415 eftlub 11433 sin0 11472 tan0 11474 cnbl0 12742 cnblcld 12743 dvconst 12869 dvcnp2cntop 12871 dvrecap 12885 dveflem 12895 sinhalfpilem 12920 sin2kpi 12940 cos2kpi 12941 sinkpi 12976 |
Copyright terms: Public domain | W3C validator |