![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2t1e2 | Structured version Visualization version GIF version |
Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Ref | Expression |
---|---|
2t1e2 | ⊢ (2 · 1) = 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 12228 | . 2 ⊢ 2 ∈ ℂ | |
2 | 1 | mulid1i 11159 | 1 ⊢ (2 · 1) = 2 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 (class class class)co 7357 1c1 11052 · cmul 11056 2c2 12208 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-mulcl 11113 ax-mulcom 11115 ax-mulass 11117 ax-distr 11118 ax-1rid 11121 ax-cnre 11124 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-iota 6448 df-fv 6504 df-ov 7360 df-2 12216 |
This theorem is referenced by: decbin2 12759 expubnd 14082 01sqrexlem7 15133 trirecip 15748 bpoly3 15941 fsumcube 15943 ege2le3 15972 cos2tsin 16061 cos2bnd 16070 odd2np1 16223 opoe 16245 flodddiv4 16295 2mulprm 16569 pythagtriplem4 16691 2503lem2 17010 2503lem3 17011 4001lem4 17016 4001prm 17017 htpycc 24343 pco1 24378 pcohtpylem 24382 pcopt 24385 pcorevlem 24389 ovolunlem1a 24860 cos2pi 25833 coskpi 25879 dcubic2 26194 dcubic 26196 basellem3 26432 chtublem 26559 bcp1ctr 26627 bclbnd 26628 bposlem1 26632 bposlem2 26633 bposlem5 26636 2lgslem3d1 26751 2sqreultlem 26795 2sqreunnltlem 26798 chebbnd1lem1 26817 chebbnd1lem3 26819 chebbnd1 26820 frgrregord013 29339 ex-ind-dvds 29405 wrdt2ind 31807 knoppndvlem12 34986 heiborlem6 36275 3lexlogpow5ineq1 40511 aks4d1p1 40533 2np3bcnp1 40552 2ap1caineq 40553 flt4lem7 40983 jm2.23 41306 sumnnodd 43861 wallispilem4 44299 wallispi2lem1 44302 wallispi2lem2 44303 wallispi2 44304 stirlinglem11 44315 dirkertrigeqlem1 44329 fouriersw 44462 fmtnorec4 45731 lighneallem2 45788 lighneallem3 45789 3exp4mod41 45798 opoeALTV 45865 fppr2odd 45913 8exp8mod9 45918 ackval2 46758 ackval2012 46767 |
Copyright terms: Public domain | W3C validator |