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 ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( 𝐶 ·no 𝐴 ) ∈ ( 𝐶 ·no 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → 𝐶 ∈ On )
2 simpll ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → 𝐵 ∈ On )
3 df-ne ⊢ ( 𝐶 ≠ ∅ ↔ ¬ 𝐶 = ∅ )
4 on0eqel ⊢ ( 𝐶 ∈ On → ( 𝐶 = ∅ ∨ ∅ ∈ 𝐶 ) )
5 4 orcanai ⊢ ( ( 𝐶 ∈ On ∧ ¬ 𝐶 = ∅ ) → ∅ ∈ 𝐶 )
6 3 5 sylan2b ⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ≠ ∅ ) → ∅ ∈ 𝐶 )
7 6 ad2ant2l ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ∅ ∈ 𝐶 )
8 simprl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → 𝐴 ∈ 𝐵 )
9 nmuladdel ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) ∈ ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) )
10 1 2 7 8 9 syl22anc ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) ∈ ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) )
11 nmull0 ⊢ ( 𝐵 ∈ On → ( ∅ ·no 𝐵 ) = ∅ )
12 2 11 syl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ∅ ·no 𝐵 ) = ∅ )
13 12 oveq1d ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) = ( ∅ +no ( 𝐶 ·no 𝐴 ) ) )
14 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
15 14 ad2ant2r ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → 𝐴 ∈ On )
16 1 15 nmulcld ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( 𝐶 ·no 𝐴 ) ∈ On )
17 naddlid ⊢ ( ( 𝐶 ·no 𝐴 ) ∈ On → ( ∅ +no ( 𝐶 ·no 𝐴 ) ) = ( 𝐶 ·no 𝐴 ) )
18 16 17 syl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ∅ +no ( 𝐶 ·no 𝐴 ) ) = ( 𝐶 ·no 𝐴 ) )
19 13 18 eqtrd ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) = ( 𝐶 ·no 𝐴 ) )
20 nmull0 ⊢ ( 𝐴 ∈ On → ( ∅ ·no 𝐴 ) = ∅ )
21 15 20 syl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ∅ ·no 𝐴 ) = ∅ )
22 21 oveq2d ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ∅ ) )
23 1 2 nmulcld ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( 𝐶 ·no 𝐵 ) ∈ On )
24 naddrid ⊢ ( ( 𝐶 ·no 𝐵 ) ∈ On → ( ( 𝐶 ·no 𝐵 ) +no ∅ ) = ( 𝐶 ·no 𝐵 ) )
25 23 24 syl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ( 𝐶 ·no 𝐵 ) +no ∅ ) = ( 𝐶 ·no 𝐵 ) )
26 22 25 eqtrd ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) = ( 𝐶 ·no 𝐵 ) )
27 10 19 26 3eltr3d ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅ ) ) → ( 𝐶 ·no 𝐴 ) ∈ ( 𝐶 ·no 𝐵 ) )