| 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 11259 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 1c1 11156 · cmul 11160 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-mulcl 11217 ax-mulcom 11219 ax-mulass 11221 ax-distr 11222 ax-1rid 11225 ax-cnre 11228 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 |
| This theorem is referenced by: addrid 11441 0lt1 11785 muleqadd 11907 1t1e1 12428 2t1e2 12429 3t1e3 12431 halfpm6th 12487 9p1e10 12735 numltc 12759 numsucc 12773 dec10p 12776 numadd 12780 numaddc 12781 11multnc 12801 4t3lem 12830 5t2e10 12833 9t11e99 12863 nn0opthlem1 14307 faclbnd4lem1 14332 rei 15195 imi 15196 cji 15198 sqrtm1 15314 0.999... 15917 efival 16188 ef01bndlem 16220 5ndvds6 16451 3lcm2e6 16769 decsplit0b 17117 2exp8 17126 37prm 17158 43prm 17159 83prm 17160 139prm 17161 163prm 17162 317prm 17163 1259lem1 17168 1259lem2 17169 1259lem3 17170 1259lem4 17171 1259lem5 17172 2503lem1 17174 2503lem2 17175 2503prm 17177 4001lem1 17178 4001lem2 17179 4001lem3 17180 cnmsgnsubg 21595 mdetralt 22614 dveflem 26017 dvsincos 26019 efhalfpi 26513 pige3ALT 26562 cosne0 26571 efif1olem4 26587 logf1o2 26692 asin1 26937 dvatan 26978 log2ublem3 26991 log2ub 26992 birthday 26997 basellem9 27132 ppiub 27248 chtub 27256 bposlem8 27335 lgsdir2 27374 mulog2sumlem2 27579 pntlemb 27641 avril1 30482 ipidsq 30729 nmopadjlem 32108 nmopcoadji 32120 unierri 32123 sgnmul 34545 signswch 34576 itgexpif 34621 reprlt 34634 breprexp 34648 hgt750lem 34666 hgt750lem2 34667 circum 35679 dvasin 37711 3lexlogpow5ineq1 42055 3lexlogpow5ineq5 42061 aks4d1p1 42077 235t711 42339 ex-decpmul 42340 it1ei 42351 sqrtcval2 43655 resqrtvalex 43658 imsqrtvalex 43659 inductionexd 44168 xralrple3 45385 wallispi 46085 wallispi2lem2 46087 stirlinglem1 46089 dirkertrigeqlem3 46115 257prm 47548 fmtno4prmfac193 47560 fmtno5fac 47569 139prmALT 47583 127prm 47586 2exp340mod341 47720 |
| Copyright terms: Public domain | W3C validator |