Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcli | 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 7901 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 424 | 1 ⊢ (𝐴 · 𝐵) ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2141 (class class class)co 5853 ℂcc 7772 · cmul 7779 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-mulcl 7872 |
This theorem is referenced by: ixi 8502 2mulicn 9100 numma 9386 nummac 9387 9t11e99 9472 decbin2 9483 irec 10575 binom2i 10584 3dec 10648 rei 10863 imi 10864 3dvdsdec 11824 3dvds2dec 11825 odd2np1 11832 3lcm2e6woprm 12040 6lcm4e12 12041 sinhalfpilem 13506 ef2pi 13520 ef2kpi 13521 efper 13522 sinperlem 13523 sin2kpi 13526 cos2kpi 13527 sin2pim 13528 cos2pim 13529 sincos4thpi 13555 sincos6thpi 13557 abssinper 13561 cosq34lt1 13565 lgsdir2lem5 13727 |
Copyright terms: Public domain | W3C validator |