![]() |
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 10391 | . 2 ⊢ 1 ∈ ℂ | |
2 | 1 | mulid1i 10442 | 1 ⊢ (1 · 1) = 1 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 (class class class)co 6974 1c1 10334 · cmul 10338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-mulcl 10395 ax-mulcom 10397 ax-mulass 10399 ax-distr 10400 ax-1rid 10403 ax-cnre 10406 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-iota 6149 df-fv 6193 df-ov 6977 |
This theorem is referenced by: neg1mulneg1e1 11658 addltmul 11681 1exp 13271 expge1 13279 mulexp 13281 mulexpz 13282 expaddz 13286 m1expeven 13289 sqrecii 13359 i4 13380 facp1 13451 hashf1 13626 binom 15043 prodf1 15105 prodfrec 15109 fprodmul 15172 fprodge1 15207 fallfac0 15240 binomfallfac 15253 pwp1fsum 15600 rpmul 15857 2503lem2 16325 2503lem3 16326 4001lem4 16331 abvtrivd 19345 iimulcl 23256 dvexp 24265 dvef 24292 mulcxplem 24980 cxpmul2 24985 dvsqrt 25036 dvcnsqrt 25038 abscxpbnd 25047 1cubr 25133 dchrmulcl 25539 dchr1cl 25541 dchrinvcl 25543 lgslem3 25589 lgsval2lem 25597 lgsneg 25611 lgsdilem 25614 lgsdir 25622 lgsdi 25624 lgsquad2lem1 25674 lgsquad2lem2 25675 dchrisum0flblem2 25799 rpvmasum2 25802 mudivsum 25820 pntibndlem2 25881 axlowdimlem6 26448 hisubcomi 28672 lnophmlem2 29587 1nei 30245 1neg1t1neg1 30246 sgnmul 31475 hgt750lem2 31600 subfacval2 32048 faclim2 32529 knoppndvlem18 33417 pell1234qrmulcl 38877 pellqrex 38901 binomcxplemnotnn0 40133 dvnprodlem3 41688 stoweidlem13 41754 stoweidlem16 41757 wallispi 41811 wallispi2lem2 41813 2exp340mod341 43291 8exp8mod9 43294 nn0sumshdiglemB 44073 |
Copyright terms: Public domain | W3C validator |