Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
⊢ 0 ∈ ℝ |
2 |
|
ltle |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) ) |
3 |
1 2
|
mpan2 |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 0 → 𝐴 ≤ 0 ) ) |
4 |
3
|
imdistani |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) ) |
5 |
|
absnid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 ) |
6 |
4 5
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 ) |
7 |
6
|
eqcomd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → - 𝐴 = ( abs ‘ 𝐴 ) ) |
8 |
|
0red |
⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ ) |
9 |
|
id |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ ) |
10 |
8 9
|
lenltd |
⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) ) |
11 |
10
|
bicomd |
⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 < 0 ↔ 0 ≤ 𝐴 ) ) |
12 |
11
|
pm5.32i |
⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 < 0 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) |
13 |
|
absid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 ) |
14 |
12 13
|
sylbi |
⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 < 0 ) → ( abs ‘ 𝐴 ) = 𝐴 ) |
15 |
14
|
eqcomd |
⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 < 0 ) → 𝐴 = ( abs ‘ 𝐴 ) ) |
16 |
7 15
|
ifeqda |
⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 < 0 , - 𝐴 , 𝐴 ) = ( abs ‘ 𝐴 ) ) |
17 |
16
|
eqcomd |
⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = if ( 𝐴 < 0 , - 𝐴 , 𝐴 ) ) |