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 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 ⊢A∈ℝ∧B∈ℝ→1=1⋅1
54 53 oveq2d ⊢A∈ℝ∧B∈ℝ→A⁢B+1=A⁢B+1⋅1
55 mulrid ⊢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 mulrid ⊢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