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 mullidi ⊢ ( 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 mulrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 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 mulrid ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · 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 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )