Metamath Proof Explorer

Theorem mulscan2dlem

Description: Lemma for mulscan2d . Cancellation of multiplication when the right term is positive. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses mulscan2d.1 ⊢ φ → A ∈ No
mulscan2d.2 ⊢ φ → B ∈ No
mulscan2d.3 ⊢ φ → C ∈ No
mulscan2dlem.1 ⊢ φ → 0 s < s C
Assertion mulscan2dlem ⊢ φ → A ⋅ s C = B ⋅ s C ↔ A = B

Proof

Step Hyp Ref Expression
1 mulscan2d.1 ⊢ φ → A ∈ No
2 mulscan2d.2 ⊢ φ → B ∈ No
3 mulscan2d.3 ⊢ φ → C ∈ No
4 mulscan2dlem.1 ⊢ φ → 0 s < s C
5 1 2 3 4 slemul1d ⊢ φ → A ≤ s B ↔ A ⋅ s C ≤ s B ⋅ s C
6 2 1 3 4 slemul1d ⊢ φ → B ≤ s A ↔ B ⋅ s C ≤ s A ⋅ s C
7 5 6 anbi12d ⊢ φ → A ≤ s B ∧ B ≤ s A ↔ A ⋅ s C ≤ s B ⋅ s C ∧ B ⋅ s C ≤ s A ⋅ s C
8 sletri3 ⊢ A ∈ No ∧ B ∈ No → A = B ↔ A ≤ s B ∧ B ≤ s A
9 1 2 8 syl2anc ⊢ φ → A = B ↔ A ≤ s B ∧ B ≤ s A
10 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
11 2 3 mulscld ⊢ φ → B ⋅ s C ∈ No
12 sletri3 ⊢ A ⋅ s C ∈ No ∧ B ⋅ s C ∈ No → A ⋅ s C = B ⋅ s C ↔ A ⋅ s C ≤ s B ⋅ s C ∧ B ⋅ s C ≤ s A ⋅ s C
13 10 11 12 syl2anc ⊢ φ → A ⋅ s C = B ⋅ s C ↔ A ⋅ s C ≤ s B ⋅ s C ∧ B ⋅ s C ≤ s A ⋅ s C
14 7 9 13 3bitr4rd ⊢ φ → A ⋅ s C = B ⋅ s C ↔ A = B