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 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )