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 10831 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2110 (class class class)co 7213 ℂcc 10727 1c1 10730 · cmul 10734 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-mulcl 10791 ax-mulcom 10793 ax-mulass 10795 ax-distr 10796 ax-1rid 10799 ax-cnre 10802 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-iota 6338 df-fv 6388 df-ov 7216 |
This theorem is referenced by: addid1 11012 0lt1 11354 muleqadd 11476 1t1e1 11992 2t1e2 11993 3t1e3 11995 halfpm6th 12051 9p1e10 12295 numltc 12319 numsucc 12333 dec10p 12336 numadd 12340 numaddc 12341 11multnc 12361 4t3lem 12390 5t2e10 12393 9t11e99 12423 nn0opthlem1 13834 faclbnd4lem1 13859 rei 14719 imi 14720 cji 14722 sqrtm1 14839 0.999... 15445 efival 15713 ef01bndlem 15745 3lcm2e6 16288 decsplit0b 16633 2exp8 16642 37prm 16674 43prm 16675 83prm 16676 139prm 16677 163prm 16678 317prm 16679 1259lem1 16684 1259lem2 16685 1259lem3 16686 1259lem4 16687 1259lem5 16688 2503lem1 16690 2503lem2 16691 2503prm 16693 4001lem1 16694 4001lem2 16695 4001lem3 16696 cnmsgnsubg 20539 mdetralt 21505 dveflem 24876 dvsincos 24878 efhalfpi 25361 pige3ALT 25409 cosne0 25418 efif1olem4 25434 logf1o2 25538 asin1 25777 dvatan 25818 log2ublem3 25831 log2ub 25832 birthday 25837 basellem9 25971 ppiub 26085 chtub 26093 bposlem8 26172 lgsdir2 26211 mulog2sumlem2 26416 pntlemb 26478 avril1 28546 ipidsq 28791 nmopadjlem 30170 nmopcoadji 30182 unierri 30185 sgnmul 32221 signswch 32252 itgexpif 32298 reprlt 32311 breprexp 32325 hgt750lem 32343 hgt750lem2 32344 circum 33345 dvasin 35598 3lexlogpow5ineq1 39796 3lexlogpow5ineq5 39802 aks4d1p1 39817 235t711 40026 ex-decpmul 40027 sqrtcval2 40926 resqrtvalex 40929 imsqrtvalex 40930 inductionexd 41442 xralrple3 42586 wallispi 43286 wallispi2lem2 43288 stirlinglem1 43290 dirkertrigeqlem3 43316 257prm 44686 fmtno4prmfac193 44698 fmtno5fac 44707 139prmALT 44721 127prm 44724 2exp340mod341 44858 |
Copyright terms: Public domain | W3C validator |