![]() |
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 7941 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 426 | 1 ⊢ (𝐴 · 𝐵) ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 (class class class)co 5878 ℂcc 7812 · cmul 7819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-mulcl 7912 |
This theorem is referenced by: ixi 8543 2mulicn 9144 numma 9430 nummac 9431 9t11e99 9516 decbin2 9527 irec 10623 binom2i 10632 3dec 10697 rei 10911 imi 10912 3dvdsdec 11873 3dvds2dec 11874 odd2np1 11881 3lcm2e6woprm 12089 6lcm4e12 12090 sinhalfpilem 14373 ef2pi 14387 ef2kpi 14388 efper 14389 sinperlem 14390 sin2kpi 14393 cos2kpi 14394 sin2pim 14395 cos2pim 14396 sincos4thpi 14422 sincos6thpi 14424 abssinper 14428 cosq34lt1 14432 lgsdir2lem5 14594 2lgsoddprmlem3c 14618 2lgsoddprmlem3d 14619 |
Copyright terms: Public domain | W3C validator |