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 9653 | . 2 |
3 | 2 | recnd 7948 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2141 cc 7772 crp 9610 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-resscn 7866 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rab 2457 df-in 3127 df-ss 3134 df-rp 9611 |
This theorem is referenced by: rpcnne0d 9663 ltaddrp2d 9688 iccf1o 9961 bcp1nk 10696 bcpasc 10700 cvg1nlemcxze 10946 cvg1nlemres 10949 resqrexlemdec 10975 resqrexlemlo 10977 resqrexlemcalc2 10979 resqrexlemcalc3 10980 resqrexlemnm 10982 resqrexlemcvg 10983 resqrexlemoverl 10985 sqrtdiv 11006 absdivap 11034 bdtrilem 11202 isumrpcl 11457 expcnvap0 11465 absgtap 11473 cvgratz 11495 mertenslemi1 11498 effsumlt 11655 pythagtriplem12 12229 pythagtriplem14 12231 pythagtriplem16 12233 limcimolemlt 13427 rpdivcxp 13626 rpcxple2 13632 rpcxplt2 13633 rpcxpsqrt 13636 rpabscxpbnd 13653 logbgcd1irr 13679 iooref1o 14066 trilpolemclim 14068 trilpolemisumle 14070 trilpolemeq1 14072 trilpolemlt1 14073 |
Copyright terms: Public domain | W3C validator |