ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nn0addcl GIF version

Theorem nn0addcl 9236
Description: Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
Assertion
Ref Expression
nn0addcl ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ0)

Proof of Theorem nn0addcl
StepHypRef Expression
1 nnsscn 8949 . 2 ℕ ⊆ ℂ
2 id 19 . . 3 (ℕ ⊆ ℂ → ℕ ⊆ ℂ)
3 df-n0 9202 . . 3 0 = (ℕ ∪ {0})
4 nnaddcl 8964 . . . 4 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
54adantl 277 . . 3 ((ℕ ⊆ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑀 + 𝑁) ∈ ℕ)
62, 3, 5un0addcl 9234 . 2 ((ℕ ⊆ ℂ ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 + 𝑁) ∈ ℕ0)
71, 6mpan 424 1 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ0)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2160  wss 3144  (class class class)co 5892  cc 7834   + caddc 7839  cn 8944  0cn0 9201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4136  ax-cnex 7927  ax-resscn 7928  ax-1cn 7929  ax-1re 7930  ax-icn 7931  ax-addcl 7932  ax-addrcl 7933  ax-mulcl 7934  ax-addcom 7936  ax-addass 7938  ax-i2m1 7941  ax-0id 7944
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-iota 5193  df-fv 5240  df-ov 5895  df-inn 8945  df-n0 9202
This theorem is referenced by:  nn0addcli  9238  peano2nn0  9241  nn0addcld  9258  nn0readdcl  9260  difelfznle  10160  elfzodifsumelfzo  10226  expadd  10588  faclbnd6  10751  facavg  10753  fsumnn0cl  11438  bcxmas  11524  eftlub  11725  4sqlem1  12415  nn0subm  13879  2sqlem7  14906
  Copyright terms: Public domain W3C validator