| 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 11213 | . 2 ⊢ 1 ∈ ℂ | |
| 2 | 1 | mulridi 11265 | 1 ⊢ (1 · 1) = 1 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 (class class class)co 7431 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: neg1mulneg1e1 12479 addltmul 12502 1exp 14132 expge1 14140 mulexp 14142 mulexpz 14143 expaddz 14147 m1expeven 14150 sqrecii 14222 i4 14243 facp1 14317 hashf1 14496 binom 15866 prodf1 15927 prodfrec 15931 fprodmul 15996 fprodge1 16031 fallfac0 16064 binomfallfac 16077 pwp1fsum 16428 rpmul 16696 2503lem2 17175 2503lem3 17176 4001lem4 17181 abvtrivd 20833 pzriprng1ALT 21507 iimulcl 24966 dvexp 25991 dvef 26018 mulcxplem 26726 cxpmul2 26731 dvsqrt 26784 dvcnsqrt 26786 abscxpbnd 26796 1cubr 26885 dchrmulcl 27293 dchr1cl 27295 dchrinvcl 27297 lgslem3 27343 lgsval2lem 27351 lgsneg 27365 lgsdilem 27368 lgsdir 27376 lgsdi 27378 lgsquad2lem1 27428 lgsquad2lem2 27429 dchrisum0flblem2 27553 rpvmasum2 27556 mudivsum 27574 pntibndlem2 27635 axlowdimlem6 28962 hisubcomi 31123 lnophmlem2 32036 1nei 32747 1neg1t1neg1 32748 sgnmul 34545 hgt750lem2 34667 subfacval2 35192 faclim2 35748 knoppndvlem18 36530 lcmineqlem12 42041 pell1234qrmulcl 42866 pellqrex 42890 imsqrtvalex 43659 binomcxplemnotnn0 44375 dvnprodlem3 45963 stoweidlem13 46028 stoweidlem16 46031 wallispi 46085 wallispi2lem2 46087 2exp340mod341 47720 8exp8mod9 47723 nn0sumshdiglemB 48541 |
| Copyright terms: Public domain | W3C validator |