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

Theorem addclpi 6174
Description: Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.)
Assertion
Ref Expression
addclpi ((A N B N) → (A +N B) N)

Proof of Theorem addclpi
StepHypRef Expression
1 addpiord 6163 . 2 ((A N B N) → (A +N B) = (A +𝑜 B))
2 pinn 6156 . . 3 (A NA 𝜔)
3 pinn 6156 . . . . 5 (B NB 𝜔)
4 nnacl 5963 . . . . 5 ((A 𝜔 B 𝜔) → (A +𝑜 B) 𝜔)
53, 4sylan2 270 . . . 4 ((A 𝜔 B N) → (A +𝑜 B) 𝜔)
6 elni2 6161 . . . . 5 (B N ↔ (B 𝜔 B))
7 nnaordi 5981 . . . . . . . 8 ((B 𝜔 A 𝜔) → (∅ B → (A +𝑜 ∅) (A +𝑜 B)))
8 ne0i 3199 . . . . . . . 8 ((A +𝑜 ∅) (A +𝑜 B) → (A +𝑜 B) ≠ ∅)
97, 8syl6 29 . . . . . . 7 ((B 𝜔 A 𝜔) → (∅ B → (A +𝑜 B) ≠ ∅))
109expcom 109 . . . . . 6 (A 𝜔 → (B 𝜔 → (∅ B → (A +𝑜 B) ≠ ∅)))
1110imp32 244 . . . . 5 ((A 𝜔 (B 𝜔 B)) → (A +𝑜 B) ≠ ∅)
126, 11sylan2b 271 . . . 4 ((A 𝜔 B N) → (A +𝑜 B) ≠ ∅)
13 elni 6155 . . . 4 ((A +𝑜 B) N ↔ ((A +𝑜 B) 𝜔 (A +𝑜 B) ≠ ∅))
145, 12, 13sylanbrc 394 . . 3 ((A 𝜔 B N) → (A +𝑜 B) N)
152, 14sylan 267 . 2 ((A N B N) → (A +𝑜 B) N)
161, 15eqeltrd 2088 1 ((A N B N) → (A +N B) N)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1367  wne 2178  c0 3193  𝜔com 4229  (class class class)co 5425   +𝑜 coa 5902  Ncnpi 6119   +N cpli 6120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1310  ax-7 1311  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-10 1370  ax-11 1371  ax-i12 1372  ax-bnd 1373  ax-4 1374  ax-13 1378  ax-14 1379  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-i5r 1402  ax-ext 1996  ax-coll 3836  ax-sep 3839  ax-nul 3847  ax-pow 3891  ax-pr 3908  ax-un 4109  ax-setind 4193  ax-iinf 4227
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3an 869  df-tru 1227  df-fal 1230  df-nf 1324  df-sb 1620  df-eu 1877  df-mo 1878  df-clab 2001  df-cleq 2007  df-clel 2010  df-nfc 2141  df-ne 2180  df-ral 2281  df-rex 2282  df-reu 2283  df-rab 2285  df-v 2529  df-sbc 2734  df-csb 2822  df-dif 2889  df-un 2891  df-in 2893  df-ss 2900  df-nul 3194  df-pw 3326  df-sn 3346  df-pr 3347  df-op 3349  df-uni 3545  df-int 3580  df-iun 3623  df-br 3729  df-opab 3783  df-mpt 3784  df-tr 3819  df-id 3994  df-iord 4042  df-on 4044  df-suc 4047  df-iom 4230  df-xp 4267  df-rel 4268  df-cnv 4269  df-co 4270  df-dm 4271  df-rn 4272  df-res 4273  df-ima 4274  df-iota 4783  df-fun 4820  df-fn 4821  df-f 4822  df-f1 4823  df-fo 4824  df-f1o 4825  df-fv 4826  df-ov 5428  df-oprab 5429  df-mpt2 5430  df-1st 5679  df-2nd 5680  df-recs 5831  df-irdg 5867  df-oadd 5909  df-ni 6151  df-pli 6152
This theorem is referenced by:  addasspig  6177  distrpig  6180  ltapig  6185  1lt2pi  6187  addcmpblnq  6213  addpipqqslem  6215  addclnq  6221  addassnqg  6228  distrnqg  6233  ltanqg  6246  1lt2nq  6251  ltexnqq  6253  archnqq  6261  prarloclemarch2  6263  nqnq0a  6296
  Copyright terms: Public domain W3C validator