Description: The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of Gleason p. 133. (Contributed by NM, 27-Jul-1999) (Revised by Mario Carneiro, 7-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | absval | ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 | ⊢ ( 𝑥 = 𝐴 → ( ∗ ‘ 𝑥 ) = ( ∗ ‘ 𝐴 ) ) | |
| 2 | oveq12 | ⊢ ( ( 𝑥 = 𝐴 ∧ ( ∗ ‘ 𝑥 ) = ( ∗ ‘ 𝐴 ) ) → ( 𝑥 · ( ∗ ‘ 𝑥 ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) | |
| 3 | 1 2 | mpdan | ⊢ ( 𝑥 = 𝐴 → ( 𝑥 · ( ∗ ‘ 𝑥 ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) |
| 4 | 3 | fveq2d | ⊢ ( 𝑥 = 𝐴 → ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ) |
| 5 | df-abs | ⊢ abs = ( 𝑥 ∈ ℂ ↦ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ) | |
| 6 | fvex | ⊢ ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ V | |
| 7 | 4 5 6 | fvmpt | ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ) |