Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( 1 < A /\ 1 < B ) -> 1 < A ) |
2 |
1
|
a1i |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 1 < A /\ 1 < B ) -> 1 < A ) ) |
3 |
|
0lt1 |
|- 0 < 1 |
4 |
|
0re |
|- 0 e. RR |
5 |
|
1re |
|- 1 e. RR |
6 |
|
lttr |
|- ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) ) |
7 |
4 5 6
|
mp3an12 |
|- ( A e. RR -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) ) |
8 |
3 7
|
mpani |
|- ( A e. RR -> ( 1 < A -> 0 < A ) ) |
9 |
8
|
adantr |
|- ( ( A e. RR /\ B e. RR ) -> ( 1 < A -> 0 < A ) ) |
10 |
|
ltmul2 |
|- ( ( 1 e. RR /\ B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 < B <-> ( A x. 1 ) < ( A x. B ) ) ) |
11 |
10
|
biimpd |
|- ( ( 1 e. RR /\ B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 < B -> ( A x. 1 ) < ( A x. B ) ) ) |
12 |
5 11
|
mp3an1 |
|- ( ( B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 < B -> ( A x. 1 ) < ( A x. B ) ) ) |
13 |
12
|
exp32 |
|- ( B e. RR -> ( A e. RR -> ( 0 < A -> ( 1 < B -> ( A x. 1 ) < ( A x. B ) ) ) ) ) |
14 |
13
|
impcom |
|- ( ( A e. RR /\ B e. RR ) -> ( 0 < A -> ( 1 < B -> ( A x. 1 ) < ( A x. B ) ) ) ) |
15 |
9 14
|
syld |
|- ( ( A e. RR /\ B e. RR ) -> ( 1 < A -> ( 1 < B -> ( A x. 1 ) < ( A x. B ) ) ) ) |
16 |
15
|
impd |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 1 < A /\ 1 < B ) -> ( A x. 1 ) < ( A x. B ) ) ) |
17 |
|
ax-1rid |
|- ( A e. RR -> ( A x. 1 ) = A ) |
18 |
17
|
adantr |
|- ( ( A e. RR /\ B e. RR ) -> ( A x. 1 ) = A ) |
19 |
18
|
breq1d |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A x. 1 ) < ( A x. B ) <-> A < ( A x. B ) ) ) |
20 |
16 19
|
sylibd |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 1 < A /\ 1 < B ) -> A < ( A x. B ) ) ) |
21 |
2 20
|
jcad |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 1 < A /\ 1 < B ) -> ( 1 < A /\ A < ( A x. B ) ) ) ) |
22 |
|
remulcl |
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR ) |
23 |
|
lttr |
|- ( ( 1 e. RR /\ A e. RR /\ ( A x. B ) e. RR ) -> ( ( 1 < A /\ A < ( A x. B ) ) -> 1 < ( A x. B ) ) ) |
24 |
5 23
|
mp3an1 |
|- ( ( A e. RR /\ ( A x. B ) e. RR ) -> ( ( 1 < A /\ A < ( A x. B ) ) -> 1 < ( A x. B ) ) ) |
25 |
22 24
|
syldan |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 1 < A /\ A < ( A x. B ) ) -> 1 < ( A x. B ) ) ) |
26 |
21 25
|
syld |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 1 < A /\ 1 < B ) -> 1 < ( A x. B ) ) ) |
27 |
26
|
imp |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < ( A x. B ) ) |