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