Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | recnd.1 | โข ( ๐ โ ๐ด โ โ ) | |
readdcld.2 | โข ( ๐ โ ๐ต โ โ ) | ||
Assertion | remulcld | โข ( ๐ โ ( ๐ด ยท ๐ต ) โ โ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recnd.1 | โข ( ๐ โ ๐ด โ โ ) | |
2 | readdcld.2 | โข ( ๐ โ ๐ต โ โ ) | |
3 | remulcl | โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท ๐ต ) โ โ ) | |
4 | 1 2 3 | syl2anc | โข ( ๐ โ ( ๐ด ยท ๐ต ) โ โ ) |