![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrp | Structured version Visualization version Unicode version |
Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
elrp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 4422 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rp 11337 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | elrab2 3210 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4419 df-rp 11337 |
This theorem is referenced by: elrpii 11339 nnrp 11345 rpgt0 11347 rpregt0 11349 ralrp 11355 rexrp 11356 rpaddcl 11357 rpmulcl 11358 rpdivcl 11359 rpgecl 11362 rphalflt 11363 ge0p1rp 11365 rpneg 11366 negelrp 11367 ltsubrp 11369 ltaddrp 11370 difrp 11371 elrpd 11372 infmrp1 11668 iccdil 11805 icccntr 11807 1mod 12167 expgt0 12343 resqrex 13369 sqrtdiv 13384 sqrtneglem 13385 mulcn2 13714 ef01bndlem 14293 sinltx 14298 met1stc 21591 met2ndci 21592 bcthlem4 22350 itg2mulc 22761 dvferm1 22993 dvne0 23019 reeff1o 23458 ellogdm 23640 cxpge0 23684 cxple2a 23700 cxpcn3lem 23743 cxpaddlelem 23747 cxpaddle 23748 atanbnd 23908 rlimcnp 23947 amgm 23972 chtub 24196 chebbnd1 24366 chto1ub 24370 pntlem3 24503 blocni 26502 dfrp2 28404 heiborlem8 32196 wallispilem4 38031 perfectALTVlem2 38979 regt1loggt0 40716 |
Copyright terms: Public domain | W3C validator |