![]() |
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 11191 | . 2 ⊢ 1 ∈ ℂ | |
2 | 1 | mulridi 11243 | 1 ⊢ (1 · 1) = 1 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 (class class class)co 7415 1c1 11134 · cmul 11138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-resscn 11190 ax-1cn 11191 ax-icn 11192 ax-addcl 11193 ax-mulcl 11195 ax-mulcom 11197 ax-mulass 11199 ax-distr 11200 ax-1rid 11203 ax-cnre 11206 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rex 3067 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4526 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4905 df-br 5144 df-iota 6495 df-fv 6551 df-ov 7418 |
This theorem is referenced by: neg1mulneg1e1 12450 addltmul 12473 1exp 14083 expge1 14091 mulexp 14093 mulexpz 14094 expaddz 14098 m1expeven 14101 sqrecii 14173 i4 14194 facp1 14264 hashf1 14445 binom 15803 prodf1 15864 prodfrec 15868 fprodmul 15931 fprodge1 15966 fallfac0 15999 binomfallfac 16012 pwp1fsum 16362 rpmul 16624 2503lem2 17101 2503lem3 17102 4001lem4 17107 abvtrivd 20714 pzriprng1ALT 21416 iimulcl 24854 dvexp 25879 dvef 25906 mulcxplem 26612 cxpmul2 26617 dvsqrt 26670 dvcnsqrt 26672 abscxpbnd 26682 1cubr 26768 dchrmulcl 27176 dchr1cl 27178 dchrinvcl 27180 lgslem3 27226 lgsval2lem 27234 lgsneg 27248 lgsdilem 27251 lgsdir 27259 lgsdi 27261 lgsquad2lem1 27311 lgsquad2lem2 27312 dchrisum0flblem2 27436 rpvmasum2 27439 mudivsum 27457 pntibndlem2 27518 axlowdimlem6 28752 hisubcomi 30908 lnophmlem2 31821 1nei 32513 1neg1t1neg1 32514 sgnmul 34157 hgt750lem2 34279 subfacval2 34792 faclim2 35337 knoppndvlem18 35999 lcmineqlem12 41506 pell1234qrmulcl 42266 pellqrex 42290 imsqrtvalex 43067 binomcxplemnotnn0 43784 dvnprodlem3 45327 stoweidlem13 45392 stoweidlem16 45395 wallispi 45449 wallispi2lem2 45451 2exp340mod341 47064 8exp8mod9 47067 nn0sumshdiglemB 47684 |
Copyright terms: Public domain | W3C validator |