![]() |
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 7162 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 403 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 (class class class)co 5543 ℂcc 7041 · cmul 7048 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 ax-mulcl 7136 |
This theorem is referenced by: kcnktkm1cn 7554 rereim 7753 cru 7769 apreim 7770 mulreim 7771 apadd1 7775 apneg 7778 mulext1 7779 mulext 7781 mulap0 7811 receuap 7826 divrecap 7843 divcanap3 7853 muldivdirap 7862 divdivdivap 7868 divsubdivap 7883 apmul1 7943 qapne 8805 cnref1o 8814 lincmb01cmp 9101 iccf1o 9102 qbtwnrelemcalc 9342 flqpmodeq 9409 modq0 9411 modqdiffl 9417 modqvalp1 9425 modqcyc 9441 modqcyc2 9442 modqadd1 9443 mulqaddmodid 9446 modqmuladdnn0 9450 qnegmod 9451 modqmul1 9459 mulexpzap 9613 expmulzap 9619 binom2 9682 binom3 9687 bernneq 9690 nn0opthd 9746 ibcval5 9787 remullem 9896 cjreim2 9929 cnrecnv 9935 absval 10025 resqrexlemover 10034 resqrexlemcalc1 10038 resqrexlemnm 10042 absimle 10108 abstri 10128 mulcn2 10289 iisermulc2 10316 climcvg1nlem 10324 dvdscmulr 10369 dvdsmulcr 10370 dvds2ln 10373 oddm1even 10419 divalglemnn 10462 divalglemnqt 10464 flodddiv4 10478 gcdaddm 10519 bezoutlemnewy 10529 bezoutlema 10532 bezoutlemb 10533 lcmgcdlem 10603 oddpwdc 10696 oddennn 10703 qdencn 10943 |
Copyright terms: Public domain | W3C validator |