rexri - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rexri		Structured version Visualization version GIF version

Theorem rexri 11296

Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)

**Hypothesis**
Ref	Expression
rexri.1	⊢ 𝐴 ∈ ℝ

**Assertion**
Ref	Expression
rexri	⊢ 𝐴 ∈ ℝ^*

**Proof of Theorem rexri**
Step	Hyp	Ref	Expression
1		rexri.1	. 2 ⊢ 𝐴 ∈ ℝ
2		rexr 11284	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ^*

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2099 ℝcr 11131 ℝ^*cxr 11271

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3472 df-un 3950 df-in 3952 df-ss 3962 df-xr 11276

This theorem is referenced by: 1xr 11297 xnn0n0n1ge2b 13137 hashgt23el 14409 hashge2el2difr 14468 tanhbnd 16131 halfleoddlt 16332 oprpiece1res1 24869 oprpiece1res2 24870 pcoass 24944 vitalilem4 25533 neghalfpirx 26394 sincosq1sgn 26426 sincosq2sgn 26427 sincosq4sgn 26429 coseq00topi 26430 coseq0negpitopi 26431 tanabsge 26434 sinq12gt0 26435 cosq14gt0 26438 cos02pilt1 26453 cosq34lt1 26454 cosordlem 26457 cos0pilt1 26459 tanord1 26464 tanord 26465 tanregt0 26466 negpitopissre 26467 ellogrn 26486 logimclad 26499 argregt0 26537 argimgt0 26539 argimlt0 26540 dvloglem 26575 logf1o2 26577 efopnlem2 26584 isosctrlem1 26743 asinneg 26811 asinsinlem 26816 acoscos 26818 reasinsin 26821 atanlogsublem 26840 atantan 26848 atanbndlem 26850 atanbnd 26851 atan1 26853 dchrvmasumlem2 27424 dchrvmasumiflem1 27427 tgldimor 28299 upgrfi 28897 umgrislfupgrlem 28928 upgrewlkle2 29413 upgr2pthnlp 29539 nmoptrii 31897 nmopcoi 31898 sgnsgn 34162 chtvalz 34255 lfuhgr2 34722 usgrcyclgt2v 34735 acycgr2v 34754 cusgracyclt3v 34760 dnizeq0 35944 cnndvlem1 36006 bj-pinftyccb 36694 bj-minftyccb 36698 bj-pinftynminfty 36700 sin2h 37077 cos2h 37078 tan2h 37079 asindmre 37170 dvasin 37171 dvacos 37172 areacirclem1 37175 acos1half 42091 areaquad 42638 isosctrlem1ALT 44367 sineq0ALT 44370 itgsin0pilem1 45332 fourierdlem24 45513 fourierdlem38 45527 fourierdlem43 45532 fourierdlem44 45533 fourierdlem46 45534 fourierdlem62 45550 fourierdlem74 45562 fourierdlem75 45563 fourierdlem85 45573 fourierdlem88 45576 fourierdlem93 45581 fourierdlem102 45590 fourierdlem103 45591 fourierdlem104 45592 fourierdlem111 45599 fourierdlem112 45600 fourierdlem114 45602 sqwvfoura 45610 sqwvfourb 45611 fourierswlem 45612 fouriersw 45613 fouriercn 45614 salexct2 45721 mod42tp1mod8 46936 bgoldbtbndlem1 47139 bgoldbtbnd 47143 pgrpgt2nabl 47424 sepfsepc 47940

W3C validator

	
		OSZAR »