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

 Description: Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.)
Assertion
Ref Expression
nnaddcl ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ)

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5794 . . . . 5 (𝑥 = 1 → (𝐴 + 𝑥) = (𝐴 + 1))
21eleq1d 2210 . . . 4 (𝑥 = 1 → ((𝐴 + 𝑥) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
32imbi2d 229 . . 3 (𝑥 = 1 → ((𝐴 ∈ ℕ → (𝐴 + 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)))
4 oveq2 5794 . . . . 5 (𝑥 = 𝑦 → (𝐴 + 𝑥) = (𝐴 + 𝑦))
54eleq1d 2210 . . . 4 (𝑥 = 𝑦 → ((𝐴 + 𝑥) ∈ ℕ ↔ (𝐴 + 𝑦) ∈ ℕ))
65imbi2d 229 . . 3 (𝑥 = 𝑦 → ((𝐴 ∈ ℕ → (𝐴 + 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 + 𝑦) ∈ ℕ)))
7 oveq2 5794 . . . . 5 (𝑥 = (𝑦 + 1) → (𝐴 + 𝑥) = (𝐴 + (𝑦 + 1)))
87eleq1d 2210 . . . 4 (𝑥 = (𝑦 + 1) → ((𝐴 + 𝑥) ∈ ℕ ↔ (𝐴 + (𝑦 + 1)) ∈ ℕ))
98imbi2d 229 . . 3 (𝑥 = (𝑦 + 1) → ((𝐴 ∈ ℕ → (𝐴 + 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 + (𝑦 + 1)) ∈ ℕ)))
10 oveq2 5794 . . . . 5 (𝑥 = 𝐵 → (𝐴 + 𝑥) = (𝐴 + 𝐵))
1110eleq1d 2210 . . . 4 (𝑥 = 𝐵 → ((𝐴 + 𝑥) ∈ ℕ ↔ (𝐴 + 𝐵) ∈ ℕ))
1211imbi2d 229 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ ℕ → (𝐴 + 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 + 𝐵) ∈ ℕ)))
13 peano2nn 8785 . . 3 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
14 peano2nn 8785 . . . . . 6 ((𝐴 + 𝑦) ∈ ℕ → ((𝐴 + 𝑦) + 1) ∈ ℕ)
15 nncn 8781 . . . . . . . 8 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
16 nncn 8781 . . . . . . . 8 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
17 ax-1cn 7766 . . . . . . . . 9 1 ∈ ℂ
18 addass 7803 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 𝑦) + 1) = (𝐴 + (𝑦 + 1)))
1917, 18mp3an3 1305 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐴 + 𝑦) + 1) = (𝐴 + (𝑦 + 1)))
2015, 16, 19syl2an 287 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 + 𝑦) + 1) = (𝐴 + (𝑦 + 1)))
2120eleq1d 2210 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (((𝐴 + 𝑦) + 1) ∈ ℕ ↔ (𝐴 + (𝑦 + 1)) ∈ ℕ))
2214, 21syl5ib 153 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 + 𝑦) ∈ ℕ → (𝐴 + (𝑦 + 1)) ∈ ℕ))
2322expcom 115 . . . 4 (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 + 𝑦) ∈ ℕ → (𝐴 + (𝑦 + 1)) ∈ ℕ)))
2423a2d 26 . . 3 (𝑦 ∈ ℕ → ((𝐴 ∈ ℕ → (𝐴 + 𝑦) ∈ ℕ) → (𝐴 ∈ ℕ → (𝐴 + (𝑦 + 1)) ∈ ℕ)))
253, 6, 9, 12, 13, 24nnind 8789 . 2 (𝐵 ∈ ℕ → (𝐴 ∈ ℕ → (𝐴 + 𝐵) ∈ ℕ))
2625impcom 124 1 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481  (class class class)co 5786  ℂcc 7671  1c1 7674   + caddc 7676  ℕcn 8773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123  ax-sep 4056  ax-cnex 7764  ax-resscn 7765  ax-1cn 7766  ax-1re 7767  ax-addrcl 7770  ax-addass 7775 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1738  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ral 2423  df-rex 2424  df-rab 2427  df-v 2693  df-un 3082  df-in 3084  df-ss 3091  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-br 3940  df-iota 5100  df-fv 5143  df-ov 5789  df-inn 8774 This theorem is referenced by:  nnmulcl  8794  nn2ge  8806  nnaddcld  8821  nnnn0addcl  9060  nn0addcl  9065  9p1e10  9237
 Copyright terms: Public domain W3C validator