![]() |
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 7631 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | recni.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
3 | 1, 2 | sselii 3058 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1461 ℂcc 7539 ℝcr 7540 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-11 1465 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-resscn 7631 |
This theorem depends on definitions: df-bi 116 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-in 3041 df-ss 3048 |
This theorem is referenced by: resubcli 7942 ltapii 8308 nncni 8634 2cn 8695 3cn 8699 4cn 8702 5cn 8704 6cn 8706 7cn 8708 8cn 8710 9cn 8712 halfcn 8832 8th4div3 8837 nn0cni 8887 numltc 9105 sqge0i 10266 lt2sqi 10267 le2sqi 10268 sq11i 10269 sqrtmsq2i 10793 0.999... 11176 ef01bndlem 11308 sin4lt0 11318 eirraplem 11325 eirr 11327 egt2lt3 11328 sqrt2irraplemnn 11696 |
Copyright terms: Public domain | W3C validator |