Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  zaddcl Structured version   Unicode version

 Description: Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elz2 10922 . 2
2 elz2 10922 . 2
3 reeanv 2975 . . 3
4 reeanv 2975 . . . . 5
5 nnaddcl 10598 . . . . . . . . . 10
65adantr 463 . . . . . . . . 9
7 nnaddcl 10598 . . . . . . . . . 10
87adantl 464 . . . . . . . . 9
9 nncn 10584 . . . . . . . . . . . 12
10 nncn 10584 . . . . . . . . . . . 12
119, 10anim12i 564 . . . . . . . . . . 11
12 nncn 10584 . . . . . . . . . . . 12
13 nncn 10584 . . . . . . . . . . . 12
1412, 13anim12i 564 . . . . . . . . . . 11
15 addsub4 9898 . . . . . . . . . . 11
1611, 14, 15syl2an 475 . . . . . . . . . 10
1716eqcomd 2410 . . . . . . . . 9
18 rspceov 6317 . . . . . . . . 9
196, 8, 17, 18syl3anc 1230 . . . . . . . 8
20 elz2 10922 . . . . . . . 8
2119, 20sylibr 212 . . . . . . 7
22 oveq12 6287 . . . . . . . 8
2322eleq1d 2471 . . . . . . 7
2421, 23syl5ibrcom 222 . . . . . 6
2524rexlimdvva 2903 . . . . 5
264, 25syl5bir 218 . . . 4
2726rexlimivv 2901 . . 3
283, 27sylbir 213 . 2
291, 2, 28syl2anb 477 1