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 9598 | . 2 |
3 | 2 | recnd 7901 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2128 cc 7725 crp 9555 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 ax-resscn 7819 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-rab 2444 df-in 3108 df-ss 3115 df-rp 9556 |
This theorem is referenced by: rpcnne0d 9608 ltaddrp2d 9633 iccf1o 9903 bcp1nk 10631 bcpasc 10635 cvg1nlemcxze 10877 cvg1nlemres 10880 resqrexlemdec 10906 resqrexlemlo 10908 resqrexlemcalc2 10910 resqrexlemcalc3 10911 resqrexlemnm 10913 resqrexlemcvg 10914 resqrexlemoverl 10916 sqrtdiv 10937 absdivap 10965 bdtrilem 11133 isumrpcl 11386 expcnvap0 11394 absgtap 11402 cvgratz 11424 mertenslemi1 11427 effsumlt 11584 limcimolemlt 13020 rpdivcxp 13219 rpcxple2 13225 rpcxplt2 13226 rpcxpsqrt 13229 rpabscxpbnd 13246 logbgcd1irr 13271 iooref1o 13592 trilpolemclim 13594 trilpolemisumle 13596 trilpolemeq1 13598 trilpolemlt1 13599 |
Copyright terms: Public domain | W3C validator |