![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rpcnd | GIF 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 9513 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | recnd 7818 | 1 ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1481 ℂcc 7642 ℝ+crp 9470 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-resscn 7736 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-rab 2426 df-in 3082 df-ss 3089 df-rp 9471 |
This theorem is referenced by: rpcnne0d 9523 ltaddrp2d 9548 iccf1o 9817 bcp1nk 10540 bcpasc 10544 cvg1nlemcxze 10786 cvg1nlemres 10789 resqrexlemdec 10815 resqrexlemlo 10817 resqrexlemcalc2 10819 resqrexlemcalc3 10820 resqrexlemnm 10822 resqrexlemcvg 10823 resqrexlemoverl 10825 sqrtdiv 10846 absdivap 10874 bdtrilem 11042 isumrpcl 11295 expcnvap0 11303 absgtap 11311 cvgratz 11333 mertenslemi1 11336 effsumlt 11435 limcimolemlt 12841 rpdivcxp 13040 rpcxple2 13046 rpcxplt2 13047 rpcxpsqrt 13050 rpabscxpbnd 13067 logbgcd1irr 13092 trilpolemclim 13404 trilpolemisumle 13406 trilpolemeq1 13408 trilpolemlt1 13409 iooref1o 13426 |
Copyright terms: Public domain | W3C validator |