Theorem 5t2e10 12535

Description: 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)

Assertion

Ref	Expression
5t2e10	⊢ (5 · 2) = ;10

Proof of Theorem 5t2e10

Step	Hyp	Ref	Expression
1		5nn0 12251	. 2 ⊢ 5 ∈ ℕ0
2		1nn0 12247	. 2 ⊢ 1 ∈ ℕ0
3		df-2 12034	. 2 ⊢ 2 = (1 + 1)
4		5cn 12059	. . 3 ⊢ 5 ∈ ℂ
5	4	mulid1i 10977	. 2 ⊢ (5 · 1) = 5
6		5p5e10 12506	. 2 ⊢ (5 + 5) = ;10
7	1, 2, 3, 5, 6	4t3lem 12532	1 ⊢ (5 · 2) = ;10

Syntax hints:   = wceq 1539  (class class class)co 7277  0cc0 10869  1c1 10870   · cmul 10874  2c2 12026  5c5 12029  ;cdc 12435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pow 5290  ax-pr 5354  ax-un 7588  ax-resscn 10926  ax-1cn 10927  ax-icn 10928  ax-addcl 10929  ax-addrcl 10930  ax-mulcl 10931  ax-mulrcl 10932  ax-mulcom 10933  ax-addass 10934  ax-mulass 10935  ax-distr 10936  ax-i2m1 10937  ax-1ne0 10938  ax-1rid 10939  ax-rnegex 10940  ax-rrecex 10941  ax-cnre 10942  ax-pre-lttri 10943  ax-pre-lttrn 10944  ax-pre-ltadd 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5077  df-opab 5139  df-mpt 5160  df-tr 5194  df-id 5491  df-eprel 5497  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-pred 6204  df-ord 6271  df-on 6272  df-lim 6273  df-suc 6274  df-iota 6393  df-fun 6437  df-fn 6438  df-f 6439  df-f1 6440  df-fo 6441  df-f1o 6442  df-fv 6443  df-ov 7280  df-om 7713  df-2nd 7832  df-frecs 8095  df-wrecs 8126  df-recs 8200  df-rdg 8239  df-er 8496  df-en 8732  df-dom 8733  df-sdom 8734  df-pnf 11009  df-mnf 11010  df-ltxr 11012  df-nn 11972  df-2 12034  df-3 12035  df-4 12036  df-5 12037  df-6 12038  df-7 12039  df-8 12040  df-9 12041  df-n0 12232  df-dec 12436

This theorem is referenced by:  5t3e15  12536  dec2dvds  16762  dec5dvds  16763  dec5nprm  16765  dec2nprm  16766  2exp16  16790  10nprm  16813  1259lem1  16830  1259lem4  16833  2503lem1  16836  2503lem2  16837  2503lem3  16838  4001lem1  16840  4001lem4  16843  4001prm  16844  log2ublem3  26096  log2ub  26097  bclbnd  26426  bpos1  26429  bposlem4  26433  bposlem5  26434  bposlem8  26437  ex-fac  28812  12gcd5e1  40008  12lcm5e60  40013  lcmineqlem23  40056  3lexlogpow5ineq5  40065  aks4d1p1p7  40079  aks4d1p1  40081  127prm  45018  41prothprm  45038  2exp340mod341  45152