![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > remulcl | GIF version |
Description: Alias for ax-mulrcl 7907, for naming consistency with remulcli 7968. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
remulcl | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulrcl 7907 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 (class class class)co 5872 ℝcr 7807 · cmul 7813 |
This theorem was proved from axioms: ax-mulrcl 7907 |
This theorem is referenced by: remulcli 7968 remulcld 7984 axmulgt0 8025 msqge0 8569 mulge0 8572 recexaplem2 8605 recexap 8606 ltmul12a 8813 lemul12b 8814 mulgt1 8816 ltdivmul 8829 cju 8914 addltmul 9151 zmulcl 9302 irrmul 9643 rpmulcl 9674 ge0mulcl 9978 iccdil 9994 reexpcl 10532 reexpclzap 10535 expge0 10551 expge1 10552 expubnd 10572 bernneq 10635 faclbnd 10714 faclbnd3 10716 facavg 10719 crre 10859 remim 10862 mulreap 10866 amgm2 11120 fprodrecl 11609 fprodreclf 11615 efcllemp 11659 ege2le3 11672 ef01bndlem 11757 cos01gt0 11763 dveflem 14058 sinq12gt0 14122 tangtx 14130 coskpi 14140 relogexp 14164 logcxp 14189 rpabscxpbnd 14230 |
Copyright terms: Public domain | W3C validator |