Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2t0e0 | Structured version Visualization version GIF version |
Description: 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
2t0e0 | ⊢ (2 · 0) = 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 11784 | . 2 ⊢ 2 ∈ ℂ | |
2 | 1 | mul01i 10901 | 1 ⊢ (2 · 0) = 0 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 (class class class)co 7164 0cc0 10608 · cmul 10613 2c2 11764 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-ov 7167 df-er 8313 df-en 8549 df-dom 8550 df-sdom 8551 df-pnf 10748 df-mnf 10749 df-ltxr 10751 df-2 11772 |
This theorem is referenced by: expmulnbnd 13681 iseraltlem2 15125 fsumcube 15499 2mulprm 16127 1259lem5 16564 smndex2dnrinv 18189 ablsimpgfindlem1 19341 htpycc 23725 pco0 23759 pcohtpylem 23764 pcopt2 23768 pcoass 23769 pcorevlem 23771 pilem2 25191 cospi 25209 sin2pi 25212 pythag 25547 bclbnd 26008 bposlem1 26012 bposlem2 26013 lgsquadlem1 26108 lgsquadlem2 26109 log2sumbnd 26272 pntrlog2bndlem4 26308 finsumvtxdg2size 27484 cdj3lem1 30361 wrdt2ind 30792 420lcm8e840 39628 dirkertrigeqlem3 43167 fourierdlem62 43235 2exp340mod341 44703 1odd 44883 ackval2012 45555 2itscp 45645 |
Copyright terms: Public domain | W3C validator |