Metamath Proof Explorer

Theorem addltmul

Description: Sum is less than product for numbers greater than 2. (Contributed by Stefan Allan, 24-Sep-2010)

Ref Expression
Assertion addltmul 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 2 < A /\ 2 < B ) ) -> ( A + B ) < ( A x. B ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1re 
 |-  1 e. RR
3 ltsub1 
 |-  ( ( 2 e. RR /\ A e. RR /\ 1 e. RR ) -> ( 2 < A <-> ( 2 - 1 ) < ( A - 1 ) ) )
4 1 2 3 mp3an13 
 |-  ( A e. RR -> ( 2 < A <-> ( 2 - 1 ) < ( A - 1 ) ) )
5 2m1e1 
 |-  ( 2 - 1 ) = 1
6 5 breq1i 
 |-  ( ( 2 - 1 ) < ( A - 1 ) <-> 1 < ( A - 1 ) )
7 4 6 bitrdi 
 |-  ( A e. RR -> ( 2 < A <-> 1 < ( A - 1 ) ) )
8 ltsub1 
 |-  ( ( 2 e. RR /\ B e. RR /\ 1 e. RR ) -> ( 2 < B <-> ( 2 - 1 ) < ( B - 1 ) ) )
9 1 2 8 mp3an13 
 |-  ( B e. RR -> ( 2 < B <-> ( 2 - 1 ) < ( B - 1 ) ) )
10 5 breq1i 
 |-  ( ( 2 - 1 ) < ( B - 1 ) <-> 1 < ( B - 1 ) )
11 9 10 bitrdi 
 |-  ( B e. RR -> ( 2 < B <-> 1 < ( B - 1 ) ) )
12 7 11 bi2anan9 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 2 < A /\ 2 < B ) <-> ( 1 < ( A - 1 ) /\ 1 < ( B - 1 ) ) ) )
13 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
14 peano2rem 
 |-  ( B e. RR -> ( B - 1 ) e. RR )
15 mulgt1 
 |-  ( ( ( ( A - 1 ) e. RR /\ ( B - 1 ) e. RR ) /\ ( 1 < ( A - 1 ) /\ 1 < ( B - 1 ) ) ) -> 1 < ( ( A - 1 ) x. ( B - 1 ) ) )
16 15 ex 
 |-  ( ( ( A - 1 ) e. RR /\ ( B - 1 ) e. RR ) -> ( ( 1 < ( A - 1 ) /\ 1 < ( B - 1 ) ) -> 1 < ( ( A - 1 ) x. ( B - 1 ) ) ) )
17 13 14 16 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 1 < ( A - 1 ) /\ 1 < ( B - 1 ) ) -> 1 < ( ( A - 1 ) x. ( B - 1 ) ) ) )
18 12 17 sylbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 2 < A /\ 2 < B ) -> 1 < ( ( A - 1 ) x. ( B - 1 ) ) ) )
19 recn 
 |-  ( A e. RR -> A e. CC )
20 recn 
 |-  ( B e. RR -> B e. CC )
21 ax-1cn 
 |-  1 e. CC
22 mulsub 
 |-  ( ( ( A e. CC /\ 1 e. CC ) /\ ( B e. CC /\ 1 e. CC ) ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
23 21 22 mpanl2 
 |-  ( ( A e. CC /\ ( B e. CC /\ 1 e. CC ) ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
24 21 23 mpanr2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
25 19 20 24 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
26 25 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 1 < ( ( A - 1 ) x. ( B - 1 ) ) <-> 1 < ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) ) )
27 remulcl 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A x. 1 ) e. RR )
28 2 27 mpan2 
 |-  ( A e. RR -> ( A x. 1 ) e. RR )
29 remulcl 
 |-  ( ( B e. RR /\ 1 e. RR ) -> ( B x. 1 ) e. RR )
30 2 29 mpan2 
 |-  ( B e. RR -> ( B x. 1 ) e. RR )
31 readdcl 
 |-  ( ( ( A x. 1 ) e. RR /\ ( B x. 1 ) e. RR ) -> ( ( A x. 1 ) + ( B x. 1 ) ) e. RR )
32 28 30 31 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. 1 ) + ( B x. 1 ) ) e. RR )
33 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
34 2 2 remulcli 
 |-  ( 1 x. 1 ) e. RR
35 readdcl 
 |-  ( ( ( A x. B ) e. RR /\ ( 1 x. 1 ) e. RR ) -> ( ( A x. B ) + ( 1 x. 1 ) ) e. RR )
36 33 34 35 sylancl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) + ( 1 x. 1 ) ) e. RR )
37 ltaddsub2 
 |-  ( ( ( ( A x. 1 ) + ( B x. 1 ) ) e. RR /\ 1 e. RR /\ ( ( A x. B ) + ( 1 x. 1 ) ) e. RR ) -> ( ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + ( 1 x. 1 ) ) <-> 1 < ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) ) )
38 2 37 mp3an2 
 |-  ( ( ( ( A x. 1 ) + ( B x. 1 ) ) e. RR /\ ( ( A x. B ) + ( 1 x. 1 ) ) e. RR ) -> ( ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + ( 1 x. 1 ) ) <-> 1 < ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) ) )
39 32 36 38 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + ( 1 x. 1 ) ) <-> 1 < ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) ) )
40 1t1e1 
 |-  ( 1 x. 1 ) = 1
41 40 oveq2i 
 |-  ( ( A x. B ) + ( 1 x. 1 ) ) = ( ( A x. B ) + 1 )
42 41 breq2i 
 |-  ( ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + ( 1 x. 1 ) ) <-> ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + 1 ) )
43 39 42 bitr3di 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 1 < ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) <-> ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + 1 ) ) )
44 ltadd1 
 |-  ( ( ( ( A x. 1 ) + ( B x. 1 ) ) e. RR /\ ( A x. B ) e. RR /\ 1 e. RR ) -> ( ( ( A x. 1 ) + ( B x. 1 ) ) < ( A x. B ) <-> ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + 1 ) ) )
45 2 44 mp3an3 
 |-  ( ( ( ( A x. 1 ) + ( B x. 1 ) ) e. RR /\ ( A x. B ) e. RR ) -> ( ( ( A x. 1 ) + ( B x. 1 ) ) < ( A x. B ) <-> ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + 1 ) ) )
46 32 33 45 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A x. 1 ) + ( B x. 1 ) ) < ( A x. B ) <-> ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + 1 ) ) )
47 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
48 ax-1rid 
 |-  ( B e. RR -> ( B x. 1 ) = B )
49 47 48 oveqan12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. 1 ) + ( B x. 1 ) ) = ( A + B ) )
50 49 breq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A x. 1 ) + ( B x. 1 ) ) < ( A x. B ) <-> ( A + B ) < ( A x. B ) ) )
51 46 50 bitr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A x. 1 ) + ( B x. 1 ) ) + 1 ) < ( ( A x. B ) + 1 ) <-> ( A + B ) < ( A x. B ) ) )
52 26 43 51 3bitrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 1 < ( ( A - 1 ) x. ( B - 1 ) ) <-> ( A + B ) < ( A x. B ) ) )
53 18 52 sylibd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 2 < A /\ 2 < B ) -> ( A + B ) < ( A x. B ) ) )
54 53 imp 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 2 < A /\ 2 < B ) ) -> ( A + B ) < ( A x. B ) )