Metamath Proof Explorer


Theorem addltmulALT

Description: A proof readability experiment for addltmul . (Contributed by Stefan Allan, 30-Oct-2010) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion addltmulALT ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 2 < 𝐴 )
2 2re 2 ∈ ℝ
3 2 a1i ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 2 ∈ ℝ )
4 simpl ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 𝐴 ∈ ℝ )
5 1re 1 ∈ ℝ
6 5 a1i ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 1 ∈ ℝ )
7 ltsub1 ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 2 < 𝐴 ↔ ( 2 − 1 ) < ( 𝐴 − 1 ) ) )
8 3 4 6 7 syl3anc ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → ( 2 < 𝐴 ↔ ( 2 − 1 ) < ( 𝐴 − 1 ) ) )
9 2cn 2 ∈ ℂ
10 ax-1cn 1 ∈ ℂ
11 df-2 2 = ( 1 + 1 )
12 11 eqcomi ( 1 + 1 ) = 2
13 9 10 10 12 subaddrii ( 2 − 1 ) = 1
14 13 breq1i ( ( 2 − 1 ) < ( 𝐴 − 1 ) ↔ 1 < ( 𝐴 − 1 ) )
15 14 a1i ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → ( ( 2 − 1 ) < ( 𝐴 − 1 ) ↔ 1 < ( 𝐴 − 1 ) ) )
16 8 15 bitrd ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → ( 2 < 𝐴 ↔ 1 < ( 𝐴 − 1 ) ) )
17 1 16 mpbid ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 1 < ( 𝐴 − 1 ) )
18 simpr ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 2 < 𝐵 )
19 2 a1i ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 2 ∈ ℝ )
20 simpl ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 𝐵 ∈ ℝ )
21 5 a1i ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 1 ∈ ℝ )
22 ltsub1 ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 2 < 𝐵 ↔ ( 2 − 1 ) < ( 𝐵 − 1 ) ) )
23 19 20 21 22 syl3anc ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → ( 2 < 𝐵 ↔ ( 2 − 1 ) < ( 𝐵 − 1 ) ) )
24 13 breq1i ( ( 2 − 1 ) < ( 𝐵 − 1 ) ↔ 1 < ( 𝐵 − 1 ) )
25 24 a1i ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → ( ( 2 − 1 ) < ( 𝐵 − 1 ) ↔ 1 < ( 𝐵 − 1 ) ) )
26 23 25 bitrd ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → ( 2 < 𝐵 ↔ 1 < ( 𝐵 − 1 ) ) )
27 18 26 mpbid ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 1 < ( 𝐵 − 1 ) )
28 17 27 anim12i ( ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) ) → ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) )
29 28 an4s ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) )
30 peano2rem ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
31 peano2rem ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
32 30 31 anim12i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐵 − 1 ) ∈ ℝ ) )
33 32 anim1i ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) → ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐵 − 1 ) ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) )
34 mulgt1 ( ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐵 − 1 ) ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) )
35 33 34 syl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) )
36 35 ex ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ) )
37 36 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ) )
38 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
39 10 a1i ( 𝐴 ∈ ℝ → 1 ∈ ℂ )
40 38 39 jca ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) )
41 recn ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
42 10 a1i ( 𝐵 ∈ ℝ → 1 ∈ ℂ )
43 41 42 jca ( 𝐵 ∈ ℝ → ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) )
44 40 43 anim12i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) ) )
45 mulsub ( ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) ) → ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) )
46 44 45 syl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) )
47 46 breq2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
48 47 biimpd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) → 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
49 48 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) → 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
50 10 mulid2i ( 1 · 1 ) = 1
51 eqcom ( ( 1 · 1 ) = 1 ↔ 1 = ( 1 · 1 ) )
52 51 biimpi ( ( 1 · 1 ) = 1 → 1 = ( 1 · 1 ) )
53 50 52 mp1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 1 = ( 1 · 1 ) )
54 53 oveq2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) + 1 ) = ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) )
55 mulid1 ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
56 eqcom ( ( 𝐴 · 1 ) = 𝐴𝐴 = ( 𝐴 · 1 ) )
57 56 biimpi ( ( 𝐴 · 1 ) = 𝐴𝐴 = ( 𝐴 · 1 ) )
58 55 57 syl ( 𝐴 ∈ ℂ → 𝐴 = ( 𝐴 · 1 ) )
59 38 58 syl ( 𝐴 ∈ ℝ → 𝐴 = ( 𝐴 · 1 ) )
60 59 adantr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 = ( 𝐴 · 1 ) )
61 mulid1 ( 𝐵 ∈ ℂ → ( 𝐵 · 1 ) = 𝐵 )
62 41 61 syl ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
63 eqcom ( ( 𝐵 · 1 ) = 𝐵𝐵 = ( 𝐵 · 1 ) )
64 63 biimpi ( ( 𝐵 · 1 ) = 𝐵𝐵 = ( 𝐵 · 1 ) )
65 62 64 syl ( 𝐵 ∈ ℝ → 𝐵 = ( 𝐵 · 1 ) )
66 65 adantl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 = ( 𝐵 · 1 ) )
67 60 66 oveq12d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) = ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) )
68 54 67 oveq12d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) )
69 68 breq2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
70 readdcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
71 5 a1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 1 ∈ ℝ )
72 remulcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
73 readdcl ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ℝ )
74 72 71 73 syl2anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ℝ )
75 ltaddsub2 ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) ) )
76 70 71 74 75 syl3anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) ) )
77 ltadd1 ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ) )
78 70 72 71 77 syl3anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ) )
79 78 bicomd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ↔ ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
80 79 biimpd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
81 76 80 sylbird ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
82 69 81 sylbird ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
83 82 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
84 37 49 83 3syld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
85 29 84 mpd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )