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 10813 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 · 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 (class class class)co 7213 ℂcc 10727 · cmul 10734 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcl 10791 |
This theorem depends on definitions: df-bi 210 df-an 400 |
This theorem is referenced by: mul02lem2 11009 addid1 11012 cnegex2 11014 ixi 11461 2mulicn 12053 numma 12337 nummac 12338 9t11e99 12423 decbin2 12434 irec 13770 binom2i 13780 crreczi 13795 3dec 13832 nn0opthi 13836 faclbnd4lem1 13859 rei 14719 imi 14720 iseraltlem2 15246 bpoly3 15620 bpoly4 15621 3dvdsdec 15893 3dvds2dec 15894 odd2np1 15902 gcdaddmlem 16083 3lcm2e6woprm 16172 6lcm4e12 16173 modxai 16621 mod2xnegi 16624 decexp2 16628 karatsuba 16637 sinhalfpilem 25353 ef2pi 25367 ef2kpi 25368 efper 25369 sinperlem 25370 sin2kpi 25373 cos2kpi 25374 sin2pim 25375 cos2pim 25376 sincos4thpi 25403 sincos6thpi 25405 pige3ALT 25409 abssinper 25410 efeq1 25417 logneg 25476 logm1 25477 eflogeq 25490 logimul 25502 logneg2 25503 cxpsqrt 25591 root1eq1 25641 cxpeq 25643 ang180lem1 25692 ang180lem3 25694 ang180lem4 25695 1cubrlem 25724 1cubr 25725 quart1lem 25738 asin1 25777 atanlogsublem 25798 log2ublem2 25830 log2ublem3 25831 log2ub 25832 bclbnd 26161 bposlem8 26172 bposlem9 26173 lgsdir2lem5 26210 2lgsoddprmlem3c 26293 2lgsoddprmlem3d 26294 ax5seglem7 27026 ip0i 28906 ip1ilem 28907 ipasslem10 28920 siilem1 28932 normlem0 29190 normlem1 29191 normlem2 29192 normlem3 29193 normlem5 29195 normlem7 29197 bcseqi 29201 norm-ii-i 29218 normpar2i 29237 polid2i 29238 h1de2i 29634 lnopunilem1 30091 lnophmlem2 30098 dfdec100 30864 dpmul100 30891 dp3mul10 30892 dpmul1000 30893 dpexpp1 30902 dpmul 30907 dpmul4 30908 ballotth 32216 efmul2picn 32288 itgexpif 32298 vtscl 32330 circlemeth 32332 hgt750lem 32343 problem2 33337 problem4 33339 quad3 33341 logi 33418 heiborlem6 35711 gcdaddmzz2nncomi 39738 sn-1ne2 40002 sqsumi 40016 sqmid3api 40018 sqdeccom12 40024 re1m1e0m0 40088 reixi 40112 sn-1ticom 40124 sn-0tie0 40129 sn-inelr 40143 proot1ex 40729 areaquad 40750 resqrtvalex 40929 imsqrtvalex 40930 coskpi2 43082 cosnegpi 43083 cosknegpi 43085 wallispilem4 43284 dirkerper 43312 dirkertrigeq 43317 dirkercncflem2 43320 fourierdlem57 43379 fourierdlem62 43384 fourierswlem 43446 fmtnorec3 44673 fmtnorec4 44674 lighneallem3 44732 3exp4mod41 44741 41prothprmlem1 44742 zlmodzxzequap 45513 nn0sumshdiglemB 45639 i2linesi 46153 |
Copyright terms: Public domain | W3C validator |