[STATEMENT]
lemma rref_suc_if_zero_below_greatest:
  fixes A::"'a::{one, zero}^'n::{mod_type}^'m::{finite,one,plus,linorder}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and not_all_zero: "\<not> (\<forall>a. is_zero_row_upt_k a k A)" (*This premisse is necessary to assure the existence of the Greatest*)
  and all_zero_below_greatest: "\<forall>a. a>(GREATEST m. \<not> is_zero_row_upt_k m k A) \<longrightarrow> is_zero_row_upt_k a (Suc k) A"
  shows "reduced_row_echelon_form_upt_k A (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A (Suc k)
[PROOF STEP]
proof (rule reduced_row_echelon_form_upt_k_intro, auto)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) A; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) A; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
assume zero_i_suc: "is_zero_row_upt_k i (Suc k) A" and i_le_j: "i < j"
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i (Suc k) A
i < j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) A; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have zero_i: "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
using zero_i_suc
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) A

goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'a)

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k A

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) A; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have "i>(GREATEST m. \<not> is_zero_row_upt_k m k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) < i
[PROOF STEP]
by (rule greatest_less_zero_row[OF r zero_i not_all_zero])
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < i

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) A; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
hence "j>(GREATEST m. \<not> is_zero_row_upt_k m k A)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < i

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) < j
[PROOF STEP]
using i_le_j
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < i
i < j

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) < j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) A; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
thus "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < j

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
using all_zero_below_greatest
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < j
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j (Suc k) A

goal (3 subgoals):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 2. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 3. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 2. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 3. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 2. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 3. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
assume not_zero_i: "\<not> is_zero_row_upt_k i (Suc k) A"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i (Suc k) A

goal (3 subgoals):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) A \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 2. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 3. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show "A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using  greatest_less_zero_row[OF r _ not_all_zero] not_zero_i r all_zero_below_greatest
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k ?i k A \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k i (Suc k) A
reduced_row_echelon_form_upt_k A k
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k ?i k A \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k i (Suc k) A
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
assume i: "i < i + 1" and not_zero_i: "\<not> is_zero_row_upt_k i (Suc k) A" and not_zero_suc_i: "\<not> is_zero_row_upt_k (i + 1) (Suc k) A"
[PROOF STATE]
proof (state)
this:
i < i + (1::'m)
\<not> is_zero_row_upt_k i (Suc k) A
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have not_zero_i_k: "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using all_zero_below_greatest greatest_less_zero_row[OF r _ not_all_zero] not_zero_i
[PROOF STATE]
proof (prove)
using this:
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
is_zero_row_upt_k ?i k A \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k i (Suc k) A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have not_zero_suc_i: "\<not> is_zero_row_upt_k (i+1) k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) k A
[PROOF STEP]
using all_zero_below_greatest greatest_less_zero_row[OF r _ not_all_zero] not_zero_suc_i
[PROOF STATE]
proof (prove)
using this:
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
is_zero_row_upt_k ?i k A \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) k A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (i + (1::'m)) k A

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have aux:"(\<forall>i j. i + 1 = j \<and> i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ j $ n \<noteq> 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i + (1::'m) = j \<and> i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<forall>i j. i + (1::'m) = j \<and> i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i j. i + (1::'m) = j \<and> i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>i j. i + (1::'m) = j \<and> i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'m); \<not> is_zero_row_upt_k i (Suc k) A; \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show "(LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
[PROOF STEP]
using aux not_zero_i_k not_zero_suc_i i
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i + (1::'m) = j \<and> i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i k A
\<not> is_zero_row_upt_k (i + (1::'m)) k A
i < i + (1::'m)

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
assume "\<not> is_zero_row_upt_k i (Suc k) A" and "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i (Suc k) A
i \<noteq> j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) A; i \<noteq> j\<rbrakk> \<Longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
thus "A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i (Suc k) A
i \<noteq> j

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using all_zero_below_greatest greatest_less_zero_row not_all_zero r rref_upt_condition4
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i (Suc k) A
i \<noteq> j
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
\<lbrakk>reduced_row_echelon_form_upt_k ?A ?k; is_zero_row_upt_k ?i ?k ?A; \<not> (\<forall>a. is_zero_row_upt_k a ?k ?A)\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m ?k ?A) < ?i
\<not> (\<forall>a. is_zero_row_upt_k a k A)
reduced_row_echelon_form_upt_k A k
reduced_row_echelon_form_upt_k ?A ?k \<Longrightarrow> \<forall>i. \<not> is_zero_row_upt_k i ?k ?A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> ?A $ j $ (LEAST n. ?A $ i $ n \<noteq> (0::?'a)) = (0::?'a))

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rref_suc_if_all_rows_not_zero:
  fixes A::"'a::{one, zero}^'n::{mod_type}^'m::{finite,one,plus,linorder}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and all_not_zero: "\<forall>n. \<not> is_zero_row_upt_k n k A"
  shows "reduced_row_echelon_form_upt_k A (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A (Suc k)
[PROOF STEP]
proof (rule rref_suc_if_zero_below_greatest)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. reduced_row_echelon_form_upt_k A k
 2. \<not> (\<forall>a. is_zero_row_upt_k a k A)
 3. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A k

goal (2 subgoals):
 1. \<not> (\<forall>a. is_zero_row_upt_k a k A)
 2. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "\<not> (\<forall>a. is_zero_row_upt_k a k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a k A)
[PROOF STEP]
using all_not_zero
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> is_zero_row_upt_k n k A

goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a k A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a. is_zero_row_upt_k a k A)

goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
using all_not_zero not_greater_Greatest
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> is_zero_row_upt_k n k A
(GREATEST x. ?P x) < ?k \<Longrightarrow> \<not> ?P ?k

goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greatest_ge_nonzero_row:
  fixes A::"'a::{zero}^'n::{mod_type}^'m::{finite,linorder}"
  assumes "\<not> is_zero_row_upt_k i k A"
  shows "i \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)
[PROOF STEP]
using Greatest_ge[of "(\<lambda>m. \<not> is_zero_row_upt_k m k A)", OF assms]
[PROOF STATE]
proof (prove)
using this:
i \<le> (GREATEST x. \<not> is_zero_row_upt_k x k A)

goal (1 subgoal):
 1. i \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)
[PROOF STEP]
.


[STATEMENT]
lemma greatest_ge_nonzero_row':
  fixes A::"'a::{zero, one}^'n::{mod_type}^'m::{finite, linorder, one, plus}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and i: "i \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)"
  and not_all_zero: "\<not> (\<forall>a. is_zero_row_upt_k a k A)"
  shows "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using greatest_less_zero_row[OF r] i not_all_zero
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_zero_row_upt_k ?i k A; \<not> (\<forall>a. is_zero_row_upt_k a k A)\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
i \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)
\<not> (\<forall>a. is_zero_row_upt_k a k A)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Gauss_Jordan_in_ij_1:
  fixes A::"'a::{field}^'m^'n::{finite, ord, wellorder}"
  assumes ex: "\<exists>n. A $ n $ j \<noteq> 0 \<and> i \<le> n"
  shows "(Gauss_Jordan_in_ij A i j) $ i $ j = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A i j $ i $ j = (1::'a)
[PROOF STEP]
proof (unfold Gauss_Jordan_in_ij_def Let_def mult_row_def interchange_rows_def, vector)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j \<noteq> (0::'a)
[PROOF STEP]
obtain n where Anj: "A $ n $ j \<noteq> 0 \<and> i \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
\<exists>n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n

goal (1 subgoal):
 1. (\<And>n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ n $ j \<noteq> (0::'a) \<and> i \<le> n

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j \<noteq> (0::'a)
[PROOF STEP]
show "A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j \<noteq> (0::'a)
[PROOF STEP]
using LeastI[of "\<lambda>n. A $ n $ j \<noteq> 0 \<and> i \<le> n" n, OF Anj]
[PROOF STATE]
proof (prove)
using this:
A $ (LEAST x. A $ x $ j \<noteq> (0::'a) \<and> i \<le> x) $ j \<noteq> (0::'a) \<and> i \<le> (LEAST x. A $ x $ j \<noteq> (0::'a) \<and> i \<le> x)

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gauss_Jordan_in_ij_0:
  fixes A::"'a::{field}^'m^'n::{finite, ord, wellorder}"
  assumes ex: "\<exists>n. A $ n $ j \<noteq> 0 \<and> i \<le> n" and a: "a \<noteq> i"
  shows "(Gauss_Jordan_in_ij A i j) $ a $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A i j $ a $ j = (0::'a)
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
\<exists>n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A i j $ a $ j = (0::'a)
[PROOF STEP]
apply (rule Gauss_Jordan_in_ij_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A i j $ a $ j = (0::'a)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<noteq> i

goal (1 subgoal):
 1. \<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A i j $ a $ j = (0::'a)
[PROOF STEP]
by (simp add: mult_row_def interchange_rows_def row_add_def)


[STATEMENT]
lemma Gauss_Jordan_in_ij_preserves_previous_elements:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and not_zero_a: "\<not> is_zero_row_upt_k a k A"
  and exists_m: "\<exists>m. A $ m $ (from_nat k) \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> m"
  and Greatest_plus_1: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<noteq> 0"
  and j_le_k: "to_nat j < k"
  shows "Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) (from_nat k) $ i $ j = A $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = A $ i $ j
[PROOF STEP]
proof (unfold Gauss_Jordan_in_ij_def Let_def interchange_rows_def mult_row_def row_add_def, auto)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j / A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 3. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
define last_nonzero_row where "last_nonzero_row = (GREATEST m. \<not> is_zero_row_upt_k m k A)"
[PROOF STATE]
proof (state)
this:
last_nonzero_row = (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (4 subgoals):
 1. \<lbrakk>i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j / A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 3. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
have "last_nonzero_row < (last_nonzero_row + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last_nonzero_row < last_nonzero_row + (1::'rows)
[PROOF STEP]
by (rule  Suc_le'[of last_nonzero_row], auto simp add: last_nonzero_row_def Greatest_plus_1)
[PROOF STATE]
proof (state)
this:
last_nonzero_row < last_nonzero_row + (1::'rows)

goal (4 subgoals):
 1. \<lbrakk>i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j / A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 3. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
hence zero_row: "is_zero_row_upt_k (last_nonzero_row + 1) k A"
[PROOF STATE]
proof (prove)
using this:
last_nonzero_row < last_nonzero_row + (1::'rows)

goal (1 subgoal):
 1. is_zero_row_upt_k (last_nonzero_row + (1::'rows)) k A
[PROOF STEP]
using not_le greatest_ge_nonzero_row last_nonzero_row_def
[PROOF STATE]
proof (prove)
using this:
last_nonzero_row < last_nonzero_row + (1::'rows)
(\<not> ?x \<le> ?y) = (?y < ?x)
\<not> is_zero_row_upt_k ?i ?k ?A \<Longrightarrow> ?i \<le> (GREATEST m. \<not> is_zero_row_upt_k m ?k ?A)
last_nonzero_row = (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (1 subgoal):
 1. is_zero_row_upt_k (last_nonzero_row + (1::'rows)) k A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (last_nonzero_row + (1::'rows)) k A

goal (4 subgoals):
 1. \<lbrakk>i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j / A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 3. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
hence A_greatest_0: "A $ (last_nonzero_row + 1) $ j = 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (last_nonzero_row + (1::'rows)) k A

goal (1 subgoal):
 1. A $ (last_nonzero_row + (1::'rows)) $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def last_nonzero_row_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ ((GREATEST m. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ m $ j = (0::'a))) + (1::'rows)) $ j = (0::'a)

goal (1 subgoal):
 1. A $ ((GREATEST m. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ m $ j = (0::'a))) + (1::'rows)) $ j = (0::'a)
[PROOF STEP]
using j_le_k
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ ((GREATEST m. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ m $ j = (0::'a))) + (1::'rows)) $ j = (0::'a)
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ ((GREATEST m. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ m $ j = (0::'a))) + (1::'rows)) $ j = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $ (last_nonzero_row + (1::'rows)) $ j = (0::'a)

goal (4 subgoals):
 1. \<lbrakk>i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j / A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 3. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A $ (last_nonzero_row + (1::'rows)) $ j = (0::'a)
[PROOF STEP]
show "A $ (last_nonzero_row + 1) $ j / A $ (last_nonzero_row + 1) $ from_nat k = A $ (last_nonzero_row + 1) $ j"
[PROOF STATE]
proof (prove)
using this:
A $ (last_nonzero_row + (1::'rows)) $ j = (0::'a)

goal (1 subgoal):
 1. A $ (last_nonzero_row + (1::'rows)) $ j / A $ (last_nonzero_row + (1::'rows)) $ mod_type_class.from_nat k = A $ (last_nonzero_row + (1::'rows)) $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ (last_nonzero_row + (1::'rows)) $ j / A $ (last_nonzero_row + (1::'rows)) $ mod_type_class.from_nat k = A $ (last_nonzero_row + (1::'rows)) $ j

goal (3 subgoals):
 1. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 2. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
 3. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
show zero: "A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n) $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
define least_n where "least_n = (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n)"
[PROOF STATE]
proof (state)
this:
least_n = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n)

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
have "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n
[PROOF STEP]
by (metis exists_m)
[PROOF STATE]
proof (state)
this:
\<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n
[PROOF STEP]
obtain n where n1: "A $ n $ from_nat k \<noteq> 0"  and n2: "(GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>A $ n $ mod_type_class.from_nat k \<noteq> (0::'a); (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ n $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
have "(GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> least_n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> least_n
[PROOF STEP]
by (metis (lifting, full_types) LeastI_ex least_n_def n1 n2)
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> least_n

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
hence "is_zero_row_upt_k least_n k A"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> least_n

goal (1 subgoal):
 1. is_zero_row_upt_k least_n k A
[PROOF STEP]
using last_nonzero_row_def less_le rref_upt_condition1[OF r] zero_row
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> least_n
last_nonzero_row = (GREATEST m. \<not> is_zero_row_upt_k m k A)
(?x < ?y) = (?x \<le> ?y \<and> ?x \<noteq> ?y)
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
is_zero_row_upt_k (last_nonzero_row + (1::'rows)) k A

goal (1 subgoal):
 1. is_zero_row_upt_k least_n k A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k least_n k A

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
thus "A $ least_n $ j = 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k least_n k A

goal (1 subgoal):
 1. A $ least_n $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ least_n $ j = (0::'a)

goal (1 subgoal):
 1. A $ least_n $ j = (0::'a)
[PROOF STEP]
using j_le_k
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ least_n $ j = (0::'a)
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ least_n $ j = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ least_n $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j = (0::'a)

goal (2 subgoals):
 1. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) \<noteq> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
 2. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
[PROOF STEP]
show "A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) $ j -
    A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) $ from_nat k *
    A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n) $ j /
    A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n) $ from_nat k =
    A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
[PROOF STEP]
unfolding last_nonzero_row_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (last_nonzero_row + (1::'rows)) $ j - A $ (last_nonzero_row + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> last_nonzero_row + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> last_nonzero_row + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> last_nonzero_row + (1::'rows) \<le> n) $ j
[PROOF STEP]
unfolding A_greatest_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) - A $ (last_nonzero_row + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> last_nonzero_row + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> last_nonzero_row + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> last_nonzero_row + (1::'rows) \<le> n) $ j
[PROOF STEP]
unfolding last_nonzero_row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j
[PROOF STEP]
unfolding zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * (0::'a) / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j - A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j

goal (1 subgoal):
 1. \<lbrakk>(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n); i = (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
[PROOF STEP]
show "A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n) $ j /
    A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<le> n) $ from_nat k =
    A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
[PROOF STEP]
unfolding zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
[PROOF STEP]
using A_greatest_0
[PROOF STATE]
proof (prove)
using this:
A $ (last_nonzero_row + (1::'rows)) $ j = (0::'a)

goal (1 subgoal):
 1. (0::'a) / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
[PROOF STEP]
unfolding last_nonzero_row_def
[PROOF STATE]
proof (prove)
using this:
A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j = (0::'a)

goal (1 subgoal):
 1. (0::'a) / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> n) $ mod_type_class.from_nat k = A $ ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) $ j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gauss_Jordan_in_ij_preserves_previous_elements':
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}"
  assumes all_zero: "\<forall>n. is_zero_row_upt_k n k A"
  and j_le_k: "to_nat j < k"
  and A_nk_not_zero: "A $ n $ (from_nat k) \<noteq> 0"
  shows "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ j = A $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ j = A $ i $ j
[PROOF STEP]
proof (unfold Gauss_Jordan_in_ij_def Let_def mult_row_def interchange_rows_def row_add_def, auto)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>i = (0::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (0::'rows) $ j / A $ (0::'rows) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows)\<rbrakk> \<Longrightarrow> A $ (0::'rows) $ j - A $ (0::'rows) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j
 3. \<lbrakk>(LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows); i = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); i \<noteq> (0::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
have A_0_j: "A $ 0 $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
using all_zero is_zero_row_upt_k_def j_le_k
[PROOF STATE]
proof (prove)
using this:
\<forall>n. is_zero_row_upt_k n k A
is_zero_row_upt_k ?i ?k ?A = (\<forall>j. mod_type_class.to_nat j < ?k \<longrightarrow> ?A $ ?i $ j = (0::?'a))
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ j = (0::'a)

goal (4 subgoals):
 1. \<lbrakk>i = (0::'rows); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (0::'rows) $ j / A $ (0::'rows) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
 2. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows)\<rbrakk> \<Longrightarrow> A $ (0::'rows) $ j - A $ (0::'rows) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j
 3. \<lbrakk>(LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows); i = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
 4. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); i \<noteq> (0::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
show "A $ 0 $ j / A $ 0 $ from_nat k = A $ 0 $ j"
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ j = (0::'a)

goal (1 subgoal):
 1. A $ (0::'rows) $ j / A $ (0::'rows) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ j / A $ (0::'rows) $ mod_type_class.from_nat k = A $ (0::'rows) $ j

goal (3 subgoals):
 1. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows)\<rbrakk> \<Longrightarrow> A $ (0::'rows) $ j - A $ (0::'rows) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j
 2. \<lbrakk>(LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows); i = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
 3. \<lbrakk>i \<noteq> (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); i \<noteq> (0::'rows); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
show A_least_j: "A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n) $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
using all_zero is_zero_row_upt_k_def j_le_k
[PROOF STATE]
proof (prove)
using this:
\<forall>n. is_zero_row_upt_k n k A
is_zero_row_upt_k ?i ?k ?A = (\<forall>j. mod_type_class.to_nat j < ?k \<longrightarrow> ?A $ ?i $ j = (0::?'a))
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j = (0::'a)

goal (2 subgoals):
 1. \<lbrakk>i = (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n); (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows)\<rbrakk> \<Longrightarrow> A $ (0::'rows) $ j - A $ (0::'rows) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j
 2. \<lbrakk>(LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows); i = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
[PROOF STEP]
show "A $ 0 $ j -
    A $ 0 $ from_nat k * A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n) $ j /
    A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n) $ from_nat k =
    A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (0::'rows) $ j - A $ (0::'rows) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j
[PROOF STEP]
unfolding A_0_j A_least_j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) - A $ (0::'rows) $ mod_type_class.from_nat k * (0::'a) / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ j - A $ (0::'rows) $ mod_type_class.from_nat k * A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j

goal (1 subgoal):
 1. \<lbrakk>(LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) \<noteq> (0::'rows); i = (0::'rows)\<rbrakk> \<Longrightarrow> A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
[PROOF STEP]
show "A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n) $ j / A $ (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n) $ from_nat k = A $ 0 $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j
[PROOF STEP]
unfolding A_least_j A_0_j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ j / A $ (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n) $ mod_type_class.from_nat k = A $ (0::'rows) $ j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_zero_after_Gauss:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  assumes zero_a: "is_zero_row_upt_k a k A"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and r: "reduced_row_echelon_form_upt_k A k"
  and greatest_less_ma: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> ma"
  and A_ma_k_not_zero: "A $ ma $ from_nat k \<noteq> 0"
  shows "is_zero_row_upt_k a k (Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k a k (Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k))
[PROOF STEP]
proof (subst is_zero_row_upt_k_def, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
fix j::'n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
assume j_less_k: "to_nat j < k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
have not_zero_g: "(GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) \<noteq> (0::'m)
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m) \<Longrightarrow> False
[PROOF STEP]
assume "(GREATEST m. \<not> is_zero_row_upt_k m k A) + 1 = 0"
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m)

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m) \<Longrightarrow> False
[PROOF STEP]
hence "(GREATEST m. \<not> is_zero_row_upt_k m k A) = -1"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m)

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) = - (1::'m)
[PROOF STEP]
using a_eq_minus_1
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m)
\<forall>a. a + (1::?'a) = (0::?'a) \<longrightarrow> a = - (1::?'a)

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) = - (1::'m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) = - (1::'m)

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m) \<Longrightarrow> False
[PROOF STEP]
hence "a\<le>(GREATEST m. \<not> is_zero_row_upt_k m k A)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) = - (1::'m)

goal (1 subgoal):
 1. a \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)
[PROOF STEP]
using Greatest_is_minus_1
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) = - (1::'m)
\<forall>a. a \<le> - (1::?'a)

goal (1 subgoal):
 1. a \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m) \<Longrightarrow> False
[PROOF STEP]
hence "\<not> is_zero_row_upt_k a k A"
[PROOF STATE]
proof (prove)
using this:
a \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k a k A
[PROOF STEP]
using greatest_less_zero_row[OF r] not_zero_m
[PROOF STATE]
proof (prove)
using this:
a \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A)
\<lbrakk>is_zero_row_upt_k ?i k A; \<not> (\<forall>a. is_zero_row_upt_k a k A)\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k a k A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k a k A

goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) = (0::'m) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k a k A

goal (1 subgoal):
 1. False
[PROOF STEP]
using zero_a
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k a k A
is_zero_row_upt_k a k A

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m) \<noteq> (0::'m)

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
have "Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) (from_nat k) $ a $ j = A $ a $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = A $ a $ j
[PROOF STEP]
by (rule Gauss_Jordan_in_ij_preserves_previous_elements[OF r not_zero_m _ not_zero_g j_less_k], auto intro!: A_ma_k_not_zero greatest_less_ma)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = A $ a $ j

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = A $ a $ j

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ a $ j = (0::'a)
[PROOF STEP]
using zero_a j_less_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k a k A
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ a $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ a $ j = (0::'a)
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ a $ j = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ a $ j = (0::'a)

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + 1) (from_nat k) $ a $ j = 0"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'m)) (mod_type_class.from_nat k) $ a $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_zero_imp_Gauss_Jordan_column_not_zero_in_row_0:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia\<equiv>(if \<forall>m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
  defines B:"B\<equiv>(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes all_zero: "\<forall>n. is_zero_row_upt_k n k A"
  and not_zero_i: "\<not> is_zero_row_upt_k i (Suc k) B"
  and Amk_zero: "A $ m $ from_nat k \<noteq> 0"
  shows "i=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = (0::'rows)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
assume i_not_0: "i \<noteq> 0"
[PROOF STATE]
proof (state)
this:
i \<noteq> (0::'rows)

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
have ia2: "ia = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = 0
[PROOF STEP]
using ia all_zero
[PROOF STATE]
proof (prove)
using this:
ia \<equiv> if \<forall>m. is_zero_row_upt_k m k A then 0 else mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
\<forall>n. is_zero_row_upt_k n k A

goal (1 subgoal):
 1. ia = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ia = 0

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
have B_eq_Gauss: "B = Gauss_Jordan_in_ij A 0 (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> 0 = nrows A then (0, A) else (0 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
using all_zero Amk_zero least_mod_type
[PROOF STATE]
proof (prove)
using this:
\<forall>n. is_zero_row_upt_k n k A
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> 0 = nrows A then (0, A) else (0 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding from_nat_0 nrows_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. is_zero_row_upt_k n k A
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> 0 = CARD('rows) then (0, A) else (0 + 1, Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
have "...$ i $ (from_nat k) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n
 2. i \<noteq> (0::'rows)
[PROOF STEP]
show "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> 0 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n
[PROOF STEP]
using Amk_zero least_mod_type
[PROOF STATE]
proof (prove)
using this:
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n

goal (1 subgoal):
 1. i \<noteq> (0::'rows)
[PROOF STEP]
show "i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> (0::'rows)
[PROOF STEP]
using i_not_0
[PROOF STATE]
proof (prove)
using this:
i \<noteq> (0::'rows)

goal (1 subgoal):
 1. i \<noteq> (0::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i \<noteq> (0::'rows)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
have "B $ i $ from_nat k = 0"
[PROOF STATE]
proof (prove)
using this:
B $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. B $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
B $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
hence "is_zero_row_upt_k i (Suc k) B"
[PROOF STATE]
proof (prove)
using this:
B $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) B
[PROOF STEP]
unfolding B_eq_Gauss
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero _ Amk_zero]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)
mod_type_class.to_nat ?j < k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j

goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
by (metis all_zero is_zero_row_upt_k_def less_SucE to_nat_from_nat)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. i \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. False
[PROOF STEP]
using not_zero_i
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) B
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_1_part_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes zero_column_k: "\<forall>m\<ge>from_nat 0. A $ m $ from_nat k = 0"
  and all_zero: "\<forall>m. is_zero_row_upt_k m k A"
  shows "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ja. mod_type_class.to_nat ja < Suc k \<longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
fix ja::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
assume ja_less_suc_k: "to_nat ja < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ja < Suc k

goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
show "A $ j $ ja = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
proof (cases "to_nat ja < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ja < k

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ja < k

goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
using all_zero
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ja < k
\<forall>m. is_zero_row_upt_k m k A

goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ja < k
\<forall>m j. mod_type_class.to_nat j < k \<longrightarrow> A $ m $ j = (0::'a)

goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ j $ ja = (0::'a)

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat ja < k

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
hence ja_eq_k: "k = to_nat ja "
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat ja < k

goal (1 subgoal):
 1. k = mod_type_class.to_nat ja
[PROOF STEP]
using ja_less_suc_k
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat ja < k
mod_type_class.to_nat ja < Suc k

goal (1 subgoal):
 1. k = mod_type_class.to_nat ja
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = mod_type_class.to_nat ja

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
using zero_column_k
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
unfolding ja_eq_k from_nat_to_nat_id from_nat_0
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>0::'rows. A $ m $ ja = (0::'a)

goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
using least_mod_type
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>0::'rows. A $ m $ ja = (0::'a)
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ j $ ja = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $ j $ ja = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed