![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mullid | Structured version Visualization version GIF version |
Description: Identity law for multiplication. See mulrid 11210 for commuted version. (Contributed by NM, 8-Oct-1999.) |
Ref | Expression |
---|---|
mullid | ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 11165 | . . 3 ⊢ 1 ∈ ℂ | |
2 | mulcom 11193 | . . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1)) | |
3 | 1, 2 | mpan 687 | . 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1)) |
4 | mulrid 11210 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
5 | 3, 4 | eqtrd 2764 | 1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 (class class class)co 7402 ℂcc 11105 1c1 11108 · cmul 11112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-mulcl 11169 ax-mulcom 11171 ax-mulass 11173 ax-distr 11174 ax-1rid 11177 ax-cnre 11180 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-br 5140 df-iota 6486 df-fv 6542 df-ov 7405 |
This theorem is referenced by: mullidi 11217 mullidd 11230 muladd11 11382 1p1times 11383 mul02lem1 11388 cnegex2 11394 mulm1 11653 div1 11901 subdivcomb2 11908 recdiv 11918 divdiv2 11924 conjmul 11929 ser1const 14022 expp1 14032 recan 15281 arisum 15804 geo2sum 15817 prodrblem 15871 prodmolem2a 15876 risefac1 15975 fallfac1 15976 bpoly3 16000 bpoly4 16001 sinhval 16096 coshval 16097 demoivreALT 16143 gcdadd 16466 gcdid 16467 cncrng 21252 cnfld1 21256 blcvx 24638 icccvx 24799 cnlmod 24991 coeidp 26120 dgrid 26121 quartlem1 26708 asinsinlem 26742 asinsin 26743 atantan 26774 musumsum 27043 brbtwn2 28635 axsegconlem1 28647 ax5seglem1 28658 ax5seglem2 28659 ax5seglem4 28662 ax5seglem5 28663 axeuclid 28693 axcontlem2 28695 axcontlem4 28697 cncvcOLD 30308 gg-cncrng 35674 gg-cnfld1 35675 dvcosax 45152 |
Copyright terms: Public domain | W3C validator |