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	⊢ ( 𝐴 ∈ N → ¬ ( 𝐴 +N 𝐵 ) = 𝐴 )

Proof

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