Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rpcn | Structured version Visualization version Unicode version |
Description: A positive real is a complex number. (Contributed by NM, 11-Nov-2008.) |
Ref | Expression |
---|---|
rpcn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpre 11839 | . 2 | |
2 | 1 | recnd 10068 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wcel 1990 cc 9934 crp 11832 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-resscn 9993 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-in 3581 df-ss 3588 df-rp 11833 |
This theorem is referenced by: rpcnne0 11850 divge1 11898 ltdifltdiv 12635 modvalr 12671 flpmodeq 12673 mulmod0 12676 negmod0 12677 modlt 12679 moddiffl 12681 modvalp1 12689 modid 12695 modid0 12696 modcyc 12705 modcyc2 12706 modadd1 12707 muladdmodid 12710 modmuladdnn0 12714 negmod 12715 modm1p1mod0 12721 modmul1 12723 2txmodxeq0 12730 2submod 12731 moddi 12738 sqrlem2 13984 sqrtdiv 14006 caurcvgr 14404 o1fsum 14545 divrcnv 14584 efgt1p2 14844 efgt1p 14845 rpmsubg 19810 uniioombl 23357 abelthlem8 24193 reefgim 24204 pilem1 24205 logne0 24326 logneg 24334 advlogexp 24401 logcxp 24415 cxprec 24432 cxpmul 24434 abscxp 24438 logsqrt 24450 dvcxp1 24481 dvcxp2 24482 dvsqrt 24483 cxpcn2 24487 loglesqrt 24499 relogbreexp 24513 relogbzexp 24514 relogbmul 24515 relogbdiv 24517 relogbexp 24518 relogbcxp 24523 relogbcxpb 24525 relogbf 24529 rlimcnp 24692 efrlim 24696 cxplim 24698 sqrtlim 24699 cxploglim 24704 logdifbnd 24720 harmonicbnd4 24737 rpdmgm 24751 logfaclbnd 24947 logexprlim 24950 logfacrlim2 24951 vmadivsum 25171 dchrisum0lem1a 25175 dchrvmasumlema 25189 dchrisum0lem1 25205 dchrisum0lem2 25207 mudivsum 25219 mulogsumlem 25220 logdivsum 25222 selberg2lem 25239 selberg2 25240 pntrmax 25253 selbergr 25257 pntibndlem1 25278 pntlem3 25298 blocnilem 27659 nmcexi 28885 nmcopexi 28886 nmcfnexi 28910 dp20h 29586 dpexpp1 29616 0dp2dp 29617 sqsscirc1 29954 logdivsqrle 30728 taupilem3 33165 taupilem1 33167 poimirlem29 33438 heicant 33444 itg2addnclem3 33463 itg2gt0cn 33465 ftc1anclem6 33490 ftc1anclem8 33492 areacirclem1 33500 areacirclem4 33503 areacirc 33505 isbnd2 33582 cntotbnd 33595 heiborlem6 33615 heiborlem7 33616 irrapxlem5 37390 2timesgt 39500 xralrple2 39570 recnnltrp 39593 rpgtrecnn 39597 rrpsscn 39820 stirlinglem14 40304 fourierdlem73 40396 divge1b 42302 divgt1b 42303 fldivmod 42313 relogbmulbexp 42355 relogbdivb 42356 amgmwlem 42548 |
Copyright terms: Public domain | W3C validator |