Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0cn | GIF version |
Description: 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn | ⊢ 0 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 7725 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 7715 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 7747 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 422 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 7713 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 7745 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 422 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2213 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1480 (class class class)co 5774 ℂcc 7618 0cc0 7620 1c1 7621 ici 7622 + caddc 7623 · cmul 7625 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 ax-1cn 7713 ax-icn 7715 ax-addcl 7716 ax-mulcl 7718 ax-i2m1 7725 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 |
This theorem is referenced by: 0cnd 7759 c0ex 7760 addid2 7901 00id 7903 cnegexlem2 7938 negcl 7962 subid 7981 subid1 7982 neg0 8008 negid 8009 negsub 8010 subneg 8011 negneg 8012 negeq0 8016 negsubdi 8018 renegcl 8023 mul02 8149 mul01 8151 mulneg1 8157 ixi 8345 negap0 8392 muleqadd 8429 divvalap 8434 div0ap 8462 recgt0 8608 0m0e0 8832 2muline0 8945 elznn0 9069 ser0 10287 0exp0e1 10298 expeq0 10324 0exp 10328 sq0 10383 bcval5 10509 shftval3 10599 shftidt2 10604 cjap0 10679 cjne0 10680 abs0 10830 abs2dif 10878 clim0 11054 climz 11061 serclim0 11074 sumrbdclem 11146 fsum3cvg 11147 summodclem3 11149 summodclem2a 11150 fisumss 11161 fsumrelem 11240 ef0 11378 eftlub 11396 sin0 11436 tan0 11438 cnbl0 12703 cnblcld 12704 dvconst 12830 dvcnp2cntop 12832 dvrecap 12846 dveflem 12855 sinhalfpilem 12872 sin2kpi 12892 cos2kpi 12893 sinkpi 12928 |
Copyright terms: Public domain | W3C validator |