nn0addcld - Intuitionistic Logic Explorer

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

Theorem nn0addcld 9628

Description: Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)

**Hypotheses**
Ref	Expression
nn0red.1
nn0addcld.2

**Assertion**
Ref	Expression
nn0addcld

**Proof of Theorem nn0addcld**
Step	Hyp	Ref	Expression
1		nn0red.1	. 2
2		nn0addcld.2	. 2
3		nn0addcl 9602	. 2 $/\$
4	1, 2, 3	syl2anc 415	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4

wcel 2209 (class class class)co 6085

caddc 8182

cn0 9567

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-ext 2220 ax-sep 4249 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-addcom 8279 ax-addass 8281 ax-i2m1 8284 ax-0id 8287

This proof depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-rab 2537 df-v 2823 df-un 3224 df-in 3226 df-ss 3233 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-br 4131 df-iota 5337 df-fv 5385 df-ov 6088 df-inn 9307 df-n0 9568

This theorem is used by: modsumfzodifsn 10846 expaddzap 11033 nn0opthlem1d 11172 nn0opthlem2d 11173 nn0opthd 11174 nn0opth2d 11175 bccl 11219 ccatfvalfi 11374 ccatcl 11375 ccatalpha 11395 swrdccat2 11457 mertenslemi1 12318 bitsmod 12739 bitsinv1lem 12744 pcpremul 13092 gzabssqcl 13180 4sqlem2 13188 mul4sq 13193 4sqlemsdc 13199 4sqlem12 13201 4sqlem14 13203 4sqlem16 13205 mplsubgfilemcl 15139 plymullem 15900 lgseisenlem2 16288 2sqlem8 16340 vtxdgfif 16632 clwwlknccat 16762