Metamath Proof Explorer

Theorem nnacan

Description: Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnacan ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A + 𝑜 B = A + 𝑜 C ↔ B = C

Proof

Step Hyp Ref Expression
1 nnaword ⊢ B ∈ ω ∧ C ∈ ω ∧ A ∈ ω → B ⊆ C ↔ A + 𝑜 B ⊆ A + 𝑜 C
2 1 3comr ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → B ⊆ C ↔ A + 𝑜 B ⊆ A + 𝑜 C
3 nnaword ⊢ C ∈ ω ∧ B ∈ ω ∧ A ∈ ω → C ⊆ B ↔ A + 𝑜 C ⊆ A + 𝑜 B
4 3 3com13 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C ⊆ B ↔ A + 𝑜 C ⊆ A + 𝑜 B
5 2 4 anbi12d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → B ⊆ C ∧ C ⊆ B ↔ A + 𝑜 B ⊆ A + 𝑜 C ∧ A + 𝑜 C ⊆ A + 𝑜 B
6 5 bicomd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A + 𝑜 B ⊆ A + 𝑜 C ∧ A + 𝑜 C ⊆ A + 𝑜 B ↔ B ⊆ C ∧ C ⊆ B
7 eqss ⊢ A + 𝑜 B = A + 𝑜 C ↔ A + 𝑜 B ⊆ A + 𝑜 C ∧ A + 𝑜 C ⊆ A + 𝑜 B
8 eqss ⊢ B = C ↔ B ⊆ C ∧ C ⊆ B
9 6 7 8 3bitr4g ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A + 𝑜 B = A + 𝑜 C ↔ B = C