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	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulscan2d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	mulscan2d.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	mulscan2dlem.1	⊢ ( 𝜑 → 0s <s 𝐶 )
Assertion	mulscan2dlem	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mulscan2d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulscan2d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		mulscan2d.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		mulscan2dlem.1	⊢ ( 𝜑 → 0s <s 𝐶 )
5	1 2 3 4	slemul1d	⊢ ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ) )
6	2 1 3 4	slemul1d	⊢ ( 𝜑 → ( 𝐵 ≤s 𝐴 ↔ ( 𝐵 ·s 𝐶 ) ≤s ( 𝐴 ·s 𝐶 ) ) )
7	5 6	anbi12d	⊢ ( 𝜑 → ( ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ↔ ( ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ∧ ( 𝐵 ·s 𝐶 ) ≤s ( 𝐴 ·s 𝐶 ) ) ) )
8		sletri3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ) )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ) )
10	1 3	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
11	2 3	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
12		sletri3	⊢ ( ( ( 𝐴 ·s 𝐶 ) ∈ No ∧ ( 𝐵 ·s 𝐶 ) ∈ No ) → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ ( ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ∧ ( 𝐵 ·s 𝐶 ) ≤s ( 𝐴 ·s 𝐶 ) ) ) )
13	10 11 12	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ ( ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ∧ ( 𝐵 ·s 𝐶 ) ≤s ( 𝐴 ·s 𝐶 ) ) ) )
14	7 9 13	3bitr4rd	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )