![]() |
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 6788 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 6778 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 6806 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 402 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 6776 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 6804 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 402 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2108 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1390 (class class class)co 5455 ℂcc 6709 0cc0 6711 1c1 6712 ici 6713 + caddc 6714 · cmul 6716 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 ax-1cn 6776 ax-icn 6778 ax-addcl 6779 ax-mulcl 6781 ax-i2m1 6788 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 |
This theorem is referenced by: 0cnd 6818 c0ex 6819 addid2 6949 00id 6951 cnegexlem2 6984 negcl 7008 subid 7026 subid1 7027 neg0 7053 negid 7054 negsub 7055 subneg 7056 negneg 7057 negeq0 7061 negsubdi 7063 renegcl 7068 mul02 7180 mul01 7182 mulneg1 7188 ixi 7367 negap0 7412 muleqadd 7431 divvalap 7435 div0ap 7461 recgt0 7597 0m0e0 7807 2muline0 7927 elznn0 8036 0exp0e1 8914 expeq0 8940 0exp 8944 sq0 8997 cjap0 9135 cjne0 9136 abs0 9222 |
Copyright terms: Public domain | W3C validator |