Theorem nmulle

Description: A condition for bounding a natural product above. Converse of ltnmul . (Contributed by Scott Fenton, 16-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		nmulcl	Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On ) with typecode |-
2		ontri1	Could not format ( ( ( A .no B ) e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> -. C e. ( A .no B ) ) ) : No typesetting found for |- ( ( ( A .no B ) e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> -. C e. ( A .no B ) ) ) with typecode |-
3	1 2	stoic3	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> -. C e. ( A .no B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> -. C e. ( A .no B ) ) ) with typecode |-
4		ltnmul	Could not format ( ( C e. On /\ A e. On /\ B e. On ) -> ( C e. ( A .no B ) <-> E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) ) ) : No typesetting found for |- ( ( C e. On /\ A e. On /\ B e. On ) -> ( C e. ( A .no B ) <-> E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) ) ) with typecode |-
5	4	3coml	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( C e. ( A .no B ) <-> E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( C e. ( A .no B ) <-> E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) ) ) with typecode |-
6		simpl3	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(a\in A\wedge b\in B\right)\right)\to C\in \mathrm{On}$$
7		simp1	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to A\in \mathrm{On}$$
8		simpl	$$⊢\left(a\in A\wedge b\in B\right)\to a\in A$$
9		onelon	$$⊢\left(A\in \mathrm{On}\wedge a\in A\right)\to a\in \mathrm{On}$$
10	7 8 9	syl2an	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(a\in A\wedge b\in B\right)\right)\to a\in \mathrm{On}$$
11		simp2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to B\in \mathrm{On}$$
12		simpr	$$⊢\left(a\in A\wedge b\in B\right)\to b\in B$$
13		onelon	$$⊢\left(B\in \mathrm{On}\wedge b\in B\right)\to b\in \mathrm{On}$$
14	11 12 13	syl2an	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(a\in A\wedge b\in B\right)\right)\to b\in \mathrm{On}$$
15	10 14	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a .no b ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a .no b ) e. On ) with typecode |-
16	6 15	naddcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( C +no ( a .no b ) ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( C +no ( a .no b ) ) e. On ) with typecode |-
17		simpl2	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(a\in A\wedge b\in B\right)\right)\to B\in \mathrm{On}$$
18	10 17	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a .no B ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a .no B ) e. On ) with typecode |-
19		simpl1	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(a\in A\wedge b\in B\right)\right)\to A\in \mathrm{On}$$
20	19 14	nmulcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( A .no b ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( A .no b ) e. On ) with typecode |-
21	18 20	naddcld	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( a .no B ) +no ( A .no b ) ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( a .no B ) +no ( A .no b ) ) e. On ) with typecode |-
22		ontri1	Could not format ( ( ( C +no ( a .no b ) ) e. On /\ ( ( a .no B ) +no ( A .no b ) ) e. On ) -> ( ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( ( C +no ( a .no b ) ) e. On /\ ( ( a .no B ) +no ( A .no b ) ) e. On ) -> ( ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) with typecode |-
23	16 21 22	syl2anc	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) with typecode |-
24	23	2rexbidva	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> E. a e. A E. b e. B -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> E. a e. A E. b e. B -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) with typecode |-
25		rexnal2	Could not format ( E. a e. A E. b e. B -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) <-> -. A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) : No typesetting found for |- ( E. a e. A E. b e. B -. ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) <-> -. A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) with typecode |-
26	24 25	bitrdi	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> -. A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. a e. A E. b e. B ( C +no ( a .no b ) ) C_ ( ( a .no B ) +no ( A .no b ) ) <-> -. A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) with typecode |-
27	5 26	bitr2d	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) <-> C e. ( A .no B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) <-> C e. ( A .no B ) ) ) with typecode |-
28	27	con1bid	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. C e. ( A .no B ) <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. C e. ( A .no B ) <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) with typecode |-
29	3 28	bitrd	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( C +no ( a .no b ) ) ) ) with typecode |-