![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rpred | Unicode version |
Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rpred.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rpred |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpssre 9053 |
. 2
![]() ![]() ![]() ![]() | |
2 | rpred.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sseldi 3010 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 |
This theorem depends on definitions: df-bi 115 df-nf 1393 df-sb 1690 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-rab 2364 df-in 2992 df-ss 2999 df-rp 9044 |
This theorem is referenced by: rpxrd 9083 rpcnd 9084 rpregt0d 9089 rprege0d 9090 rprene0d 9091 rprecred 9094 ltmulgt11d 9118 ltmulgt12d 9119 gt0divd 9120 ge0divd 9121 lediv12ad 9142 ltexp2a 9858 leexp2a 9859 expnlbnd2 9928 cvg1nlemcxze 10256 cvg1nlemcau 10258 cvg1nlemres 10259 cvg1n 10260 resqrexlemp1rp 10280 resqrexlemfp1 10283 resqrexlemover 10284 resqrexlemdec 10285 resqrexlemdecn 10286 resqrexlemlo 10287 resqrexlemcalc1 10288 resqrexlemcalc2 10289 resqrexlemcalc3 10290 resqrexlemnmsq 10291 resqrexlemnm 10292 resqrexlemcvg 10293 resqrexlemgt0 10294 resqrexlemoverl 10295 resqrexlemglsq 10296 resqrexlemga 10297 cau3lem 10388 addcn2 10537 mulcn2 10539 climrecvg1n 10573 climcvg1nlem 10574 qdencn 11271 |
Copyright terms: Public domain | W3C validator |