This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 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 biimtrdi ⊢ ( ¬ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = 𝐴 → ¬ 𝐴 ∈ N ) )
31 30 con2d ⊢ ( ¬ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ∈ N → ¬ ( 𝐴 +N 𝐵 ) = 𝐴 ) )
32 23 31 pm2.61i ⊢ ( 𝐴 ∈ N → ¬ ( 𝐴 +N 𝐵 ) = 𝐴 )