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