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