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

Theorem decaddi 12150
Description: Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
Hypotheses
Ref Expression
decaddi.1 𝐴 ∈ ℕ0
decaddi.2 𝐵 ∈ ℕ0
decaddi.3 𝑁 ∈ ℕ0
decaddi.4 𝑀 = 𝐴𝐵
decaddi.5 (𝐵 + 𝑁) = 𝐶
Assertion
Ref Expression
decaddi (𝑀 + 𝑁) = 𝐴𝐶

Proof of Theorem decaddi
StepHypRef Expression
1 decaddi.1 . 2 𝐴 ∈ ℕ0
2 decaddi.2 . 2 𝐵 ∈ ℕ0
3 0nn0 11904 . 2 0 ∈ ℕ0
4 decaddi.3 . 2 𝑁 ∈ ℕ0
5 decaddi.4 . 2 𝑀 = 𝐴𝐵
64dec0h 12112 . 2 𝑁 = 0𝑁
71nn0cni 11901 . . 3 𝐴 ∈ ℂ
87addid1i 10819 . 2 (𝐴 + 0) = 𝐴
9 decaddi.5 . 2 (𝐵 + 𝑁) = 𝐶
101, 2, 3, 4, 5, 6, 8, 9decadd 12144 1 (𝑀 + 𝑁) = 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1531  wcel 2108  (class class class)co 7148  0cc0 10529   + caddc 10532  0cn0 11889  cdc 12090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-om 7573  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-dec 12091
This theorem is referenced by:  4t4e16  12189  6t3e18  12195  7t4e28  12201  7t7e49  12204  2exp16  16416  17prm  16442  23prm  16444  prmlem2  16445  37prm  16446  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem2  16467  4001lem4  16469  4001prm  16470  log2ublem3  25518  log2ub  25519  birthday  25524  ex-fac  28222  hgt750lem2  31916  decaddcom  39160  sqn5i  39161  sqdeccom12  39165  sq3deccom12  39166  235t711  39167  ex-decpmul  39168  fmtno5lem1  43705  fmtno5lem2  43706  fmtno5lem4  43708  257prm  43713  fmtno4prmfac  43724  fmtno4nprmfac193  43726  fmtno5faclem1  43731  fmtno5faclem2  43732  fmtno5faclem3  43733  139prmALT  43749  127prm  43753  2exp11  43755  11t31e341  43887
  Copyright terms: Public domain W3C validator