![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > recni | Unicode 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 7358 |
. 2
![]() ![]() ![]() ![]() | |
2 | recni.1 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | sselii 3009 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-11 1440 ax-4 1443 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-resscn 7358 |
This theorem depends on definitions: df-bi 115 df-nf 1393 df-sb 1690 df-clab 2072 df-cleq 2078 df-clel 2081 df-in 2992 df-ss 2999 |
This theorem is referenced by: resubcli 7666 ltapii 8028 nncni 8344 2cn 8405 3cn 8409 4cn 8412 5cn 8414 6cn 8416 7cn 8418 8cn 8420 9cn 8422 halfcn 8540 8th4div3 8545 nn0cni 8595 numltc 8811 sqge0i 9892 lt2sqi 9893 le2sqi 9894 sq11i 9895 sqrtmsq2i 10409 sqrt2irraplemnn 10951 |
Copyright terms: Public domain | W3C validator |