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 ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = A + 𝑵 C ↔ B = C

Proof

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