This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: The absolute value of 0. (Contributed by NM, 26-Mar-2005) (Revised by Mario Carneiro, 29-May-2016)
|
|
Ref |
Expression |
|
Assertion |
abs0 |
⊢ ( abs ‘ 0 ) = 0 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
0cn |
⊢ 0 ∈ ℂ |
| 2 |
|
absval |
⊢ ( 0 ∈ ℂ → ( abs ‘ 0 ) = ( √ ‘ ( 0 · ( ∗ ‘ 0 ) ) ) ) |
| 3 |
1 2
|
ax-mp |
⊢ ( abs ‘ 0 ) = ( √ ‘ ( 0 · ( ∗ ‘ 0 ) ) ) |
| 4 |
1
|
cjcli |
⊢ ( ∗ ‘ 0 ) ∈ ℂ |
| 5 |
4
|
mul02i |
⊢ ( 0 · ( ∗ ‘ 0 ) ) = 0 |
| 6 |
5
|
fveq2i |
⊢ ( √ ‘ ( 0 · ( ∗ ‘ 0 ) ) ) = ( √ ‘ 0 ) |
| 7 |
|
sqrt0 |
⊢ ( √ ‘ 0 ) = 0 |
| 8 |
3 6 7
|
3eqtri |
⊢ ( abs ‘ 0 ) = 0 |