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