Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
|- 0 e. RR |
2 |
|
ltle |
|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) ) |
3 |
1 2
|
mpan |
|- ( A e. RR -> ( 0 < A -> 0 <_ A ) ) |
4 |
3
|
imp |
|- ( ( A e. RR /\ 0 < A ) -> 0 <_ A ) |
5 |
4
|
olcd |
|- ( ( A e. RR /\ 0 < A ) -> ( -. -u A e. RR \/ 0 <_ A ) ) |
6 |
|
renegcl |
|- ( A e. RR -> -u A e. RR ) |
7 |
6
|
pm2.24d |
|- ( A e. RR -> ( -. -u A e. RR -> 0 < A ) ) |
8 |
7
|
adantr |
|- ( ( A e. RR /\ A =/= 0 ) -> ( -. -u A e. RR -> 0 < A ) ) |
9 |
|
ltlen |
|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> ( 0 <_ A /\ A =/= 0 ) ) ) |
10 |
1 9
|
mpan |
|- ( A e. RR -> ( 0 < A <-> ( 0 <_ A /\ A =/= 0 ) ) ) |
11 |
10
|
biimprd |
|- ( A e. RR -> ( ( 0 <_ A /\ A =/= 0 ) -> 0 < A ) ) |
12 |
11
|
expcomd |
|- ( A e. RR -> ( A =/= 0 -> ( 0 <_ A -> 0 < A ) ) ) |
13 |
12
|
imp |
|- ( ( A e. RR /\ A =/= 0 ) -> ( 0 <_ A -> 0 < A ) ) |
14 |
8 13
|
jaod |
|- ( ( A e. RR /\ A =/= 0 ) -> ( ( -. -u A e. RR \/ 0 <_ A ) -> 0 < A ) ) |
15 |
|
simpl |
|- ( ( A e. RR /\ A =/= 0 ) -> A e. RR ) |
16 |
14 15
|
jctild |
|- ( ( A e. RR /\ A =/= 0 ) -> ( ( -. -u A e. RR \/ 0 <_ A ) -> ( A e. RR /\ 0 < A ) ) ) |
17 |
5 16
|
impbid2 |
|- ( ( A e. RR /\ A =/= 0 ) -> ( ( A e. RR /\ 0 < A ) <-> ( -. -u A e. RR \/ 0 <_ A ) ) ) |
18 |
|
lenlt |
|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> -. A < 0 ) ) |
19 |
1 18
|
mpan |
|- ( A e. RR -> ( 0 <_ A <-> -. A < 0 ) ) |
20 |
|
lt0neg1 |
|- ( A e. RR -> ( A < 0 <-> 0 < -u A ) ) |
21 |
20
|
notbid |
|- ( A e. RR -> ( -. A < 0 <-> -. 0 < -u A ) ) |
22 |
19 21
|
bitrd |
|- ( A e. RR -> ( 0 <_ A <-> -. 0 < -u A ) ) |
23 |
22
|
adantr |
|- ( ( A e. RR /\ A =/= 0 ) -> ( 0 <_ A <-> -. 0 < -u A ) ) |
24 |
23
|
orbi2d |
|- ( ( A e. RR /\ A =/= 0 ) -> ( ( -. -u A e. RR \/ 0 <_ A ) <-> ( -. -u A e. RR \/ -. 0 < -u A ) ) ) |
25 |
17 24
|
bitrd |
|- ( ( A e. RR /\ A =/= 0 ) -> ( ( A e. RR /\ 0 < A ) <-> ( -. -u A e. RR \/ -. 0 < -u A ) ) ) |
26 |
|
ianor |
|- ( -. ( -u A e. RR /\ 0 < -u A ) <-> ( -. -u A e. RR \/ -. 0 < -u A ) ) |
27 |
25 26
|
bitr4di |
|- ( ( A e. RR /\ A =/= 0 ) -> ( ( A e. RR /\ 0 < A ) <-> -. ( -u A e. RR /\ 0 < -u A ) ) ) |
28 |
|
elrp |
|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) ) |
29 |
|
elrp |
|- ( -u A e. RR+ <-> ( -u A e. RR /\ 0 < -u A ) ) |
30 |
29
|
notbii |
|- ( -. -u A e. RR+ <-> -. ( -u A e. RR /\ 0 < -u A ) ) |
31 |
27 28 30
|
3bitr4g |
|- ( ( A e. RR /\ A =/= 0 ) -> ( A e. RR+ <-> -. -u A e. RR+ ) ) |