Metamath Proof Explorer

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 
|- ( ( 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmulcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On )
2 ontri1 
 |-  ( ( ( A .no B ) e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> -. C e. ( A .no B ) ) )
3 1 2 stoic3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .no B ) C_ C <-> -. C e. ( A .no B ) ) )
4 ltnmul 
 |-  ( ( 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 ) ) ) )
5 4 3coml 
 |-  ( ( 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 ) ) ) )
6 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> C e. On )
7 simp1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> A e. On )
8 simpl 
 |-  ( ( a e. A /\ b e. B ) -> a e. A )
9 onelon 
 |-  ( ( A e. On /\ a e. A ) -> a e. On )
10 7 8 9 syl2an 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> a e. On )
11 simp2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> B e. On )
12 simpr 
 |-  ( ( a e. A /\ b e. B ) -> b e. B )
13 onelon 
 |-  ( ( B e. On /\ b e. B ) -> b e. On )
14 11 12 13 syl2an 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> b e. On )
15 10 14 nmulcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a .no b ) e. On )
16 6 15 naddcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( C +no ( a .no b ) ) e. On )
17 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> B e. On )
18 10 17 nmulcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a .no B ) e. On )
19 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> A e. On )
20 19 14 nmulcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( A .no b ) e. On )
21 18 20 naddcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( a .no B ) +no ( A .no b ) ) e. On )
22 ontri1 
 |-  ( ( ( 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 ) ) ) )
23 16 21 22 syl2anc 
 |-  ( ( ( 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 ) ) ) )
24 23 2rexbidva 
 |-  ( ( 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 ) ) ) )
25 rexnal2 
 |-  ( 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 ) ) )
26 24 25 bitrdi 
 |-  ( ( 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 ) ) ) )
27 5 26 bitr2d 
 |-  ( ( 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 ) ) )
28 27 con1bid 
 |-  ( ( 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 ) ) ) )
29 3 28 bitrd 
 |-  ( ( 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 ) ) ) )