Metamath Proof Explorer

Theorem rpneg

Description: Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of Apostol p. 20. (Contributed by NM, 7-Nov-2008)

Ref Expression
Assertion rpneg 
|- ( ( A e. RR /\ A =/= 0 ) -> ( A e. RR+ <-> -. -u A e. RR+ ) )

Proof

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+ ) )