Theorem ltnmul

Description: Characterize less-than a natural product. (Contributed by Scott Fenton, 15-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = A -> ( x +no ( b .no c ) ) = ( A +no ( b .no c ) ) ) : No typesetting found for |- ( x = A -> ( x +no ( b .no c ) ) = ( A +no ( b .no c ) ) ) with typecode |-
2	1	eleq2d	Could not format ( x = A -> ( ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) <-> ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( x = A -> ( ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) <-> ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
3	2	2ralbidv	Could not format ( x = A -> ( A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) <-> A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( x = A -> ( A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) <-> A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
4	3	onnminsb	Could not format ( A e. On -> ( A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } -> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( A e. On -> ( A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } -> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
5	4	3ad2ant1	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } -> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } -> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
6		nmulval	Could not format ( ( B e. On /\ C e. On ) -> ( B .no C ) = |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } ) : No typesetting found for |- ( ( B e. On /\ C e. On ) -> ( B .no C ) = |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } ) with typecode |-
7	6	eleq2d	Could not format ( ( B e. On /\ C e. On ) -> ( A e. ( B .no C ) <-> A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } ) ) : No typesetting found for |- ( ( B e. On /\ C e. On ) -> ( A e. ( B .no C ) <-> A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } ) ) with typecode |-
8	7	3adant1	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B .no C ) <-> A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B .no C ) <-> A e. |^| { x e. On | A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( x +no ( b .no c ) ) } ) ) with typecode |-
9		simpl1	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(b\in B\wedge c\in C\right)\right)\to A\in \mathrm{On}$$
10		simp2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to B\in \mathrm{On}$$
11		simpl	$$⊢\left(b\in B\wedge c\in C\right)\to b\in B$$
12		onelon	$$⊢\left(B\in \mathrm{On}\wedge b\in B\right)\to b\in \mathrm{On}$$
13	10 11 12	syl2an	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(b\in B\wedge c\in C\right)\right)\to b\in \mathrm{On}$$
14		simp3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to C\in \mathrm{On}$$
15		simpr	$$⊢\left(b\in B\wedge c\in C\right)\to c\in C$$
16		onelon	$$⊢\left(C\in \mathrm{On}\wedge c\in C\right)\to c\in \mathrm{On}$$
17	14 15 16	syl2an	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(b\in B\wedge c\in C\right)\right)\to c\in \mathrm{On}$$
18	13 17	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( b .no c ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( b .no c ) e. On ) with typecode |-
19	9 18	naddcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( A +no ( b .no c ) ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( A +no ( b .no c ) ) e. On ) with typecode |-
20		simpl3	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(b\in B\wedge c\in C\right)\right)\to C\in \mathrm{On}$$
21	13 20	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( b .no C ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( b .no C ) e. On ) with typecode |-
22		simpl2	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(b\in B\wedge c\in C\right)\right)\to B\in \mathrm{On}$$
23	22 17	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( B .no c ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( B .no c ) e. On ) with typecode |-
24	21 23	naddcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( b .no C ) +no ( B .no c ) ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( b .no C ) +no ( B .no c ) ) e. On ) with typecode |-
25		ontri1	Could not format ( ( ( A +no ( b .no c ) ) e. On /\ ( ( b .no C ) +no ( B .no c ) ) e. On ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( ( A +no ( b .no c ) ) e. On /\ ( ( b .no C ) +no ( B .no c ) ) e. On ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
26	19 24 25	syl2anc	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
27	26	2rexbidva	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> E. b e. B E. c e. C -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> E. b e. B E. c e. C -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
28		rexnal2	Could not format ( E. b e. B E. c e. C -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) <-> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) : No typesetting found for |- ( E. b e. B E. c e. C -. ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) <-> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) with typecode |-
29	27 28	bitrdi	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) <-> -. A. b e. B A. c e. C ( ( b .no C ) +no ( B .no c ) ) e. ( A +no ( b .no c ) ) ) ) with typecode |-
30	5 8 29	3imtr4d	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B .no C ) -> E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B .no C ) -> E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) ) ) with typecode |-
31		nmuladdel	Could not format ( ( ( B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) : No typesetting found for |- ( ( ( B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) with typecode |-
32	31	3adantl1	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) with typecode |-
33	22 20	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( B .no C ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( B .no C ) e. On ) with typecode |-
34	33 18	naddcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( B .no C ) +no ( b .no c ) ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( B .no C ) +no ( b .no c ) ) e. On ) with typecode |-
35		ontr2	Could not format ( ( ( A +no ( b .no c ) ) e. On /\ ( ( B .no C ) +no ( b .no c ) ) e. On ) -> ( ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) /\ ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) -> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( ( A +no ( b .no c ) ) e. On /\ ( ( B .no C ) +no ( b .no c ) ) e. On ) -> ( ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) /\ ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) -> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) with typecode |-
36	19 34 35	syl2anc	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) /\ ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) -> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) /\ ( ( b .no C ) +no ( B .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) -> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) with typecode |-
37	32 36	mpan2d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) -> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) -> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) with typecode |-
38		naddel1	Could not format ( ( A e. On /\ ( B .no C ) e. On /\ ( b .no c ) e. On ) -> ( A e. ( B .no C ) <-> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( A e. On /\ ( B .no C ) e. On /\ ( b .no c ) e. On ) -> ( A e. ( B .no C ) <-> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) with typecode |-
39	9 33 18 38	syl3anc	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( A e. ( B .no C ) <-> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( A e. ( B .no C ) <-> ( A +no ( b .no c ) ) e. ( ( B .no C ) +no ( b .no c ) ) ) ) with typecode |-
40	37 39	sylibrd	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) -> A e. ( B .no C ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ c e. C ) ) -> ( ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) -> A e. ( B .no C ) ) ) with typecode |-
41	40	rexlimdvva	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) -> A e. ( B .no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) -> A e. ( B .no C ) ) ) with typecode |-
42	30 41	impbid	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B .no C ) <-> E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B .no C ) <-> E. b e. B E. c e. C ( A +no ( b .no c ) ) C_ ( ( b .no C ) +no ( B .no c ) ) ) ) with typecode |-