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 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ∈ ℝ+ ↔ ¬ - 𝐴 ∈ ℝ+ ) )

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 ltle ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
3 1 2 mpan ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
4 3 imp ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ≤ 𝐴 )
5 4 olcd ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ¬ - 𝐴 ∈ ℝ ∨ 0 ≤ 𝐴 ) )
6 renegcl ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
7 6 pm2.24d ( 𝐴 ∈ ℝ → ( ¬ - 𝐴 ∈ ℝ → 0 < 𝐴 ) )
8 7 adantr ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ¬ - 𝐴 ∈ ℝ → 0 < 𝐴 ) )
9 ltlen ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 ↔ ( 0 ≤ 𝐴𝐴 ≠ 0 ) ) )
10 1 9 mpan ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( 0 ≤ 𝐴𝐴 ≠ 0 ) ) )
11 10 biimprd ( 𝐴 ∈ ℝ → ( ( 0 ≤ 𝐴𝐴 ≠ 0 ) → 0 < 𝐴 ) )
12 11 expcomd ( 𝐴 ∈ ℝ → ( 𝐴 ≠ 0 → ( 0 ≤ 𝐴 → 0 < 𝐴 ) ) )
13 12 imp ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 ≤ 𝐴 → 0 < 𝐴 ) )
14 8 13 jaod ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( ¬ - 𝐴 ∈ ℝ ∨ 0 ≤ 𝐴 ) → 0 < 𝐴 ) )
15 simpl ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
16 14 15 jctild ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( ¬ - 𝐴 ∈ ℝ ∨ 0 ≤ 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) )
17 5 16 impbid2 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ↔ ( ¬ - 𝐴 ∈ ℝ ∨ 0 ≤ 𝐴 ) ) )
18 lenlt ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
19 1 18 mpan ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
20 lt0neg1 ( 𝐴 ∈ ℝ → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) )
21 20 notbid ( 𝐴 ∈ ℝ → ( ¬ 𝐴 < 0 ↔ ¬ 0 < - 𝐴 ) )
22 19 21 bitrd ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ¬ 0 < - 𝐴 ) )
23 22 adantr ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 ≤ 𝐴 ↔ ¬ 0 < - 𝐴 ) )
24 23 orbi2d ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( ¬ - 𝐴 ∈ ℝ ∨ 0 ≤ 𝐴 ) ↔ ( ¬ - 𝐴 ∈ ℝ ∨ ¬ 0 < - 𝐴 ) ) )
25 17 24 bitrd ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ↔ ( ¬ - 𝐴 ∈ ℝ ∨ ¬ 0 < - 𝐴 ) ) )
26 ianor ( ¬ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ) ↔ ( ¬ - 𝐴 ∈ ℝ ∨ ¬ 0 < - 𝐴 ) )
27 25 26 bitr4di ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ↔ ¬ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ) ) )
28 elrp ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
29 elrp ( - 𝐴 ∈ ℝ+ ↔ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ) )
30 29 notbii ( ¬ - 𝐴 ∈ ℝ+ ↔ ¬ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ) )
31 27 28 30 3bitr4g ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ∈ ℝ+ ↔ ¬ - 𝐴 ∈ ℝ+ ) )