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 
|- ( A e. N. -> -. ( A +N B ) = A )

Proof

Step Hyp Ref Expression
1 pinn 
 |-  ( A e. N. -> A e. _om )
2 elni2 
 |-  ( B e. N. <-> ( B e. _om /\ (/) e. B ) )
3 nnaordi 
 |-  ( ( B e. _om /\ A e. _om ) -> ( (/) e. B -> ( A +o (/) ) e. ( A +o B ) ) )
4 nna0 
 |-  ( A e. _om -> ( A +o (/) ) = A )
5 4 eleq1d 
 |-  ( A e. _om -> ( ( A +o (/) ) e. ( A +o B ) <-> A e. ( A +o B ) ) )
6 nnord 
 |-  ( A e. _om -> Ord A )
7 ordirr 
 |-  ( Ord A -> -. A e. A )
8 6 7 syl 
 |-  ( A e. _om -> -. A e. A )
9 eleq2 
 |-  ( ( A +o B ) = A -> ( A e. ( A +o B ) <-> A e. A ) )
10 9 notbid 
 |-  ( ( A +o B ) = A -> ( -. A e. ( A +o B ) <-> -. A e. A ) )
11 8 10 syl5ibrcom 
 |-  ( A e. _om -> ( ( A +o B ) = A -> -. A e. ( A +o B ) ) )
12 11 con2d 
 |-  ( A e. _om -> ( A e. ( A +o B ) -> -. ( A +o B ) = A ) )
13 5 12 sylbid 
 |-  ( A e. _om -> ( ( A +o (/) ) e. ( A +o B ) -> -. ( A +o B ) = A ) )
14 13 adantl 
 |-  ( ( B e. _om /\ A e. _om ) -> ( ( A +o (/) ) e. ( A +o B ) -> -. ( A +o B ) = A ) )
15 3 14 syld 
 |-  ( ( B e. _om /\ A e. _om ) -> ( (/) e. B -> -. ( A +o B ) = A ) )
16 15 expcom 
 |-  ( A e. _om -> ( B e. _om -> ( (/) e. B -> -. ( A +o B ) = A ) ) )
17 16 imp32 
 |-  ( ( A e. _om /\ ( B e. _om /\ (/) e. B ) ) -> -. ( A +o B ) = A )
18 2 17 sylan2b 
 |-  ( ( A e. _om /\ B e. N. ) -> -. ( A +o B ) = A )
19 1 18 sylan 
 |-  ( ( A e. N. /\ B e. N. ) -> -. ( A +o B ) = A )
20 addpiord 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )
21 20 eqeq1d 
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = A <-> ( A +o B ) = A ) )
22 19 21 mtbird 
 |-  ( ( A e. N. /\ B e. N. ) -> -. ( A +N B ) = A )
23 22 a1d 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A e. N. -> -. ( A +N B ) = A ) )
24 dmaddpi 
 |-  dom +N = ( N. X. N. )
25 24 ndmov 
 |-  ( -. ( A e. N. /\ B e. N. ) -> ( A +N B ) = (/) )
26 25 eqeq1d 
 |-  ( -. ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = A <-> (/) = A ) )
27 0npi 
 |-  -. (/) e. N.
28 eleq1 
 |-  ( (/) = A -> ( (/) e. N. <-> A e. N. ) )
29 27 28 mtbii 
 |-  ( (/) = A -> -. A e. N. )
30 26 29 biimtrdi 
 |-  ( -. ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = A -> -. A e. N. ) )
31 30 con2d 
 |-  ( -. ( A e. N. /\ B e. N. ) -> ( A e. N. -> -. ( A +N B ) = A ) )
32 23 31 pm2.61i 
 |-  ( A e. N. -> -. ( A +N B ) = A )