![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnaddcld | Structured version Visualization version GIF version |
Description: Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnge1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
nnmulcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℕ) |
Ref | Expression |
---|---|
nnaddcld | ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnge1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
2 | nnmulcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℕ) | |
3 | nnaddcl 11497 | . 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2079 (class class class)co 7007 + caddc 10375 ℕcn 11475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-1cn 10430 ax-addcl 10432 ax-addass 10437 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-ral 3108 df-rex 3109 df-reu 3110 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-ov 7010 df-om 7428 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-nn 11476 |
This theorem is referenced by: relexpaddnn 14232 pythagtriplem4 15973 pythagtriplem6 15975 pythagtriplem7 15976 pythagtriplem11 15979 pythagtriplem13 15981 pythagtriplem15 15983 vdwlem1 16134 vdwlem3 16136 vdwlem5 16138 vdwlem6 16139 vdwlem8 16141 vdwlem9 16142 vdwlem10 16143 vdwlem11 16144 prmgaplem2 16203 prmgaplcmlem2 16205 gsumccat 17805 aaliou3lem8 24605 lgsqrlem2 25593 lgseisenlem2 25622 2sqmod 25682 mdetlap 30668 ballotlem5 31330 faclimlem1 32528 faclimlem2 32529 faclim2 32533 fmtnoprmfac2 43165 gbowpos 43360 |
Copyright terms: Public domain | W3C validator |