Metamath Proof Explorer

Theorem nmulss1

Description: Natural multiplication preserves less-than or equal. (Contributed by Scott Fenton, 15-Jul-2026)

Ref Expression
Assertion nmulss1 
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) C_ ( C .no B ) )

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> C e. On )
2 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> B e. On )
3 0elon 
 |-  (/) e. On
4 3 a1i 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> (/) e. On )
5 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> A e. On )
6 0ss 
 |-  (/) C_ C
7 6 a1i 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> (/) C_ C )
8 simpr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> A C_ B )
9 nmuladdss 
 |-  ( ( ( C e. On /\ B e. On ) /\ ( (/) e. On /\ A e. On ) /\ ( (/) C_ C /\ A C_ B ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) C_ ( ( C .no B ) +no ( (/) .no A ) ) )
10 1 2 4 5 7 8 9 syl222anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( (/) .no B ) +no ( C .no A ) ) C_ ( ( C .no B ) +no ( (/) .no A ) ) )
11 nmull0 
 |-  ( B e. On -> ( (/) .no B ) = (/) )
12 2 11 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) .no B ) = (/) )
13 12 oveq1d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( (/) +no ( C .no A ) ) )
14 1 5 nmulcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) e. On )
15 naddlid 
 |-  ( ( C .no A ) e. On -> ( (/) +no ( C .no A ) ) = ( C .no A ) )
16 14 15 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) +no ( C .no A ) ) = ( C .no A ) )
17 13 16 eqtr2d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) = ( ( (/) .no B ) +no ( C .no A ) ) )
18 nmull0 
 |-  ( A e. On -> ( (/) .no A ) = (/) )
19 5 18 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) .no A ) = (/) )
20 19 oveq2d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( ( C .no B ) +no (/) ) )
21 1 2 nmulcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no B ) e. On )
22 naddrid 
 |-  ( ( C .no B ) e. On -> ( ( C .no B ) +no (/) ) = ( C .no B ) )
23 21 22 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( C .no B ) +no (/) ) = ( C .no B ) )
24 20 23 eqtr2d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no B ) = ( ( C .no B ) +no ( (/) .no A ) ) )
25 10 17 24 3sstr4d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) C_ ( C .no B ) )