[STATEMENT]
lemma abs_complex_real[simp]: "abs x \<in> \<real>" for x :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in> \<real>
[PROOF STEP]
by (simp add: abs_complex_def)