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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 2 < A ∧ 2 < B → A + B < A ⁢ B

Proof

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