Metamath Proof Explorer

Theorem oaltom

Description: Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025)

Ref Expression
Assertion oaltom 
|- ( ( A e. On /\ B e. On ) -> ( ( 1o e. A /\ A e. B ) -> ( B +o A ) e. ( B .o A ) ) )

Proof

Step Hyp Ref Expression
1 om2 
 |-  ( B e. On -> ( B +o B ) = ( B .o 2o ) )
2 1 ad2antlr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B +o B ) = ( B .o 2o ) )
3 2on 
 |-  2o e. On
4 3 a1i 
 |-  ( ( A e. On /\ B e. On ) -> 2o e. On )
5 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
6 simpr 
 |-  ( ( A e. On /\ B e. On ) -> B e. On )
7 4 5 6 3jca 
 |-  ( ( A e. On /\ B e. On ) -> ( 2o e. On /\ A e. On /\ B e. On ) )
8 7 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( 2o e. On /\ A e. On /\ B e. On ) )
9 df-2o 
 |-  2o = suc 1o
10 9 a1i 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> 2o = suc 1o )
11 simprl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> 1o e. A )
12 eloni 
 |-  ( A e. On -> Ord A )
13 12 adantr 
 |-  ( ( A e. On /\ B e. On ) -> Ord A )
14 13 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> Ord A )
15 11 14 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( 1o e. A /\ Ord A ) )
16 ordelsuc 
 |-  ( ( 1o e. A /\ Ord A ) -> ( 1o e. A <-> suc 1o C_ A ) )
17 16 biimpd 
 |-  ( ( 1o e. A /\ Ord A ) -> ( 1o e. A -> suc 1o C_ A ) )
18 15 11 17 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> suc 1o C_ A )
19 10 18 eqsstrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> 2o C_ A )
20 omwordi 
 |-  ( ( 2o e. On /\ A e. On /\ B e. On ) -> ( 2o C_ A -> ( B .o 2o ) C_ ( B .o A ) ) )
21 8 19 20 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B .o 2o ) C_ ( B .o A ) )
22 2 21 eqsstrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B +o B ) C_ ( B .o A ) )
23 6 6 jca 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. On /\ B e. On ) )
24 simpr 
 |-  ( ( 1o e. A /\ A e. B ) -> A e. B )
25 oaordi 
 |-  ( ( B e. On /\ B e. On ) -> ( A e. B -> ( B +o A ) e. ( B +o B ) ) )
26 25 imp 
 |-  ( ( ( B e. On /\ B e. On ) /\ A e. B ) -> ( B +o A ) e. ( B +o B ) )
27 23 24 26 syl2an 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B +o A ) e. ( B +o B ) )
28 22 27 sseldd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B +o A ) e. ( B .o A ) )
29 28 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( ( 1o e. A /\ A e. B ) -> ( B +o A ) e. ( B .o A ) ) )