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