[STATEMENT]
lemma add_conj_le:
  shows "z + cnj z \<le> 2 * cmod z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
have z: "z + cnj z = 2 * Re z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + cnj z = complex_of_real (2 * Re z)
[PROOF STEP]
by (simp add: complex_add_cnj)
[PROOF STATE]
proof (state)
this:
z + cnj z = complex_of_real (2 * Re z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
have "Re z \<le> cmod z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re z \<le> cmod z
[PROOF STEP]
by (simp add: complex_Re_le_cmod)
[PROOF STATE]
proof (state)
this:
Re z \<le> cmod z

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
hence "2 *complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)"
[PROOF STATE]
proof (prove)
using this:
Re z \<le> cmod z

goal (1 subgoal):
 1. 2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)
[PROOF STEP]
using less_eq_complex_def
[PROOF STATE]
proof (prove)
using this:
Re z \<le> cmod z
(?x \<le> ?y) = (Re ?x \<le> Re ?y \<and> Im ?x = Im ?y)

goal (1 subgoal):
 1. 2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)
z + cnj z = complex_of_real (2 * Re z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z + cnj z \<le> complex_of_real (2 * cmod z)

goal:
No subgoals!
[PROOF STEP]
qed