Metamath Proof Explorer

Theorem addnidpi

Description: There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion addnidpi ⊢ A ∈ 𝑵 → ¬ A + 𝑵 B = A

Proof

Step Hyp Ref Expression
1 pinn ⊢ A ∈ 𝑵 → A ∈ ω
2 elni2 ⊢ B ∈ 𝑵 ↔ B ∈ ω ∧ ∅ ∈ B
3 nnaordi ⊢ B ∈ ω ∧ A ∈ ω → ∅ ∈ B → A + 𝑜 ∅ ∈ A + 𝑜 B
4 nna0 ⊢ A ∈ ω → A + 𝑜 ∅ = A
5 4 eleq1d ⊢ A ∈ ω → A + 𝑜 ∅ ∈ A + 𝑜 B ↔ A ∈ A + 𝑜 B
6 nnord ⊢ A ∈ ω → Ord ⁡ A
7 ordirr ⊢ Ord ⁡ A → ¬ A ∈ A
8 6 7 syl ⊢ A ∈ ω → ¬ A ∈ A
9 eleq2 ⊢ A + 𝑜 B = A → A ∈ A + 𝑜 B ↔ A ∈ A
10 9 notbid ⊢ A + 𝑜 B = A → ¬ A ∈ A + 𝑜 B ↔ ¬ A ∈ A
11 8 10 syl5ibrcom ⊢ A ∈ ω → A + 𝑜 B = A → ¬ A ∈ A + 𝑜 B
12 11 con2d ⊢ A ∈ ω → A ∈ A + 𝑜 B → ¬ A + 𝑜 B = A
13 5 12 sylbid ⊢ A ∈ ω → A + 𝑜 ∅ ∈ A + 𝑜 B → ¬ A + 𝑜 B = A
14 13 adantl ⊢ B ∈ ω ∧ A ∈ ω → A + 𝑜 ∅ ∈ A + 𝑜 B → ¬ A + 𝑜 B = A
15 3 14 syld ⊢ B ∈ ω ∧ A ∈ ω → ∅ ∈ B → ¬ A + 𝑜 B = A
16 15 expcom ⊢ A ∈ ω → B ∈ ω → ∅ ∈ B → ¬ A + 𝑜 B = A
17 16 imp32 ⊢ A ∈ ω ∧ B ∈ ω ∧ ∅ ∈ B → ¬ A + 𝑜 B = A
18 2 17 sylan2b ⊢ A ∈ ω ∧ B ∈ 𝑵 → ¬ A + 𝑜 B = A
19 1 18 sylan ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → ¬ A + 𝑜 B = A
20 addpiord ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = A + 𝑜 B
21 20 eqeq1d ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = A ↔ A + 𝑜 B = A
22 19 21 mtbird ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → ¬ A + 𝑵 B = A
23 22 a1d ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ∈ 𝑵 → ¬ A + 𝑵 B = A
24 dmaddpi ⊢ dom ⁡ + 𝑵 = 𝑵 × 𝑵
25 24 ndmov ⊢ ¬ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = ∅
26 25 eqeq1d ⊢ ¬ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = A ↔ ∅ = A
27 0npi ⊢ ¬ ∅ ∈ 𝑵
28 eleq1 ⊢ ∅ = A → ∅ ∈ 𝑵 ↔ A ∈ 𝑵
29 27 28 mtbii ⊢ ∅ = A → ¬ A ∈ 𝑵
30 26 29 biimtrdi ⊢ ¬ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = A → ¬ A ∈ 𝑵
31 30 con2d ⊢ ¬ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ∈ 𝑵 → ¬ A + 𝑵 B = A
32 23 31 pm2.61i ⊢ A ∈ 𝑵 → ¬ A + 𝑵 B = A