Metamath Proof Explorer

Theorem addcanpi

Description: Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion addcanpi 
|- ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = ( A +N C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 addclpi 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A +N B ) e. N. )
2 eleq1 
 |-  ( ( A +N B ) = ( A +N C ) -> ( ( A +N B ) e. N. <-> ( A +N C ) e. N. ) )
3 1 2 imbitrid 
 |-  ( ( A +N B ) = ( A +N C ) -> ( ( A e. N. /\ B e. N. ) -> ( A +N C ) e. N. ) )
4 3 imp 
 |-  ( ( ( A +N B ) = ( A +N C ) /\ ( A e. N. /\ B e. N. ) ) -> ( A +N C ) e. N. )
5 dmaddpi 
 |-  dom +N = ( N. X. N. )
6 0npi 
 |-  -. (/) e. N.
7 5 6 ndmovrcl 
 |-  ( ( A +N C ) e. N. -> ( A e. N. /\ C e. N. ) )
8 simpr 
 |-  ( ( A e. N. /\ C e. N. ) -> C e. N. )
9 4 7 8 3syl 
 |-  ( ( ( A +N B ) = ( A +N C ) /\ ( A e. N. /\ B e. N. ) ) -> C e. N. )
10 addpiord 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )
11 10 adantr 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A +N B ) = ( A +o B ) )
12 addpiord 
 |-  ( ( A e. N. /\ C e. N. ) -> ( A +N C ) = ( A +o C ) )
13 12 adantlr 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A +N C ) = ( A +o C ) )
14 11 13 eqeq12d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A +N B ) = ( A +N C ) <-> ( A +o B ) = ( A +o C ) ) )
15 pinn 
 |-  ( A e. N. -> A e. _om )
16 pinn 
 |-  ( B e. N. -> B e. _om )
17 pinn 
 |-  ( C e. N. -> C e. _om )
18 nnacan 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
19 18 biimpd 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A +o B ) = ( A +o C ) -> B = C ) )
20 15 16 17 19 syl3an 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A +o B ) = ( A +o C ) -> B = C ) )
21 20 3expa 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A +o B ) = ( A +o C ) -> B = C ) )
22 14 21 sylbid 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A +N B ) = ( A +N C ) -> B = C ) )
23 9 22 sylan2 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( ( A +N B ) = ( A +N C ) /\ ( A e. N. /\ B e. N. ) ) ) -> ( ( A +N B ) = ( A +N C ) -> B = C ) )
24 23 exp32 
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = ( A +N C ) -> ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = ( A +N C ) -> B = C ) ) ) )
25 24 imp4b 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( A +N B ) = ( A +N C ) ) -> ( ( ( A e. N. /\ B e. N. ) /\ ( A +N B ) = ( A +N C ) ) -> B = C ) )
26 25 pm2.43i 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( A +N B ) = ( A +N C ) ) -> B = C )
27 26 ex 
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = ( A +N C ) -> B = C ) )
28 oveq2 
 |-  ( B = C -> ( A +N B ) = ( A +N C ) )
29 27 28 impbid1 
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = ( A +N C ) <-> B = C ) )