![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulridi | Structured version Visualization version GIF version |
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
mulridi | ⊢ (𝐴 · 1) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | mulrid 11256 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 ∈ wcel 2105 (class class class)co 7430 ℂcc 11150 1c1 11153 · cmul 11157 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-mulcl 11214 ax-mulcom 11216 ax-mulass 11218 ax-distr 11219 ax-1rid 11222 ax-cnre 11225 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-iota 6515 df-fv 6570 df-ov 7433 |
This theorem is referenced by: addrid 11438 0lt1 11782 muleqadd 11904 1t1e1 12425 2t1e2 12426 3t1e3 12428 halfpm6th 12484 9p1e10 12732 numltc 12756 numsucc 12770 dec10p 12773 numadd 12777 numaddc 12778 11multnc 12798 4t3lem 12827 5t2e10 12830 9t11e99 12860 nn0opthlem1 14303 faclbnd4lem1 14328 rei 15191 imi 15192 cji 15194 sqrtm1 15310 0.999... 15913 efival 16184 ef01bndlem 16216 5ndvds6 16447 3lcm2e6 16765 decsplit0b 17113 2exp8 17122 37prm 17154 43prm 17155 83prm 17156 139prm 17157 163prm 17158 317prm 17159 1259lem1 17164 1259lem2 17165 1259lem3 17166 1259lem4 17167 1259lem5 17168 2503lem1 17170 2503lem2 17171 2503prm 17173 4001lem1 17174 4001lem2 17175 4001lem3 17176 cnmsgnsubg 21612 mdetralt 22629 dveflem 26031 dvsincos 26033 efhalfpi 26527 pige3ALT 26576 cosne0 26585 efif1olem4 26601 logf1o2 26706 asin1 26951 dvatan 26992 log2ublem3 27005 log2ub 27006 birthday 27011 basellem9 27146 ppiub 27262 chtub 27270 bposlem8 27349 lgsdir2 27388 mulog2sumlem2 27593 pntlemb 27655 avril1 30491 ipidsq 30738 nmopadjlem 32117 nmopcoadji 32129 unierri 32132 sgnmul 34523 signswch 34554 itgexpif 34599 reprlt 34612 breprexp 34626 hgt750lem 34644 hgt750lem2 34645 circum 35658 dvasin 37690 3lexlogpow5ineq1 42035 3lexlogpow5ineq5 42041 aks4d1p1 42057 235t711 42317 ex-decpmul 42318 it1ei 42329 sqrtcval2 43631 resqrtvalex 43634 imsqrtvalex 43635 inductionexd 44144 xralrple3 45323 wallispi 46025 wallispi2lem2 46027 stirlinglem1 46029 dirkertrigeqlem3 46055 257prm 47485 fmtno4prmfac193 47497 fmtno5fac 47506 139prmALT 47520 127prm 47523 2exp340mod341 47657 |
Copyright terms: Public domain | W3C validator |