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 7866 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 7856 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 7888 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 424 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 7854 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 7886 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 424 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2244 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2141 (class class class)co 5850 ℂcc 7759 0cc0 7761 1c1 7762 ici 7763 + caddc 7764 · cmul 7766 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 ax-1cn 7854 ax-icn 7856 ax-addcl 7857 ax-mulcl 7859 ax-i2m1 7866 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 |
This theorem is referenced by: 0cnd 7900 c0ex 7901 addid2 8045 00id 8047 cnegexlem2 8082 negcl 8106 subid 8125 subid1 8126 neg0 8152 negid 8153 negsub 8154 subneg 8155 negneg 8156 negeq0 8160 negsubdi 8162 renegcl 8167 mul02 8293 mul01 8295 mulneg1 8301 ixi 8489 negap0 8536 muleqadd 8573 divvalap 8578 div0ap 8606 recgt0 8753 0m0e0 8977 2muline0 9090 elznn0 9214 ser0 10457 0exp0e1 10468 expeq0 10494 0exp 10498 sq0 10553 bcval5 10684 shftval3 10778 shftidt2 10783 cjap0 10858 cjne0 10859 abs0 11009 abs2dif 11057 clim0 11235 climz 11242 serclim0 11255 sumrbdclem 11327 fsum3cvg 11328 summodclem3 11330 summodclem2a 11331 fisumss 11342 fsumrelem 11421 ef0 11622 eftlub 11640 sin0 11679 tan0 11681 cnbl0 13287 cnblcld 13288 dvconst 13414 dvcnp2cntop 13416 dvrecap 13430 dveflem 13440 sinhalfpilem 13465 sin2kpi 13485 cos2kpi 13486 sinkpi 13521 dcapnconst 14052 |
Copyright terms: Public domain | W3C validator |