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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )

Proof

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