Theorem nmulss1

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl3	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge A\subseteq B\right)\to C\in \mathrm{On}$$
2		simpl2	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge A\subseteq B\right)\to B\in \mathrm{On}$$
3		0elon	$$⊢\varnothing \in \mathrm{On}$$
4	3	a1i	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge A\subseteq B\right)\to \varnothing \in \mathrm{On}$$
5		simpl1	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge A\subseteq B\right)\to A\in \mathrm{On}$$
6		0ss	$$⊢\varnothing \subseteq C$$
7	6	a1i	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge A\subseteq B\right)\to \varnothing \subseteq C$$
8		simpr	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge A\subseteq B\right)\to A\subseteq B$$
9		nmuladdss	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
10	1 2 4 5 7 8 9	syl222anc	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) 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 ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) .no B ) = (/) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) .no B ) = (/) ) with typecode |-
13	12	oveq1d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( (/) +no ( C .no A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( (/) .no B ) +no ( C .no A ) ) = ( (/) +no ( C .no A ) ) ) with typecode |-
14	1 5	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) e. On ) with typecode |-
15		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 |-
16	14 15	syl	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) +no ( C .no A ) ) = ( C .no A ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) +no ( C .no A ) ) = ( C .no A ) ) with typecode |-
17	13 16	eqtr2d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) = ( ( (/) .no B ) +no ( C .no A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) = ( ( (/) .no B ) +no ( C .no A ) ) ) with typecode |-
18		nmull0	Could not format ( A e. On -> ( (/) .no A ) = (/) ) : No typesetting found for |- ( A e. On -> ( (/) .no A ) = (/) ) with typecode |-
19	5 18	syl	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) .no A ) = (/) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( (/) .no A ) = (/) ) with typecode |-
20	19	oveq2d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( ( C .no B ) +no (/) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( C .no B ) +no ( (/) .no A ) ) = ( ( C .no B ) +no (/) ) ) with typecode |-
21	1 2	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no B ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no B ) e. On ) with typecode |-
22		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 |-
23	21 22	syl	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( C .no B ) +no (/) ) = ( C .no B ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( C .no B ) +no (/) ) = ( C .no B ) ) with typecode |-
24	20 23	eqtr2d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no B ) = ( ( C .no B ) +no ( (/) .no A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no B ) = ( ( C .no B ) +no ( (/) .no A ) ) ) with typecode |-
25	10 17 24	3sstr4d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) C_ ( C .no B ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( C .no A ) C_ ( C .no B ) ) with typecode |-