MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4t2e8 Structured version   Visualization version   GIF version

Theorem 4t2e8 11448
Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
4t2e8 (4 · 2) = 8

Proof of Theorem 4t2e8
StepHypRef Expression
1 4cn 11360 . . 3 4 ∈ ℂ
21times2i 11420 . 2 (4 · 2) = (4 + 4)
3 4p4e8 11435 . 2 (4 + 4) = 8
42, 3eqtri 2787 1 (4 · 2) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  (class class class)co 6844   + caddc 10194   · cmul 10196  2c2 11329  4c4 11331  8c8 11335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-mulcl 10253  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-1rid 10261  ax-cnre 10264
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-iota 6033  df-fv 6078  df-ov 6847  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343
This theorem is referenced by:  8th4div3  11500  4t3e12  11842  sq4e2t8  13172  cu2  13173  sqoddm1div8  13238  cos2bnd  15203  2exp8  16073  8nprm  16095  19prm  16101  139prm  16107  1259lem2  16115  1259lem3  16116  1259lem4  16117  1259lem5  16118  2503lem1  16120  2503lem2  16121  4001lem1  16124  4001lem2  16125  4001lem3  16126  4001lem4  16127  quart1lem  24876  quart1  24877  quartlem1  24878  log2tlbnd  24966  log2ub  24970  bpos1  25302  bposlem8  25310  lgsdir2lem2  25345  2lgslem3a  25415  2lgslem3b  25416  2lgslem3c  25417  2lgslem3d  25418  2lgsoddprmlem2  25428  2lgsoddprmlem3c  25431  2lgsoddprmlem3d  25432  chebbnd1lem2  25453  chebbnd1lem3  25454  pntlemr  25585  ex-exp  27769  fmtno4prmfac  42163  139prmALT  42190  2exp7  42193  mod42tp1mod8  42198  3exp4mod41  42212  41prothprm  42215  8even  42301
  Copyright terms: Public domain W3C validator