![]() |
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 11132 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (𝐴 · 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7354 ℂcc 11046 · cmul 11053 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcl 11110 |
This theorem depends on definitions: df-bi 206 df-an 397 |
This theorem is referenced by: mul02lem2 11329 addid1 11332 cnegex2 11334 ixi 11781 2mulicn 12373 numma 12659 nummac 12660 9t11e99 12745 decbin2 12756 irec 14102 binom2i 14113 crreczi 14128 3dec 14163 nn0opthi 14167 faclbnd4lem1 14190 rei 15038 imi 15039 iseraltlem2 15564 bpoly3 15938 bpoly4 15939 3dvdsdec 16211 3dvds2dec 16212 odd2np1 16220 gcdaddmlem 16401 3lcm2e6woprm 16488 6lcm4e12 16489 modxai 16937 mod2xnegi 16940 decexp2 16944 karatsuba 16953 sinhalfpilem 25816 ef2pi 25830 ef2kpi 25831 efper 25832 sinperlem 25833 sin2kpi 25836 cos2kpi 25837 sin2pim 25838 cos2pim 25839 sincos4thpi 25866 sincos6thpi 25868 pige3ALT 25872 abssinper 25873 efeq1 25880 logneg 25939 logm1 25940 eflogeq 25953 logimul 25965 logneg2 25966 cxpsqrt 26054 root1eq1 26104 cxpeq 26106 ang180lem1 26155 ang180lem3 26157 ang180lem4 26158 1cubrlem 26187 1cubr 26188 quart1lem 26201 asin1 26240 atanlogsublem 26261 log2ublem2 26293 log2ublem3 26294 log2ub 26295 bclbnd 26624 bposlem8 26635 bposlem9 26636 lgsdir2lem5 26673 2lgsoddprmlem3c 26756 2lgsoddprmlem3d 26757 ax5seglem7 27782 ip0i 29665 ip1ilem 29666 ipasslem10 29679 siilem1 29691 normlem0 29949 normlem1 29950 normlem2 29951 normlem3 29952 normlem5 29954 normlem7 29956 bcseqi 29960 norm-ii-i 29977 normpar2i 29996 polid2i 29997 h1de2i 30393 lnopunilem1 30850 lnophmlem2 30857 dfdec100 31621 dpmul100 31648 dp3mul10 31649 dpmul1000 31650 dpexpp1 31659 dpmul 31664 dpmul4 31665 ballotth 33028 efmul2picn 33100 itgexpif 33110 vtscl 33142 circlemeth 33144 hgt750lem 33155 problem2 34145 problem4 34147 quad3 34149 logi 34199 heiborlem6 36264 gcdaddmzz2nncomi 40442 sn-1ne2 40757 sqsumi 40771 sqmid3api 40773 sqdeccom12 40779 re1m1e0m0 40842 reixi 40867 sn-1ticom 40879 sn-0tie0 40884 sn-inelr 40910 proot1ex 41504 areaquad 41526 resqrtvalex 41897 imsqrtvalex 41898 coskpi2 44077 cosnegpi 44078 cosknegpi 44080 wallispilem4 44279 dirkerper 44307 dirkertrigeq 44312 dirkercncflem2 44315 fourierdlem57 44374 fourierdlem62 44379 fourierswlem 44441 fmtnorec3 45710 fmtnorec4 45711 lighneallem3 45769 3exp4mod41 45778 41prothprmlem1 45779 zlmodzxzequap 46550 nn0sumshdiglemB 46676 i2linesi 47195 |
Copyright terms: Public domain | W3C validator |