![]() |
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 7772 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 423 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-mulrcl 7743 |
This theorem is referenced by: addltmul 8980 nn0lele2xi 9052 numltc 9231 ef01bndlem 11499 cos2bnd 11503 sin4lt0 11509 sincosq3sgn 12957 sincosq4sgn 12958 cosq23lt0 12962 coseq0q4123 12963 coseq00topi 12964 coseq0negpitopi 12965 sincos4thpi 12969 cosq34lt1 12979 cos02pilt1 12980 cos0pilt1 12981 taupi 13430 |
Copyright terms: Public domain | W3C validator |