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 e. RR /\ B e. RR ) /\ ( 2 < A /\ 2 < B ) ) -> ( A + B ) < ( A x. B ) )

Proof

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