![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reelprrecn | Structured version Visualization version GIF version |
Description: Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
reelprrecn | ⊢ ℝ ∈ {ℝ, ℂ} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reex 10617 | . 2 ⊢ ℝ ∈ V | |
2 | 1 | prid1 4658 | 1 ⊢ ℝ ∈ {ℝ, ℂ} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 {cpr 4527 ℂcc 10524 ℝcr 10525 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-sep 5167 ax-cnex 10582 ax-resscn 10583 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 |
This theorem is referenced by: dvf 24510 dvmptresicc 24519 dvmptcj 24571 dvmptre 24572 dvmptim 24573 rolle 24593 cmvth 24594 mvth 24595 dvlip 24596 dvlipcn 24597 dvle 24610 dvivthlem1 24611 dvivth 24613 lhop2 24618 dvcnvre 24622 dvfsumle 24624 dvfsumge 24625 dvfsumabs 24626 dvfsumlem2 24630 dvfsum2 24637 ftc2 24647 itgparts 24650 itgsubstlem 24651 itgpowd 24653 aalioulem3 24930 taylthlem2 24969 taylth 24970 efcvx 25044 pige3ALT 25112 dvrelog 25228 advlog 25245 advlogexp 25246 logccv 25254 dvcxp1 25329 loglesqrt 25347 divsqrtsumlem 25565 lgamgulmlem2 25615 logexprlim 25809 logdivsum 26117 log2sumbnd 26128 fdvneggt 31981 fdvnegge 31983 itgexpif 31987 logdivsqrle 32031 ftc2nc 35139 dvreasin 35143 dvreacos 35144 areacirclem1 35145 lhe4.4ex1a 41033 dvcosre 42554 dvcnre 42558 itgsin0pilem1 42592 itgsinexplem1 42596 itgcoscmulx 42611 itgiccshift 42622 itgperiod 42623 itgsbtaddcnst 42624 dirkeritg 42744 dirkercncflem2 42746 fourierdlem28 42777 fourierdlem39 42788 fourierdlem56 42804 fourierdlem57 42805 fourierdlem58 42806 fourierdlem59 42807 fourierdlem60 42808 fourierdlem61 42809 fourierdlem62 42810 fourierdlem68 42816 fourierdlem72 42820 fouriersw 42873 etransclem2 42878 etransclem23 42899 etransclem35 42911 etransclem38 42914 etransclem39 42915 etransclem44 42920 etransclem45 42921 etransclem46 42922 etransclem47 42923 |
Copyright terms: Public domain | W3C validator |