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 ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 addclpi ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐵 ) ∈ N )
2 eleq1 ⊢ ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → ( ( 𝐴 +N 𝐵 ) ∈ N ↔ ( 𝐴 +N 𝐶 ) ∈ N ) )
3 1 2 imbitrid ⊢ ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐶 ) ∈ N ) )
4 3 imp ⊢ ( ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ∧ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ) → ( 𝐴 +N 𝐶 ) ∈ N )
5 dmaddpi ⊢ dom +N = ( N × N )
6 0npi ⊢ ¬ ∅ ∈ N
7 5 6 ndmovrcl ⊢ ( ( 𝐴 +N 𝐶 ) ∈ N → ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) )
8 simpr ⊢ ( ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) → 𝐶 ∈ N )
9 4 7 8 3syl ⊢ ( ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ∧ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ) → 𝐶 ∈ N )
10 addpiord ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐵 ) = ( 𝐴 +o 𝐵 ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 +N 𝐵 ) = ( 𝐴 +o 𝐵 ) )
12 addpiord ⊢ ( ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 +N 𝐶 ) = ( 𝐴 +o 𝐶 ) )
13 12 adantlr ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 +N 𝐶 ) = ( 𝐴 +o 𝐶 ) )
14 11 13 eqeq12d ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ↔ ( 𝐴 +o 𝐵 ) = ( 𝐴 +o 𝐶 ) ) )
15 pinn ⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
16 pinn ⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
17 pinn ⊢ ( 𝐶 ∈ N → 𝐶 ∈ ω )
18 nnacan ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 +o 𝐵 ) = ( 𝐴 +o 𝐶 ) ↔ 𝐵 = 𝐶 ) )
19 18 biimpd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 +o 𝐵 ) = ( 𝐴 +o 𝐶 ) → 𝐵 = 𝐶 ) )
20 15 16 17 19 syl3an ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 +o 𝐵 ) = ( 𝐴 +o 𝐶 ) → 𝐵 = 𝐶 ) )
21 20 3expa ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 +o 𝐵 ) = ( 𝐴 +o 𝐶 ) → 𝐵 = 𝐶 ) )
22 14 21 sylbid ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → 𝐵 = 𝐶 ) )
23 9 22 sylan2 ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ∧ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ) ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → 𝐵 = 𝐶 ) )
24 23 exp32 ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → 𝐵 = 𝐶 ) ) ) )
25 24 imp4b ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ) → ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ) → 𝐵 = 𝐶 ) )
26 25 pm2.43i ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ) → 𝐵 = 𝐶 )
27 26 ex ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) → 𝐵 = 𝐶 ) )
28 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) )
29 27 28 impbid1 ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) = ( 𝐴 +N 𝐶 ) ↔ 𝐵 = 𝐶 ) )