Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > remulcli | Unicode version |
Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Ref | Expression |
---|---|
recni.1 | |
axri.2 |
Ref | Expression |
---|---|
remulcli |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recni.1 | . 2 | |
2 | axri.2 | . 2 | |
3 | remulcl 7716 | . 2 | |
4 | 1, 2, 3 | mp2an 422 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1465 (class class class)co 5742 cr 7587 cmul 7593 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-mulrcl 7687 |
This theorem is referenced by: addltmul 8924 nn0lele2xi 8996 numltc 9175 ef01bndlem 11390 cos2bnd 11394 sin4lt0 11400 sincosq3sgn 12836 sincosq4sgn 12837 cosq23lt0 12841 coseq0q4123 12842 coseq00topi 12843 coseq0negpitopi 12844 sincos4thpi 12848 cosq34lt1 12858 cos02pilt1 12859 taupi 13166 |
Copyright terms: Public domain | W3C validator |