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 B 2 < A 2 < B A + B < A B

Proof

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