![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulcli | Structured version Visualization version GIF version |
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
Ref | Expression |
---|---|
mulcli | ⊢ (𝐴 · 𝐵) ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | mulcl 11242 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (𝐴 · 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 (class class class)co 7424 ℂcc 11156 · cmul 11163 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcl 11220 |
This theorem depends on definitions: df-bi 206 df-an 395 |
This theorem is referenced by: mul02lem2 11441 addrid 11444 cnegex2 11446 ixi 11893 2mulicn 12487 numma 12773 nummac 12774 9t11e99 12859 decbin2 12870 irec 14219 binom2i 14230 crreczi 14245 3dec 14283 nn0opthi 14287 faclbnd4lem1 14310 rei 15161 imi 15162 iseraltlem2 15687 bpoly3 16060 bpoly4 16061 3dvdsdec 16334 3dvds2dec 16335 odd2np1 16343 gcdaddmlem 16524 3lcm2e6woprm 16616 6lcm4e12 16617 modxai 17070 mod2xnegi 17073 decexp2 17077 karatsuba 17086 sinhalfpilem 26491 ef2pi 26505 ef2kpi 26506 efper 26507 sinperlem 26508 sin2kpi 26511 cos2kpi 26512 sin2pim 26513 cos2pim 26514 sincos4thpi 26541 sincos6thpi 26543 pige3ALT 26547 abssinper 26548 efeq1 26555 logi 26614 logneg 26615 logm1 26616 eflogeq 26629 logimul 26641 logneg2 26642 cxpsqrt 26730 root1eq1 26783 cxpeq 26785 ang180lem1 26837 ang180lem3 26839 ang180lem4 26840 1cubrlem 26869 1cubr 26870 quart1lem 26883 asin1 26922 atanlogsublem 26943 log2ublem2 26975 log2ublem3 26976 log2ub 26977 bclbnd 27309 bposlem8 27320 bposlem9 27321 lgsdir2lem5 27358 2lgsoddprmlem3c 27441 2lgsoddprmlem3d 27442 ax5seglem7 28869 ip0i 30758 ip1ilem 30759 ipasslem10 30772 siilem1 30784 normlem0 31042 normlem1 31043 normlem2 31044 normlem3 31045 normlem5 31047 normlem7 31049 bcseqi 31053 norm-ii-i 31070 normpar2i 31089 polid2i 31090 h1de2i 31486 lnopunilem1 31943 lnophmlem2 31950 dfdec100 32731 dpmul100 32758 dp3mul10 32759 dpmul1000 32760 dpexpp1 32769 dpmul 32774 dpmul4 32775 ballotth 34371 efmul2picn 34442 itgexpif 34452 vtscl 34484 circlemeth 34486 hgt750lem 34497 problem2 35494 problem4 35496 quad3 35498 heiborlem6 37517 gcdaddmzz2nncomi 41694 sn-1ne2 42079 sqsumi 42094 sqmid3api 42096 sqdeccom12 42102 cxp112d 42137 cxp111d 42138 cxpi11d 42139 re1m1e0m0 42177 reixi 42202 sn-1ticom 42214 sn-0tie0 42219 sn-inelr 42247 proot1ex 42861 areaquad 42881 resqrtvalex 43312 imsqrtvalex 43313 coskpi2 45487 cosnegpi 45488 cosknegpi 45490 wallispilem4 45689 dirkerper 45717 dirkertrigeq 45722 dirkercncflem2 45725 fourierdlem57 45784 fourierdlem62 45789 fourierswlem 45851 fmtnorec3 47120 fmtnorec4 47121 lighneallem3 47179 3exp4mod41 47188 41prothprmlem1 47189 zlmodzxzequap 47882 nn0sumshdiglemB 48008 i2linesi 48526 |
Copyright terms: Public domain | W3C validator |