Step |
Hyp |
Ref |
Expression |
1 |
|
mul2lt0.1 |
|- ( ph -> A e. RR ) |
2 |
|
mul2lt0.2 |
|- ( ph -> B e. RR ) |
3 |
|
mul2lt0.3 |
|- ( ph -> ( A x. B ) < 0 ) |
4 |
1 2
|
remulcld |
|- ( ph -> ( A x. B ) e. RR ) |
5 |
4
|
adantr |
|- ( ( ph /\ B < 0 ) -> ( A x. B ) e. RR ) |
6 |
|
0red |
|- ( ( ph /\ B < 0 ) -> 0 e. RR ) |
7 |
|
negelrp |
|- ( B e. RR -> ( -u B e. RR+ <-> B < 0 ) ) |
8 |
2 7
|
syl |
|- ( ph -> ( -u B e. RR+ <-> B < 0 ) ) |
9 |
8
|
biimpar |
|- ( ( ph /\ B < 0 ) -> -u B e. RR+ ) |
10 |
3
|
adantr |
|- ( ( ph /\ B < 0 ) -> ( A x. B ) < 0 ) |
11 |
5 6 9 10
|
ltdiv1dd |
|- ( ( ph /\ B < 0 ) -> ( ( A x. B ) / -u B ) < ( 0 / -u B ) ) |
12 |
1
|
recnd |
|- ( ph -> A e. CC ) |
13 |
12
|
adantr |
|- ( ( ph /\ B < 0 ) -> A e. CC ) |
14 |
2
|
recnd |
|- ( ph -> B e. CC ) |
15 |
14
|
adantr |
|- ( ( ph /\ B < 0 ) -> B e. CC ) |
16 |
13 15
|
mulcld |
|- ( ( ph /\ B < 0 ) -> ( A x. B ) e. CC ) |
17 |
|
simpr |
|- ( ( ph /\ B < 0 ) -> B < 0 ) |
18 |
17
|
lt0ne0d |
|- ( ( ph /\ B < 0 ) -> B =/= 0 ) |
19 |
16 15 18
|
divneg2d |
|- ( ( ph /\ B < 0 ) -> -u ( ( A x. B ) / B ) = ( ( A x. B ) / -u B ) ) |
20 |
13 15 18
|
divcan4d |
|- ( ( ph /\ B < 0 ) -> ( ( A x. B ) / B ) = A ) |
21 |
20
|
negeqd |
|- ( ( ph /\ B < 0 ) -> -u ( ( A x. B ) / B ) = -u A ) |
22 |
19 21
|
eqtr3d |
|- ( ( ph /\ B < 0 ) -> ( ( A x. B ) / -u B ) = -u A ) |
23 |
15
|
negcld |
|- ( ( ph /\ B < 0 ) -> -u B e. CC ) |
24 |
15 18
|
negne0d |
|- ( ( ph /\ B < 0 ) -> -u B =/= 0 ) |
25 |
23 24
|
div0d |
|- ( ( ph /\ B < 0 ) -> ( 0 / -u B ) = 0 ) |
26 |
11 22 25
|
3brtr3d |
|- ( ( ph /\ B < 0 ) -> -u A < 0 ) |
27 |
1
|
adantr |
|- ( ( ph /\ B < 0 ) -> A e. RR ) |
28 |
27
|
lt0neg2d |
|- ( ( ph /\ B < 0 ) -> ( 0 < A <-> -u A < 0 ) ) |
29 |
26 28
|
mpbird |
|- ( ( ph /\ B < 0 ) -> 0 < A ) |