Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 1t1e1 | Structured version Visualization version GIF version |
Description: 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
1t1e1 | ⊢ (1 · 1) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 10583 | . 2 ⊢ 1 ∈ ℂ | |
2 | 1 | mulid1i 10633 | 1 ⊢ (1 · 1) = 1 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 (class class class)co 7145 1c1 10526 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-resscn 10582 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-mulcl 10587 ax-mulcom 10589 ax-mulass 10591 ax-distr 10592 ax-1rid 10595 ax-cnre 10598 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 |
This theorem is referenced by: neg1mulneg1e1 11838 addltmul 11861 1exp 13446 expge1 13454 mulexp 13456 mulexpz 13457 expaddz 13461 m1expeven 13464 sqrecii 13534 i4 13555 facp1 13626 hashf1 13803 binom 15173 prodf1 15235 prodfrec 15239 fprodmul 15302 fprodge1 15337 fallfac0 15370 binomfallfac 15383 pwp1fsum 15730 rpmul 15991 2503lem2 16459 2503lem3 16460 4001lem4 16465 abvtrivd 19540 iimulcl 23468 dvexp 24477 dvef 24504 mulcxplem 25194 cxpmul2 25199 dvsqrt 25250 dvcnsqrt 25252 abscxpbnd 25261 1cubr 25347 dchrmulcl 25752 dchr1cl 25754 dchrinvcl 25756 lgslem3 25802 lgsval2lem 25810 lgsneg 25824 lgsdilem 25827 lgsdir 25835 lgsdi 25837 lgsquad2lem1 25887 lgsquad2lem2 25888 dchrisum0flblem2 26012 rpvmasum2 26015 mudivsum 26033 pntibndlem2 26094 axlowdimlem6 26660 hisubcomi 28808 lnophmlem2 29721 1nei 30398 1neg1t1neg1 30399 sgnmul 31699 hgt750lem2 31822 subfacval2 32331 faclim2 32877 knoppndvlem18 33765 pell1234qrmulcl 39330 pellqrex 39354 binomcxplemnotnn0 40565 dvnprodlem3 42109 stoweidlem13 42175 stoweidlem16 42178 wallispi 42232 wallispi2lem2 42234 2exp340mod341 43775 8exp8mod9 43778 nn0sumshdiglemB 44608 |
Copyright terms: Public domain | W3C validator |