Step |
Hyp |
Ref |
Expression |
1 |
|
mulgt0con2d.a |
|- ( ph -> A e. RR ) |
2 |
|
mulgt0con2d.b |
|- ( ph -> B e. RR ) |
3 |
|
mulgt0con2d.1 |
|- ( ph -> 0 < A ) |
4 |
|
mulgt0con2d.2 |
|- ( ph -> ( A x. B ) < 0 ) |
5 |
1 2
|
remulcld |
|- ( ph -> ( A x. B ) e. RR ) |
6 |
1
|
adantr |
|- ( ( ph /\ 0 < B ) -> A e. RR ) |
7 |
2
|
adantr |
|- ( ( ph /\ 0 < B ) -> B e. RR ) |
8 |
3
|
adantr |
|- ( ( ph /\ 0 < B ) -> 0 < A ) |
9 |
|
simpr |
|- ( ( ph /\ 0 < B ) -> 0 < B ) |
10 |
6 7 8 9
|
mulgt0d |
|- ( ( ph /\ 0 < B ) -> 0 < ( A x. B ) ) |
11 |
10
|
ex |
|- ( ph -> ( 0 < B -> 0 < ( A x. B ) ) ) |
12 |
|
remul01 |
|- ( A e. RR -> ( A x. 0 ) = 0 ) |
13 |
1 12
|
syl |
|- ( ph -> ( A x. 0 ) = 0 ) |
14 |
|
oveq2 |
|- ( B = 0 -> ( A x. B ) = ( A x. 0 ) ) |
15 |
14
|
eqeq1d |
|- ( B = 0 -> ( ( A x. B ) = 0 <-> ( A x. 0 ) = 0 ) ) |
16 |
13 15
|
syl5ibrcom |
|- ( ph -> ( B = 0 -> ( A x. B ) = 0 ) ) |
17 |
2 5 11 16
|
mulgt0con1dlem |
|- ( ph -> ( ( A x. B ) < 0 -> B < 0 ) ) |
18 |
4 17
|
mpd |
|- ( ph -> B < 0 ) |