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 10633 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2110 (class class class)co 7150 ℂcc 10529 1c1 10532 · cmul 10536 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-mulcl 10593 ax-mulcom 10595 ax-mulass 10597 ax-distr 10598 ax-1rid 10601 ax-cnre 10604 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 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 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-br 5060 df-iota 6309 df-fv 6358 df-ov 7153 |
This theorem is referenced by: addid1 10814 0lt1 11156 muleqadd 11278 1t1e1 11793 2t1e2 11794 3t1e3 11796 halfpm6th 11852 9p1e10 12094 numltc 12118 numsucc 12132 dec10p 12135 numadd 12139 numaddc 12140 11multnc 12160 4t3lem 12189 5t2e10 12192 9t11e99 12222 nn0opthlem1 13622 faclbnd4lem1 13647 rei 14509 imi 14510 cji 14512 sqrtm1 14629 0.999... 15231 efival 15499 ef01bndlem 15531 3lcm2e6 16066 decsplit0b 16410 2exp8 16417 37prm 16448 43prm 16449 83prm 16450 139prm 16451 163prm 16452 317prm 16453 1259lem1 16458 1259lem2 16459 1259lem3 16460 1259lem4 16461 1259lem5 16462 2503lem1 16464 2503lem2 16465 2503prm 16467 4001lem1 16468 4001lem2 16469 4001lem3 16470 cnmsgnsubg 20715 mdetralt 21211 dveflem 24570 dvsincos 24572 efhalfpi 25051 pige3ALT 25099 cosne0 25108 efif1olem4 25123 logf1o2 25227 asin1 25466 dvatan 25507 log2ublem3 25520 log2ub 25521 birthday 25526 basellem9 25660 ppiub 25774 chtub 25782 bposlem8 25861 lgsdir2 25900 mulog2sumlem2 26105 pntlemb 26167 avril1 28236 ipidsq 28481 nmopadjlem 29860 nmopcoadji 29872 unierri 29875 sgnmul 31795 signswch 31826 itgexpif 31872 reprlt 31885 breprexp 31899 hgt750lem 31917 hgt750lem2 31918 circum 32912 dvasin 34972 235t711 39170 ex-decpmul 39171 inductionexd 40498 xralrple3 41634 wallispi 42348 wallispi2lem2 42350 stirlinglem1 42352 dirkertrigeqlem3 42378 257prm 43716 fmtno4prmfac193 43728 fmtno5fac 43737 139prmALT 43752 127prm 43756 2exp340mod341 43891 |
Copyright terms: Public domain | W3C validator |