Metamath Proof Explorer

Theorem nmulel1

Description: Natural multiplication by a non-zero number preserves less-than. (Contributed by Scott Fenton, 15-Jul-2026)

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

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> C e. On )
2 simpll 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> B e. On )
3 df-ne 
 |-  ( C =/= (/) <-> -. C = (/) )
4 on0eqel 
 |-  ( C e. On -> ( C = (/) \/ (/) e. C ) )
5 4 orcanai 
 |-  ( ( C e. On /\ -. C = (/) ) -> (/) e. C )
6 3 5 sylan2b 
 |-  ( ( C e. On /\ C =/= (/) ) -> (/) e. C )
7 6 ad2ant2l 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> (/) e. C )
8 simprl 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> A e. B )
9 nmuladdel 
 |-  ( ( ( C e. On /\ B e. On ) /\ ( (/) e. C /\ A e. B ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) e. ( ( C .no B ) +no ( (/) .no A ) ) )
10 1 2 7 8 9 syl22anc 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) e. ( ( C .no B ) +no ( (/) .no A ) ) )
11 nmull0 
 |-  ( B e. On -> ( (/) .no B ) = (/) )
12 2 11 syl 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) .no B ) = (/) )
13 12 oveq1d 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( (/) +no ( C .no A ) ) )
14 onelon 
 |-  ( ( B e. On /\ A e. B ) -> A e. On )
15 14 ad2ant2r 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> A e. On )
16 1 15 nmulcld 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. On )
17 naddlid 
 |-  ( ( C .no A ) e. On -> ( (/) +no ( C .no A ) ) = ( C .no A ) )
18 16 17 syl 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) +no ( C .no A ) ) = ( C .no A ) )
19 13 18 eqtrd 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( C .no A ) )
20 nmull0 
 |-  ( A e. On -> ( (/) .no A ) = (/) )
21 15 20 syl 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) .no A ) = (/) )
22 21 oveq2d 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( ( C .no B ) +no (/) ) )
23 1 2 nmulcld 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no B ) e. On )
24 naddrid 
 |-  ( ( C .no B ) e. On -> ( ( C .no B ) +no (/) ) = ( C .no B ) )
25 23 24 syl 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no (/) ) = ( C .no B ) )
26 22 25 eqtrd 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( C .no B ) )
27 10 19 26 3eltr3d 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. ( C .no B ) )