Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcld | GIF version |
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
mulcld | ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | mulcl 7008 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 391 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 · cmul 6894 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 ax-mulcl 6982 |
This theorem is referenced by: kcnktkm1cn 7380 rereim 7577 cru 7593 apreim 7594 mulreim 7595 apadd1 7599 apneg 7602 mulext1 7603 mulext 7605 mulap0 7635 receuap 7650 divrecap 7667 divcanap3 7675 divdivdivap 7689 divsubdivap 7704 apmul1 7764 qapne 8574 cnref1o 8582 lincmb01cmp 8871 iccf1o 8872 qbtwnrelemcalc 9110 flqpmodeq 9169 modq0 9171 modqdiffl 9177 mulexpzap 9295 expmulzap 9301 binom2 9362 binom3 9366 bernneq 9369 remullem 9471 cjreim2 9504 cnrecnv 9510 absval 9599 resqrexlemover 9608 resqrexlemcalc1 9612 resqrexlemnm 9616 absimle 9680 abstri 9700 mulcn2 9833 iisermulc2 9860 climcvg1nlem 9868 qdencn 10124 |
Copyright terms: Public domain | W3C validator |