| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sn-reclt0d.a |
|- ( ph -> A e. RR ) |
| 2 |
|
sn-reclt0d.z |
|- ( ph -> A < 0 ) |
| 3 |
2
|
lt0ne0d |
|- ( ph -> A =/= 0 ) |
| 4 |
1 3
|
sn-rereccld |
|- ( ph -> ( 1 /R A ) e. RR ) |
| 5 |
|
rernegcl |
|- ( A e. RR -> ( 0 -R A ) e. RR ) |
| 6 |
1 5
|
syl |
|- ( ph -> ( 0 -R A ) e. RR ) |
| 7 |
|
relt0neg1 |
|- ( A e. RR -> ( A < 0 <-> 0 < ( 0 -R A ) ) ) |
| 8 |
1 7
|
syl |
|- ( ph -> ( A < 0 <-> 0 < ( 0 -R A ) ) ) |
| 9 |
2 8
|
mpbid |
|- ( ph -> 0 < ( 0 -R A ) ) |
| 10 |
4 1
|
remulneg2d |
|- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R ( ( 1 /R A ) x. A ) ) ) |
| 11 |
1 3
|
rerecid2d |
|- ( ph -> ( ( 1 /R A ) x. A ) = 1 ) |
| 12 |
11
|
oveq2d |
|- ( ph -> ( 0 -R ( ( 1 /R A ) x. A ) ) = ( 0 -R 1 ) ) |
| 13 |
10 12
|
eqtrd |
|- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R 1 ) ) |
| 14 |
|
reneg1lt0 |
|- ( 0 -R 1 ) < 0 |
| 15 |
14
|
a1i |
|- ( ph -> ( 0 -R 1 ) < 0 ) |
| 16 |
13 15
|
eqbrtrd |
|- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) < 0 ) |
| 17 |
4 6 9 16
|
mulgt0con1d |
|- ( ph -> ( 1 /R A ) < 0 ) |