| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mullt0b1d.a |
|- ( ph -> A e. RR ) |
| 2 |
|
mullt0b1d.b |
|- ( ph -> B e. RR ) |
| 3 |
|
mullt0b1d.1 |
|- ( ph -> A < 0 ) |
| 4 |
|
mulltgt0d.2 |
|- ( ph -> 0 < B ) |
| 5 |
3
|
lt0ne0d |
|- ( ph -> A =/= 0 ) |
| 6 |
4
|
gt0ne0d |
|- ( ph -> B =/= 0 ) |
| 7 |
5 6
|
jca |
|- ( ph -> ( A =/= 0 /\ B =/= 0 ) ) |
| 8 |
|
neanior |
|- ( ( A =/= 0 /\ B =/= 0 ) <-> -. ( A = 0 \/ B = 0 ) ) |
| 9 |
7 8
|
sylib |
|- ( ph -> -. ( A = 0 \/ B = 0 ) ) |
| 10 |
1 2
|
sn-remul0ord |
|- ( ph -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) ) |
| 11 |
9 10
|
mtbird |
|- ( ph -> -. ( A x. B ) = 0 ) |
| 12 |
|
0red |
|- ( ph -> 0 e. RR ) |
| 13 |
1 12 3
|
ltnsymd |
|- ( ph -> -. 0 < A ) |
| 14 |
1 2 4
|
mulgt0b2d |
|- ( ph -> ( 0 < A <-> 0 < ( A x. B ) ) ) |
| 15 |
13 14
|
mtbid |
|- ( ph -> -. 0 < ( A x. B ) ) |
| 16 |
|
ioran |
|- ( -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) <-> ( -. ( A x. B ) = 0 /\ -. 0 < ( A x. B ) ) ) |
| 17 |
11 15 16
|
sylanbrc |
|- ( ph -> -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) ) |
| 18 |
1 2
|
remulcld |
|- ( ph -> ( A x. B ) e. RR ) |
| 19 |
18 12
|
lttrid |
|- ( ph -> ( ( A x. B ) < 0 <-> -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) ) ) |
| 20 |
17 19
|
mpbird |
|- ( ph -> ( A x. B ) < 0 ) |