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 7836 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | recni.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
3 | 1, 2 | sselii 3134 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2135 ℂcc 7742 ℝcr 7743 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-resscn 7836 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: resubcli 8152 ltapii 8524 nncni 8858 2cn 8919 3cn 8923 4cn 8926 5cn 8928 6cn 8930 7cn 8932 8cn 8934 9cn 8936 halfcn 9062 8th4div3 9067 nn0cni 9117 numltc 9338 sqge0i 10531 lt2sqi 10532 le2sqi 10533 sq11i 10534 sqrtmsq2i 11063 0.999... 11448 ef01bndlem 11683 sin4lt0 11693 eirraplem 11703 eirr 11705 egt2lt3 11706 sqrt2irraplemnn 12090 picn 13255 sinhalfpilem 13259 cosneghalfpi 13266 sinhalfpip 13288 sinhalfpim 13289 coshalfpip 13290 coshalfpim 13291 sincosq1sgn 13294 sincosq2sgn 13295 sincosq3sgn 13296 sincosq4sgn 13297 cosq23lt0 13301 coseq00topi 13303 sincosq1eq 13307 sincos4thpi 13308 tan4thpi 13309 sincos6thpi 13310 2logb9irrALT 13439 taupi 13790 |
Copyright terms: Public domain | W3C validator |