remulcli - Metamath Proof Explorer

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

Theorem remulcli 10054

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)

**Hypotheses**
Ref	Expression
recni.1
axri.2

**Assertion**
Ref	Expression
remulcli

**Proof of Theorem remulcli**
Step	Hyp	Ref	Expression
1		recni.1	. 2
2		axri.2	. 2
3		remulcl 10021	. 2 $/\$
4	1, 2, 3	mp2an 708	1

Colors of variables: wff setvar class

Syntax hints:

wcel 1990 (class class class)co 6650

cr 9935

cmul 9941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulrcl 9999

This theorem depends on definitions: df-bi 197 df-an 386

This theorem is referenced by: ledivp1i 10949 ltdivp1i 10950 addltmul 11268 nn0lele2xi 11348 numltc 11528 decleOLD 11543 nn0opthlem2 13056 faclbnd4lem1 13080 ef01bndlem 14914 cos2bnd 14918 sin4lt0 14925 dvdslelem 15031 divalglem1 15117 divalglem6 15121 sincosq3sgn 24252 sincosq4sgn 24253 sincos4thpi 24265 efif1olem1 24288 efif1olem2 24289 efif1olem4 24291 efif1o 24292 efifo 24293 ang180lem1 24539 ang180lem2 24540 log2ublem1 24673 log2ublem2 24674 bpos1lem 25007 bposlem7 25015 bposlem8 25016 bposlem9 25017 chebbnd1lem3 25160 chebbnd1 25161 chto1ub 25165 siilem1 27706 normlem6 27972 normlem7 27973 norm-ii-i 27994 bcsiALT 28036 nmopadjlem 28948 nmopcoi 28954 bdopcoi 28957 nmopcoadji 28960 unierri 28963 dpmul4 29622 hgt750lem 30729 hgt750lem2 30730 hgt750leme 30736 problem5 31563 circum 31568 iexpire 31621 taupi 33169 sin2h 33399 tan2h 33401 sumnnodd 39862 sinaover2ne0 40079 stirlinglem11 40301 dirkerper 40313 dirkercncflem2 40321 dirkercncflem4 40323 fourierdlem24 40348 fourierdlem43 40367 fourierdlem44 40368 fourierdlem68 40391 fourierdlem94 40417 fourierdlem111 40434 fourierdlem113 40436 sqwvfoura 40445 sqwvfourb 40446 fourierswlem 40447 fouriersw 40448 lighneallem4a 41525 tgoldbach 41705 tgoldbachOLD 41712