Theorem nmulel1

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

	Ref	Expression
Assertion	nmulel1	Could not format assertion : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. ( C .no B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simplr	$$⊢\left(\left(B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(A\in B\wedge C\ne \varnothing \right)\right)\to C\in \mathrm{On}$$
2		simpll	$$⊢\left(\left(B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(A\in B\wedge C\ne \varnothing \right)\right)\to B\in \mathrm{On}$$
3		df-ne	$$⊢C\ne \varnothing \leftrightarrow \neg C=\varnothing$$
4		on0eqel	$$⊢C\in \mathrm{On}\to \left(C=\varnothing \vee \varnothing \in C\right)$$
5	4	orcanai	$$⊢\left(C\in \mathrm{On}\wedge \neg C=\varnothing \right)\to \varnothing \in C$$
6	3 5	sylan2b	$$⊢\left(C\in \mathrm{On}\wedge C\ne \varnothing \right)\to \varnothing \in C$$
7	6	ad2ant2l	$$⊢\left(\left(B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(A\in B\wedge C\ne \varnothing \right)\right)\to \varnothing \in C$$
8		simprl	$$⊢\left(\left(B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(A\in B\wedge C\ne \varnothing \right)\right)\to A\in B$$
9		nmuladdel	Could not format ( ( ( C e. On /\ B e. On ) /\ ( (/) e. C /\ A e. B ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) e. ( ( C .no B ) +no ( (/) .no A ) ) ) : No typesetting found for |- ( ( ( C e. On /\ B e. On ) /\ ( (/) e. C /\ A e. B ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) e. ( ( C .no B ) +no ( (/) .no A ) ) ) with typecode |-
10	1 2 7 8 9	syl22anc	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) e. ( ( C .no B ) +no ( (/) .no A ) ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) e. ( ( C .no B ) +no ( (/) .no A ) ) ) with typecode |-
11		nmull0	Could not format ( B e. On -> ( (/) .no B ) = (/) ) : No typesetting found for |- ( B e. On -> ( (/) .no B ) = (/) ) with typecode |-
12	2 11	syl	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) .no B ) = (/) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) .no B ) = (/) ) with typecode |-
13	12	oveq1d	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( (/) +no ( C .no A ) ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( (/) +no ( C .no A ) ) ) with typecode |-
14		onelon	$$⊢\left(B\in \mathrm{On}\wedge A\in B\right)\to A\in \mathrm{On}$$
15	14	ad2ant2r	$$⊢\left(\left(B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(A\in B\wedge C\ne \varnothing \right)\right)\to A\in \mathrm{On}$$
16	1 15	nmulcld	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. On ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. On ) with typecode |-
17		naddlid	Could not format ( ( C .no A ) e. On -> ( (/) +no ( C .no A ) ) = ( C .no A ) ) : No typesetting found for |- ( ( C .no A ) e. On -> ( (/) +no ( C .no A ) ) = ( C .no A ) ) with typecode |-
18	16 17	syl	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) +no ( C .no A ) ) = ( C .no A ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) +no ( C .no A ) ) = ( C .no A ) ) with typecode |-
19	13 18	eqtrd	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( C .no A ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( C .no A ) ) with typecode |-
20		nmull0	Could not format ( A e. On -> ( (/) .no A ) = (/) ) : No typesetting found for |- ( A e. On -> ( (/) .no A ) = (/) ) with typecode |-
21	15 20	syl	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) .no A ) = (/) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( (/) .no A ) = (/) ) with typecode |-
22	21	oveq2d	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( ( C .no B ) +no (/) ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( ( C .no B ) +no (/) ) ) with typecode |-
23	1 2	nmulcld	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no B ) e. On ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no B ) e. On ) with typecode |-
24		naddrid	Could not format ( ( C .no B ) e. On -> ( ( C .no B ) +no (/) ) = ( C .no B ) ) : No typesetting found for |- ( ( C .no B ) e. On -> ( ( C .no B ) +no (/) ) = ( C .no B ) ) with typecode |-
25	23 24	syl	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no (/) ) = ( C .no B ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no (/) ) = ( C .no B ) ) with typecode |-
26	22 25	eqtrd	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( C .no B ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( C .no B ) ) with typecode |-
27	10 19 26	3eltr3d	Could not format ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. ( C .no B ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( A e. B /\ C =/= (/) ) ) -> ( C .no A ) e. ( C .no B ) ) with typecode |-