![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elrpd | GIF version |
Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
elrpd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
elrpd.2 | ⊢ (𝜑 → 0 < 𝐴) |
Ref | Expression |
---|---|
elrpd | ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrpd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | elrpd.2 | . 2 ⊢ (𝜑 → 0 < 𝐴) | |
3 | elrp 9721 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
4 | 1, 2, 3 | sylanbrc 417 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2164 class class class wbr 4029 ℝcr 7871 0cc0 7872 < clt 8054 ℝ+crp 9719 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-rab 2481 df-v 2762 df-un 3157 df-sn 3624 df-pr 3625 df-op 3627 df-br 4030 df-rp 9720 |
This theorem is referenced by: mul2lt0rgt0 9826 mul2lt0np 9829 zltaddlt1le 10073 modqval 10395 ltexp2a 10662 leexp2a 10663 expnlbnd2 10736 nn0ltexp2 10780 resqrexlem1arp 11149 resqrexlemp1rp 11150 resqrexlemcalc2 11159 resqrexlemcalc3 11160 resqrexlemgt0 11164 resqrexlemglsq 11166 rpsqrtcl 11185 absrpclap 11205 rpmaxcl 11367 rpmincl 11381 xrminrpcl 11417 xrbdtri 11419 mulcn2 11455 reccn2ap 11456 climge0 11468 divcnv 11640 georeclim 11656 cvgratnnlembern 11666 cvgratnnlemsumlt 11671 cvgratnnlemfm 11672 cvgratnnlemrate 11673 cvgratnn 11674 cvgratz 11675 rpefcl 11828 efltim 11841 ef01bndlem 11899 pythagtriplem12 12413 pythagtriplem14 12415 pythagtriplem16 12417 bdmopn 14672 mulcncflem 14761 ivthinclemlopn 14790 ivthinclemuopn 14792 dveflem 14872 reeff1olem 14906 pilem3 14918 tanrpcl 14972 cosordlem 14984 rplogcl 15014 logdivlti 15016 cxplt 15050 cxple 15051 rpabscxpbnd 15073 ltexp2 15074 iooref1o 15524 |
Copyright terms: Public domain | W3C validator |