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