![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > remulcld | GIF version |
Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
recnd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
readdcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
Ref | Expression |
---|---|
remulcld | ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recnd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | readdcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
3 | remulcl 7215 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | syl2anc 403 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 (class class class)co 5563 ℝcr 7094 · cmul 7100 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 ax-mulrcl 7189 |
This theorem is referenced by: rimul 7804 ltmul1a 7810 ltmul1 7811 lemul1 7812 reapmul1lem 7813 reapmul1 7814 remulext1 7818 mulext1 7831 recexaplem2 7861 redivclap 7938 prodgt0gt0 8048 prodgt0 8049 prodge0 8051 lemul1a 8055 ltmuldiv 8071 ledivmul 8074 lt2mul2div 8076 lemuldiv 8078 lt2msq1 8082 lt2msq 8083 ltdiv23 8089 lediv23 8090 le2msq 8098 msq11 8099 div4p1lem1div2 8403 lincmb01cmp 9153 iccf1o 9154 qbtwnrelemcalc 9394 qbtwnre 9395 flhalf 9436 modqval 9458 modqge0 9466 modqmulnn 9476 bernneq 9742 bernneq3 9744 expnbnd 9745 nn0opthlem2d 9797 faclbnd 9817 faclbnd6 9820 remullem 9959 cvg1nlemres 10072 resqrexlemover 10097 resqrexlemnm 10105 resqrexlemglsq 10109 sqrtmul 10122 abstri 10191 maxabslemlub 10294 maxltsup 10305 mulcn2 10352 dvdslelemd 10451 divalglemnqt 10527 oddennn 10812 |
Copyright terms: Public domain | W3C validator |