![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > recni | GIF version |
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
recni.1 | ⊢ 𝐴 ∈ ℝ |
Ref | Expression |
---|---|
recni | ⊢ 𝐴 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn 7917 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | recni.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
3 | 1, 2 | sselii 3164 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2158 ℂcc 7823 ℝcr 7824 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 ax-resscn 7917 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-in 3147 df-ss 3154 |
This theorem is referenced by: resubcli 8234 ltapii 8606 nncni 8943 2cn 9004 3cn 9008 4cn 9011 5cn 9013 6cn 9015 7cn 9017 8cn 9019 9cn 9021 halfcn 9147 8th4div3 9152 nn0cni 9202 numltc 9423 sqge0i 10621 lt2sqi 10622 le2sqi 10623 sq11i 10624 sqrtmsq2i 11158 0.999... 11543 ef01bndlem 11778 sin4lt0 11788 eirraplem 11798 eirr 11800 egt2lt3 11801 sqrt2irraplemnn 12193 picn 14504 sinhalfpilem 14508 cosneghalfpi 14515 sinhalfpip 14537 sinhalfpim 14538 coshalfpip 14539 coshalfpim 14540 sincosq1sgn 14543 sincosq2sgn 14544 sincosq3sgn 14545 sincosq4sgn 14546 cosq23lt0 14550 coseq00topi 14552 sincosq1eq 14556 sincos4thpi 14557 tan4thpi 14558 sincos6thpi 14559 2logb9irrALT 14688 taupi 15118 |
Copyright terms: Public domain | W3C validator |