Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mulid1i | Structured version Visualization version GIF version |
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
mulid1i | ⊢ (𝐴 · 1) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | mulid1 10628 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10524 1c1 10527 · cmul 10531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-mulcl 10588 ax-mulcom 10590 ax-mulass 10592 ax-distr 10593 ax-1rid 10596 ax-cnre 10599 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-iota 6308 df-fv 6357 df-ov 7148 |
This theorem is referenced by: addid1 10809 0lt1 11151 muleqadd 11273 1t1e1 11788 2t1e2 11789 3t1e3 11791 halfpm6th 11847 9p1e10 12089 numltc 12113 numsucc 12127 dec10p 12130 numadd 12134 numaddc 12135 11multnc 12155 4t3lem 12184 5t2e10 12187 9t11e99 12217 nn0opthlem1 13618 faclbnd4lem1 13643 rei 14505 imi 14506 cji 14508 sqrtm1 14625 0.999... 15227 efival 15495 ef01bndlem 15527 3lcm2e6 16062 decsplit0b 16406 2exp8 16413 37prm 16444 43prm 16445 83prm 16446 139prm 16447 163prm 16448 317prm 16449 1259lem1 16454 1259lem2 16455 1259lem3 16456 1259lem4 16457 1259lem5 16458 2503lem1 16460 2503lem2 16461 2503prm 16463 4001lem1 16464 4001lem2 16465 4001lem3 16466 cnmsgnsubg 20651 mdetralt 21147 dveflem 24505 dvsincos 24507 efhalfpi 24986 pige3ALT 25034 cosne0 25041 efif1olem4 25056 logf1o2 25160 asin1 25399 dvatan 25440 log2ublem3 25454 log2ub 25455 birthday 25460 basellem9 25594 ppiub 25708 chtub 25716 bposlem8 25795 lgsdir2 25834 mulog2sumlem2 26039 pntlemb 26101 avril1 28170 ipidsq 28415 nmopadjlem 29794 nmopcoadji 29806 unierri 29809 sgnmul 31700 signswch 31731 itgexpif 31777 reprlt 31790 breprexp 31804 hgt750lem 31822 hgt750lem2 31823 circum 32815 dvasin 34860 235t711 39057 ex-decpmul 39058 inductionexd 40385 xralrple3 41522 wallispi 42236 wallispi2lem2 42238 stirlinglem1 42240 dirkertrigeqlem3 42266 257prm 43570 fmtno4prmfac193 43582 fmtno5fac 43591 139prmALT 43606 127prm 43610 2exp340mod341 43745 |
Copyright terms: Public domain | W3C validator |