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 7859 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 423 | 1 ⊢ (𝐴 · 𝐵) ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2128 (class class class)co 5824 ℂcc 7730 · cmul 7737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-mulcl 7830 |
This theorem is referenced by: ixi 8458 2mulicn 9055 numma 9338 nummac 9339 9t11e99 9424 decbin2 9435 irec 10518 binom2i 10527 3dec 10588 rei 10799 imi 10800 3dvdsdec 11756 3dvds2dec 11757 odd2np1 11764 3lcm2e6woprm 11963 6lcm4e12 11964 sinhalfpilem 13123 ef2pi 13137 ef2kpi 13138 efper 13139 sinperlem 13140 sin2kpi 13143 cos2kpi 13144 sin2pim 13145 cos2pim 13146 sincos4thpi 13172 sincos6thpi 13174 abssinper 13178 cosq34lt1 13182 |
Copyright terms: Public domain | W3C validator |