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