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 
|- ( ph -> A e. No )
mulscan2d.2 
|- ( ph -> B e. No )
mulscan2d.3 
|- ( ph -> C e. No )
mulscan2dlem.1 
|- ( ph -> 0s
Assertion mulscan2dlem 
|- ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 mulscan2d.1 
 |-  ( ph -> A e. No )
2 mulscan2d.2 
 |-  ( ph -> B e. No )
3 mulscan2d.3 
 |-  ( ph -> C e. No )
4 mulscan2dlem.1 
 |-  ( ph -> 0s
5 1 2 3 4 slemul1d 
 |-  ( ph -> ( A <_s B <-> ( A x.s C ) <_s ( B x.s C ) ) )
6 2 1 3 4 slemul1d 
 |-  ( ph -> ( B <_s A <-> ( B x.s C ) <_s ( A x.s C ) ) )
7 5 6 anbi12d 
 |-  ( ph -> ( ( A <_s B /\ B <_s A ) <-> ( ( A x.s C ) <_s ( B x.s C ) /\ ( B x.s C ) <_s ( A x.s C ) ) ) )
8 sletri3 
 |-  ( ( A e. No /\ B e. No ) -> ( A = B <-> ( A <_s B /\ B <_s A ) ) )
9 1 2 8 syl2anc 
 |-  ( ph -> ( A = B <-> ( A <_s B /\ B <_s A ) ) )
10 1 3 mulscld 
 |-  ( ph -> ( A x.s C ) e. No )
11 2 3 mulscld 
 |-  ( ph -> ( B x.s C ) e. No )
12 sletri3 
 |-  ( ( ( A x.s C ) e. No /\ ( B x.s C ) e. No ) -> ( ( A x.s C ) = ( B x.s C ) <-> ( ( A x.s C ) <_s ( B x.s C ) /\ ( B x.s C ) <_s ( A x.s C ) ) ) )
13 10 11 12 syl2anc 
 |-  ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> ( ( A x.s C ) <_s ( B x.s C ) /\ ( B x.s C ) <_s ( A x.s C ) ) ) )
14 7 9 13 3bitr4rd 
 |-  ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )