For this proof we follow Elliott H. Lieb and Michael Loss. From the assumptions, ∂ ∂ j | f | ∈ ∈ L loc 1 ( R n ) when viewed in the sense of distributions and ∂ ∂ j | f | ( x ) = Re ⁡ ⁡ ( f ¯ ¯ ( x ) | f ( x ) | ∂ ∂ j f ( x ) ) for almost every x such that f ( x ) ≠ ≠ 0 (and ∂ ∂ j | f | ( x ) = 0 if f ( x ) = 0 ). Moreover, Re ⁡ ⁡ ( f ¯ ¯ ( x ) | f ( x ) | i A j f ( x ) ) = Im ⁡ ⁡ ( A j f ) = 0. So ∇ ∇ | f | ( x ) = Re ⁡ ⁡ ( f ¯ ¯ ( x ) | f ( x ) | D f ( x ) ) ≤ ≤ | f ¯ ¯ ( x ) | f ( x ) | D f ( x ) | = | D f ( x ) | for almost every x such that f ( x ) ≠ ≠ 0 . The case that f ( x ) = 0 is similar.