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 ∈ ℝ ∧ A ≠ 0 → A ∈ ℝ + ↔ ¬ − A ∈ ℝ +

Proof

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