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 6989 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 6979 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 7008 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 402 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 6977 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 7006 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 402 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2111 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 0cc0 6889 1c1 6890 ici 6891 + caddc 6892 · cmul 6894 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 ax-1cn 6977 ax-icn 6979 ax-addcl 6980 ax-mulcl 6982 ax-i2m1 6989 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-clel 2036 |
This theorem is referenced by: 0cnd 7020 c0ex 7021 addid2 7152 00id 7154 cnegexlem2 7187 negcl 7211 subid 7230 subid1 7231 neg0 7257 negid 7258 negsub 7259 subneg 7260 negneg 7261 negeq0 7265 negsubdi 7267 renegcl 7272 mul02 7384 mul01 7386 mulneg1 7392 ixi 7574 negap0 7620 muleqadd 7649 divvalap 7653 div0ap 7679 recgt0 7816 0m0e0 8029 2muline0 8150 elznn0 8260 iser0 9250 0exp0e1 9260 expeq0 9286 0exp 9290 sq0 9344 shftval3 9428 shftidt2 9433 cjap0 9507 cjne0 9508 abs0 9656 abs00 9662 abs2dif 9702 clim0 9806 climz 9813 iserclim0 9826 |
Copyright terms: Public domain | W3C validator |