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	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(A\in {ℝ}^{+}\leftrightarrow \neg -A\in {ℝ}^{+}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		ltle	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0<A\to 0\le A\right)$$
3	1 2	mpan	$$⊢A\in ℝ\to \left(0<A\to 0\le A\right)$$
4	3	imp	$$⊢\left(A\in ℝ\wedge 0<A\right)\to 0\le A$$
5	4	olcd	$$⊢\left(A\in ℝ\wedge 0<A\right)\to \left(\neg -A\in ℝ\vee 0\le A\right)$$
6		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
7	6	pm2.24d	$$⊢A\in ℝ\to \left(\neg -A\in ℝ\to 0<A\right)$$
8	7	adantr	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\neg -A\in ℝ\to 0<A\right)$$
9		ltlen	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0<A\leftrightarrow \left(0\le A\wedge A\ne 0\right)\right)$$
10	1 9	mpan	$$⊢A\in ℝ\to \left(0<A\leftrightarrow \left(0\le A\wedge A\ne 0\right)\right)$$
11	10	biimprd	$$⊢A\in ℝ\to \left(\left(0\le A\wedge A\ne 0\right)\to 0<A\right)$$
12	11	expcomd	$$⊢A\in ℝ\to \left(A\ne 0\to \left(0\le A\to 0<A\right)\right)$$
13	12	imp	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(0\le A\to 0<A\right)$$
14	8 13	jaod	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(\neg -A\in ℝ\vee 0\le A\right)\to 0<A\right)$$
15		simpl	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to A\in ℝ$$
16	14 15	jctild	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(\neg -A\in ℝ\vee 0\le A\right)\to \left(A\in ℝ\wedge 0<A\right)\right)$$
17	5 16	impbid2	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(A\in ℝ\wedge 0<A\right)\leftrightarrow \left(\neg -A\in ℝ\vee 0\le A\right)\right)$$
18		lenlt	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0\le A\leftrightarrow \neg A<0\right)$$
19	1 18	mpan	$$⊢A\in ℝ\to \left(0\le A\leftrightarrow \neg A<0\right)$$
20		lt0neg1	$$⊢A\in ℝ\to \left(A<0\leftrightarrow 0<-A\right)$$
21	20	notbid	$$⊢A\in ℝ\to \left(\neg A<0\leftrightarrow \neg 0<-A\right)$$
22	19 21	bitrd	$$⊢A\in ℝ\to \left(0\le A\leftrightarrow \neg 0<-A\right)$$
23	22	adantr	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(0\le A\leftrightarrow \neg 0<-A\right)$$
24	23	orbi2d	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(\neg -A\in ℝ\vee 0\le A\right)\leftrightarrow \left(\neg -A\in ℝ\vee \neg 0<-A\right)\right)$$
25	17 24	bitrd	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(A\in ℝ\wedge 0<A\right)\leftrightarrow \left(\neg -A\in ℝ\vee \neg 0<-A\right)\right)$$
26		ianor	$$⊢\neg \left(-A\in ℝ\wedge 0<-A\right)\leftrightarrow \left(\neg -A\in ℝ\vee \neg 0<-A\right)$$
27	25 26	bitr4di	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(A\in ℝ\wedge 0<A\right)\leftrightarrow \neg \left(-A\in ℝ\wedge 0<-A\right)\right)$$
28		elrp	$$⊢A\in {ℝ}^{+}\leftrightarrow \left(A\in ℝ\wedge 0<A\right)$$
29		elrp	$$⊢-A\in {ℝ}^{+}\leftrightarrow \left(-A\in ℝ\wedge 0<-A\right)$$
30	29	notbii	$$⊢\neg -A\in {ℝ}^{+}\leftrightarrow \neg \left(-A\in ℝ\wedge 0<-A\right)$$
31	27 28 30	3bitr4g	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(A\in {ℝ}^{+}\leftrightarrow \neg -A\in {ℝ}^{+}\right)$$