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