[STATEMENT]
lemma agsprod_assoc:"\<lbrakk>m \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (cut_tac less_linear[of "m" "0"], cut_tac less_linear[of "n" "0"],
       cut_tac mem_ant[of "x"],
      (erule disjE)+, simp,
      frule zmult_neg_neg[of "m" "n"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<noteq> 0; n \<noteq> 0; m < 0; n < 0; (\<exists>z. x = ant z) \<or> x = \<infinity>\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
 2. \<lbrakk>m \<noteq> 0; n \<noteq> 0; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; m < 0; n = 0 \<or> 0 < n\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
 3. \<lbrakk>m \<noteq> 0; n \<noteq> 0; n < 0 \<or> n = 0 \<or> 0 < n; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; m = 0 \<or> 0 < m\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (erule disjE, erule exE, simp add:asprod_mult,
      frule zmult_neg_neg[of "m" "n"], assumption+, simp+,
      erule disjE, simp,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp,
      erule disjE, erule exE, simp,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp add:asprod_mult,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<noteq> 0; n \<noteq> 0; n < 0 \<or> n = 0 \<or> 0 < n; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; m = 0 \<or> 0 < m\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (simp, (erule disjE)+,
      frule zmult_pos_neg[of "m" "n"], assumption+,
      simp,
      erule disjE, erule exE, simp add:asprod_mult,
      frule zmult_pos_neg[of "m" "n"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; 0 < m; 0 < n\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (frule zmult_pos_pos[of "m" "n"], assumption+,
      erule disjE, simp,
      erule disjE, erule exE, simp add:asprod_mult, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done