Step |
Hyp |
Ref |
Expression |
1 |
|
prodge0rd.1 |
|- ( ph -> A e. RR+ ) |
2 |
|
prodge0rd.2 |
|- ( ph -> B e. RR ) |
3 |
|
prodge0rd.3 |
|- ( ph -> 0 <_ ( A x. B ) ) |
4 |
|
0red |
|- ( ph -> 0 e. RR ) |
5 |
1
|
rpred |
|- ( ph -> A e. RR ) |
6 |
5 2
|
remulcld |
|- ( ph -> ( A x. B ) e. RR ) |
7 |
4 6 3
|
lensymd |
|- ( ph -> -. ( A x. B ) < 0 ) |
8 |
5
|
adantr |
|- ( ( ph /\ 0 < -u B ) -> A e. RR ) |
9 |
2
|
renegcld |
|- ( ph -> -u B e. RR ) |
10 |
9
|
adantr |
|- ( ( ph /\ 0 < -u B ) -> -u B e. RR ) |
11 |
1
|
rpgt0d |
|- ( ph -> 0 < A ) |
12 |
11
|
adantr |
|- ( ( ph /\ 0 < -u B ) -> 0 < A ) |
13 |
|
simpr |
|- ( ( ph /\ 0 < -u B ) -> 0 < -u B ) |
14 |
8 10 12 13
|
mulgt0d |
|- ( ( ph /\ 0 < -u B ) -> 0 < ( A x. -u B ) ) |
15 |
5
|
recnd |
|- ( ph -> A e. CC ) |
16 |
15
|
adantr |
|- ( ( ph /\ 0 < -u B ) -> A e. CC ) |
17 |
2
|
recnd |
|- ( ph -> B e. CC ) |
18 |
17
|
adantr |
|- ( ( ph /\ 0 < -u B ) -> B e. CC ) |
19 |
16 18
|
mulneg2d |
|- ( ( ph /\ 0 < -u B ) -> ( A x. -u B ) = -u ( A x. B ) ) |
20 |
14 19
|
breqtrd |
|- ( ( ph /\ 0 < -u B ) -> 0 < -u ( A x. B ) ) |
21 |
20
|
ex |
|- ( ph -> ( 0 < -u B -> 0 < -u ( A x. B ) ) ) |
22 |
2
|
lt0neg1d |
|- ( ph -> ( B < 0 <-> 0 < -u B ) ) |
23 |
6
|
lt0neg1d |
|- ( ph -> ( ( A x. B ) < 0 <-> 0 < -u ( A x. B ) ) ) |
24 |
21 22 23
|
3imtr4d |
|- ( ph -> ( B < 0 -> ( A x. B ) < 0 ) ) |
25 |
7 24
|
mtod |
|- ( ph -> -. B < 0 ) |
26 |
4 2 25
|
nltled |
|- ( ph -> 0 <_ B ) |