![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addnidpig | GIF version |
Description: There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) |
Ref | Expression |
---|---|
addnidpig | ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ¬ (𝐴 +N 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pinn 6550 | . . 3 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω) | |
2 | elni2 6555 | . . . 4 ⊢ (𝐵 ∈ N ↔ (𝐵 ∈ ω ∧ ∅ ∈ 𝐵)) | |
3 | nnaordi 6140 | . . . . . . 7 ⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅ ∈ 𝐵 → (𝐴 +𝑜 ∅) ∈ (𝐴 +𝑜 𝐵))) | |
4 | nna0 6111 | . . . . . . . . . 10 ⊢ (𝐴 ∈ ω → (𝐴 +𝑜 ∅) = 𝐴) | |
5 | 4 | eleq1d 2148 | . . . . . . . . 9 ⊢ (𝐴 ∈ ω → ((𝐴 +𝑜 ∅) ∈ (𝐴 +𝑜 𝐵) ↔ 𝐴 ∈ (𝐴 +𝑜 𝐵))) |
6 | nnord 4354 | . . . . . . . . . . . 12 ⊢ (𝐴 ∈ ω → Ord 𝐴) | |
7 | ordirr 4287 | . . . . . . . . . . . 12 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) | |
8 | 6, 7 | syl 14 | . . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → ¬ 𝐴 ∈ 𝐴) |
9 | eleq2 2143 | . . . . . . . . . . . 12 ⊢ ((𝐴 +𝑜 𝐵) = 𝐴 → (𝐴 ∈ (𝐴 +𝑜 𝐵) ↔ 𝐴 ∈ 𝐴)) | |
10 | 9 | notbid 625 | . . . . . . . . . . 11 ⊢ ((𝐴 +𝑜 𝐵) = 𝐴 → (¬ 𝐴 ∈ (𝐴 +𝑜 𝐵) ↔ ¬ 𝐴 ∈ 𝐴)) |
11 | 8, 10 | syl5ibrcom 155 | . . . . . . . . . 10 ⊢ (𝐴 ∈ ω → ((𝐴 +𝑜 𝐵) = 𝐴 → ¬ 𝐴 ∈ (𝐴 +𝑜 𝐵))) |
12 | 11 | con2d 587 | . . . . . . . . 9 ⊢ (𝐴 ∈ ω → (𝐴 ∈ (𝐴 +𝑜 𝐵) → ¬ (𝐴 +𝑜 𝐵) = 𝐴)) |
13 | 5, 12 | sylbid 148 | . . . . . . . 8 ⊢ (𝐴 ∈ ω → ((𝐴 +𝑜 ∅) ∈ (𝐴 +𝑜 𝐵) → ¬ (𝐴 +𝑜 𝐵) = 𝐴)) |
14 | 13 | adantl 271 | . . . . . . 7 ⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐴 +𝑜 ∅) ∈ (𝐴 +𝑜 𝐵) → ¬ (𝐴 +𝑜 𝐵) = 𝐴)) |
15 | 3, 14 | syld 44 | . . . . . 6 ⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅ ∈ 𝐵 → ¬ (𝐴 +𝑜 𝐵) = 𝐴)) |
16 | 15 | expcom 114 | . . . . 5 ⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (∅ ∈ 𝐵 → ¬ (𝐴 +𝑜 𝐵) = 𝐴))) |
17 | 16 | imp32 253 | . . . 4 ⊢ ((𝐴 ∈ ω ∧ (𝐵 ∈ ω ∧ ∅ ∈ 𝐵)) → ¬ (𝐴 +𝑜 𝐵) = 𝐴) |
18 | 2, 17 | sylan2b 281 | . . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) → ¬ (𝐴 +𝑜 𝐵) = 𝐴) |
19 | 1, 18 | sylan 277 | . 2 ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ¬ (𝐴 +𝑜 𝐵) = 𝐴) |
20 | addpiord 6557 | . . 3 ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +𝑜 𝐵)) | |
21 | 20 | eqeq1d 2090 | . 2 ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = 𝐴 ↔ (𝐴 +𝑜 𝐵) = 𝐴)) |
22 | 19, 21 | mtbird 631 | 1 ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ¬ (𝐴 +N 𝐵) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 102 = wceq 1285 ∈ wcel 1434 ∅c0 3252 Ord word 4119 ωcom 4333 (class class class)co 5537 +𝑜 coa 6056 Ncnpi 6513 +N cpli 6514 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-coll 3895 ax-sep 3898 ax-nul 3906 ax-pow 3950 ax-pr 3966 ax-un 4190 ax-setind 4282 ax-iinf 4331 |
This theorem depends on definitions: df-bi 115 df-dc 777 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-csb 2910 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-nul 3253 df-pw 3386 df-sn 3406 df-pr 3407 df-op 3409 df-uni 3604 df-int 3639 df-iun 3682 df-br 3788 df-opab 3842 df-mpt 3843 df-tr 3878 df-id 4050 df-iord 4123 df-on 4125 df-suc 4128 df-iom 4334 df-xp 4371 df-rel 4372 df-cnv 4373 df-co 4374 df-dm 4375 df-rn 4376 df-res 4377 df-ima 4378 df-iota 4891 df-fun 4928 df-fn 4929 df-f 4930 df-f1 4931 df-fo 4932 df-f1o 4933 df-fv 4934 df-ov 5540 df-oprab 5541 df-mpt2 5542 df-1st 5792 df-2nd 5793 df-recs 5948 df-irdg 6013 df-oadd 6063 df-ni 6545 df-pli 6546 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |