![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reelprrecn | Structured version Visualization version Unicode version |
Description: Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
reelprrecn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reex 9655 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | prid1 4092 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-cnex 9620 ax-resscn 9621 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-un 3420 df-in 3422 df-ss 3429 df-sn 3980 df-pr 3982 |
This theorem is referenced by: dvf 22910 dvmptcj 22970 dvmptre 22971 dvmptim 22972 rolle 22990 cmvth 22991 mvth 22992 dvlip 22993 dvlipcn 22994 dvle 23007 dvivthlem1 23008 dvivth 23010 lhop2 23015 dvcnvre 23019 dvfsumle 23021 dvfsumge 23022 dvfsumabs 23023 dvfsumlem2 23027 dvfsum2 23034 ftc2 23044 itgparts 23047 itgsubstlem 23048 aalioulem3 23338 taylthlem2 23377 taylth 23378 efcvx 23452 pige3 23520 dvrelog 23630 advlog 23647 advlogexp 23648 logccv 23656 dvcxp1 23728 loglesqrt 23746 divsqrtsumlem 23953 lgamgulmlem2 24003 logexprlim 24201 logdivsum 24419 log2sumbnd 24430 ftc2nc 32070 dvreasin 32074 dvreacos 32075 areacirclem1 32076 itgpowd 36143 lhe4.4ex1a 36721 dvcosre 37818 dvcnre 37823 dvmptresicc 37828 itgsin0pilem1 37863 itgsinexplem1 37867 itgcoscmulx 37883 itgiccshift 37894 itgperiod 37895 itgsbtaddcnst 37896 dirkeritg 38001 dirkercncflem2 38003 fourierdlem28 38034 fourierdlem39 38046 fourierdlem56 38063 fourierdlem57 38064 fourierdlem58 38065 fourierdlem59 38066 fourierdlem60 38067 fourierdlem61 38068 fourierdlem62 38069 fourierdlem68 38075 fourierdlem72 38079 fouriersw 38132 etransclem2 38138 etransclem23 38159 etransclem35 38171 etransclem38 38174 etransclem39 38175 etransclem44 38180 etransclem45 38181 etransclem46 38182 etransclem47 38183 |
Copyright terms: Public domain | W3C validator |