Metamath Proof Explorer


Theorem nnacl

Description: Closure of addition of natural numbers. Proposition 8.9 of TakeutiZaring p. 59. (Contributed by NM, 20-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nnacl A ω B ω A + 𝑜 B ω

Proof

Step Hyp Ref Expression
1 oveq2 x = B A + 𝑜 x = A + 𝑜 B
2 1 eleq1d x = B A + 𝑜 x ω A + 𝑜 B ω
3 2 imbi2d x = B A ω A + 𝑜 x ω A ω A + 𝑜 B ω
4 oveq2 x = A + 𝑜 x = A + 𝑜
5 4 eleq1d x = A + 𝑜 x ω A + 𝑜 ω
6 oveq2 x = y A + 𝑜 x = A + 𝑜 y
7 6 eleq1d x = y A + 𝑜 x ω A + 𝑜 y ω
8 oveq2 x = suc y A + 𝑜 x = A + 𝑜 suc y
9 8 eleq1d x = suc y A + 𝑜 x ω A + 𝑜 suc y ω
10 nna0 A ω A + 𝑜 = A
11 10 eleq1d A ω A + 𝑜 ω A ω
12 11 ibir A ω A + 𝑜 ω
13 peano2 A + 𝑜 y ω suc A + 𝑜 y ω
14 nnasuc A ω y ω A + 𝑜 suc y = suc A + 𝑜 y
15 14 eleq1d A ω y ω A + 𝑜 suc y ω suc A + 𝑜 y ω
16 13 15 syl5ibr A ω y ω A + 𝑜 y ω A + 𝑜 suc y ω
17 16 expcom y ω A ω A + 𝑜 y ω A + 𝑜 suc y ω
18 5 7 9 12 17 finds2 x ω A ω A + 𝑜 x ω
19 3 18 vtoclga B ω A ω A + 𝑜 B ω
20 19 impcom A ω B ω A + 𝑜 B ω