Metamath Proof Explorer

Theorem nnmcan

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

Ref Expression
Assertion nnmcan ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → A ⋅ 𝑜 B = A ⋅ 𝑜 C ↔ B = C

Proof

Step Hyp Ref Expression
1 3anrot ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ↔ B ∈ ω ∧ C ∈ ω ∧ A ∈ ω
2 nnmword ⊢ B ∈ ω ∧ C ∈ ω ∧ A ∈ ω ∧ ∅ ∈ A → B ⊆ C ↔ A ⋅ 𝑜 B ⊆ A ⋅ 𝑜 C
3 1 2 sylanb ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → B ⊆ C ↔ A ⋅ 𝑜 B ⊆ A ⋅ 𝑜 C
4 3anrev ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ↔ C ∈ ω ∧ B ∈ ω ∧ A ∈ ω
5 nnmword ⊢ C ∈ ω ∧ B ∈ ω ∧ A ∈ ω ∧ ∅ ∈ A → C ⊆ B ↔ A ⋅ 𝑜 C ⊆ A ⋅ 𝑜 B
6 4 5 sylanb ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → C ⊆ B ↔ A ⋅ 𝑜 C ⊆ A ⋅ 𝑜 B
7 3 6 anbi12d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → B ⊆ C ∧ C ⊆ B ↔ A ⋅ 𝑜 B ⊆ A ⋅ 𝑜 C ∧ A ⋅ 𝑜 C ⊆ A ⋅ 𝑜 B
8 7 bicomd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → A ⋅ 𝑜 B ⊆ A ⋅ 𝑜 C ∧ A ⋅ 𝑜 C ⊆ A ⋅ 𝑜 B ↔ B ⊆ C ∧ C ⊆ B
9 eqss ⊢ A ⋅ 𝑜 B = A ⋅ 𝑜 C ↔ A ⋅ 𝑜 B ⊆ A ⋅ 𝑜 C ∧ A ⋅ 𝑜 C ⊆ A ⋅ 𝑜 B
10 eqss ⊢ B = C ↔ B ⊆ C ∧ C ⊆ B
11 8 9 10 3bitr4g ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → A ⋅ 𝑜 B = A ⋅ 𝑜 C ↔ B = C