Metamath Proof Explorer

Theorem ltnmul

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

Ref Expression
Assertion ltnmul 
|- ( ( 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 ) ) ) )

Proof

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