Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rpcnd | Unicode version |
Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rpred.1 |
Ref | Expression |
---|---|
rpcnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpred.1 | . . 3 | |
2 | 1 | rpred 9476 | . 2 |
3 | 2 | recnd 7787 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 cc 7611 crp 9434 |
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-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-resscn 7705 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-rab 2423 df-in 3072 df-ss 3079 df-rp 9435 |
This theorem is referenced by: rpcnne0d 9486 ltaddrp2d 9511 iccf1o 9780 bcp1nk 10501 bcpasc 10505 cvg1nlemcxze 10747 cvg1nlemres 10750 resqrexlemdec 10776 resqrexlemlo 10778 resqrexlemcalc2 10780 resqrexlemcalc3 10781 resqrexlemnm 10783 resqrexlemcvg 10784 resqrexlemoverl 10786 sqrtdiv 10807 absdivap 10835 bdtrilem 11003 isumrpcl 11256 expcnvap0 11264 absgtap 11272 cvgratz 11294 mertenslemi1 11297 effsumlt 11387 limcimolemlt 12791 trilpolemclim 13218 trilpolemisumle 13220 trilpolemeq1 13222 trilpolemlt1 13223 |
Copyright terms: Public domain | W3C validator |