![]() |
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 11217 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 ∈ wcel 2105 (class class class)co 7412 ℂcc 11112 1c1 11115 · cmul 11119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-mulcl 11176 ax-mulcom 11178 ax-mulass 11180 ax-distr 11181 ax-1rid 11184 ax-cnre 11187 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 df-ov 7415 |
This theorem is referenced by: addrid 11399 0lt1 11741 muleqadd 11863 1t1e1 12379 2t1e2 12380 3t1e3 12382 halfpm6th 12438 9p1e10 12684 numltc 12708 numsucc 12722 dec10p 12725 numadd 12729 numaddc 12730 11multnc 12750 4t3lem 12779 5t2e10 12782 9t11e99 12812 nn0opthlem1 14233 faclbnd4lem1 14258 rei 15108 imi 15109 cji 15111 sqrtm1 15227 0.999... 15832 efival 16100 ef01bndlem 16132 3lcm2e6 16673 decsplit0b 17018 2exp8 17027 37prm 17059 43prm 17060 83prm 17061 139prm 17062 163prm 17063 317prm 17064 1259lem1 17069 1259lem2 17070 1259lem3 17071 1259lem4 17072 1259lem5 17073 2503lem1 17075 2503lem2 17076 2503prm 17078 4001lem1 17079 4001lem2 17080 4001lem3 17081 cnmsgnsubg 21350 mdetralt 22331 dveflem 25732 dvsincos 25734 efhalfpi 26218 pige3ALT 26266 cosne0 26275 efif1olem4 26291 logf1o2 26395 asin1 26636 dvatan 26677 log2ublem3 26690 log2ub 26691 birthday 26696 basellem9 26830 ppiub 26944 chtub 26952 bposlem8 27031 lgsdir2 27070 mulog2sumlem2 27275 pntlemb 27337 avril1 29984 ipidsq 30231 nmopadjlem 31610 nmopcoadji 31622 unierri 31625 sgnmul 33840 signswch 33871 itgexpif 33917 reprlt 33930 breprexp 33944 hgt750lem 33962 hgt750lem2 33963 circum 34958 dvasin 36876 3lexlogpow5ineq1 41226 3lexlogpow5ineq5 41232 aks4d1p1 41248 235t711 41508 ex-decpmul 41509 sqrtcval2 42696 resqrtvalex 42699 imsqrtvalex 42700 inductionexd 43209 xralrple3 44383 wallispi 45085 wallispi2lem2 45087 stirlinglem1 45089 dirkertrigeqlem3 45115 257prm 46528 fmtno4prmfac193 46540 fmtno5fac 46549 139prmALT 46563 127prm 46566 2exp340mod341 46700 |
Copyright terms: Public domain | W3C validator |