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