Theorem nnacl 5487

Description: Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (The proof was shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
nnacl	|- ((A e. om /\ B e. om) -> (A +o B) e. om)

Proof of Theorem nnacl

Step	Hyp	Ref	Expression
1		opreq2 5026	. . . . 5 |- (x = B -> (A +o x) = (A +o B))
2	1	eleq1d 2239	. . . 4 |- (x = B -> ((A +o x) e. om <-> (A +o B) e. om))
3	2	imbi2d 380	. . 3 |- (x = B -> ((A e. om -> (A +o x) e. om) <-> (A e. om -> (A +o B) e. om)))
4		opreq2 5026	. . . . 5 |- (x = (/) -> (A +o x) = (A +o (/)))
5	4	eleq1d 2239	. . . 4 |- (x = (/) -> ((A +o x) e. om <-> (A +o (/)) e. om))
6		opreq2 5026	. . . . 5 |- (x = y -> (A +o x) = (A +o y))
7	6	eleq1d 2239	. . . 4 |- (x = y -> ((A +o x) e. om <-> (A +o y) e. om))
8		opreq2 5026	. . . . 5 |- (x = suc y -> (A +o x) = (A +o suc y))
9	8	eleq1d 2239	. . . 4 |- (x = suc y -> ((A +o x) e. om <-> (A +o suc y) e. om))
10		nna0 5481	. . . . . 6 |- (A e. om -> (A +o (/)) = A)
11	10	eleq1d 2239	. . . . 5 |- (A e. om -> ((A +o (/)) e. om <-> A e. om))
12	11	ibir 299	. . . 4 |- (A e. om -> (A +o (/)) e. om)
13		peano2 4138	. . . . . 6 |- ((A +o y) e. om -> suc (A +o y) e. om)
14		nnasuc 5483	. . . . . . 7 |- ((A e. om /\ y e. om) -> (A +o suc y) = suc (A +o y))
15	14	eleq1d 2239	. . . . . 6 |- ((A e. om /\ y e. om) -> ((A +o suc y) e. om <-> suc (A +o y) e. om))
16	13, 15	syl5ibr 278	. . . . 5 |- ((A e. om /\ y e. om) -> ((A +o y) e. om -> (A +o suc y) e. om))
17	16	expcom 495	. . . 4 |- (y e. om -> (A e. om -> ((A +o y) e. om -> (A +o suc y) e. om)))
18	5, 7, 9, 12, 17	finds2 4146	. . 3 |- (x e. om -> (A e. om -> (A +o x) e. om))
19	3, 18	vtoclga 2624	. 2 |- (B e. om -> (A e. om -> (A +o B) e. om))
20	19	impcom 490	1 |- ((A e. om /\ B e. om) -> (A +o B) e. om)

Syntax hints:   -> wi 3   /\ wa 433   = wceq 1615   e. wcel 1617  (/)c0 3114  suc csuc 3845  omcom 4117  (class class class)co 5020   +o coa 5381

This theorem is referenced by:  nnmcl 5488  nnarcl 5490  oaabslem 5509  nneob 5513  unfilem1 5904  unfi 5907  nnacda 6328  nnaun 6329  pwsdompw 6331  nnacdaOLD 6532  nnaunOLD 6533  addclpi 6615  hashgadd 14605  nnacli 14743  omssadd 14745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-fv 4179  df-opr 5022  df-oprab 5023  df-rdg 5344  df-oadd 5386

Copyright terms: Public domain