[STATEMENT]
lemma condition_3:
  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 rref: "reduced_row_echelon_form_upt_k A k"
  and i_le: "i < i + 1"
  and not_zero_i_suc_k: "\<not> is_zero_row_upt_k i (Suc k) B"
  and not_zero_suc_i_suc_k: "\<not> is_zero_row_upt_k (i + 1) (Suc k) B"
  shows "(LEAST n. B $ i $ n \<noteq> 0) < (LEAST n. B $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. B $ i $ n \<noteq> (0::'a)) < (LEAST n. B $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
proof (unfold B Gauss_Jordan_column_k_def ia Let_def fst_conv snd_conv, auto, unfold from_nat_to_nat_greatest from_nat_0)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; \<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; (0::'rows) \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 5. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
assume all_zero: "\<forall>m. is_zero_row_upt_k m k A"
    and all_zero_k: "\<forall>m\<ge>0. A $ m $ from_nat k = 0"
[PROOF STATE]
proof (state)
this:
\<forall>m. is_zero_row_upt_k m k A
\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)

goal (5 subgoals):
 1. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; \<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; (0::'rows) \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 5. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (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::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using condition_3_part_1[OF _ all_zero]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k ?i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ ?i $ n \<noteq> (0::'a)) < (LEAST n. A $ (?i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using all_zero_k least_mod_type not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k ?i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ ?i $ n \<noteq> (0::'a)) < (LEAST n. A $ (?i + (1::'rows)) $ n \<noteq> (0::'a))
\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)
(0::?'a) \<le> ?n
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k ?i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ ?i $ n \<noteq> (0::'a)) < (LEAST n. A $ (?i + (1::'rows)) $ n \<noteq> (0::'a))
\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)
(0::?'a) \<le> ?n
\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))

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

goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; (0::'rows) \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; (0::'rows) \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; (0::'rows) \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
assume all_zero: "\<forall>m. is_zero_row_upt_k m k A"
    and Amk_notzero: "A $ m $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<forall>m. is_zero_row_upt_k m k A
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; (0::'rows) \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
show "(LEAST n. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ n \<noteq> 0) < (LEAST n. Gauss_Jordan_in_ij A 0 (from_nat k) $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using condition_3_part_2[OF i_le _ _ all_zero Amk_notzero]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using not_zero_i_suc_k not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) B
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (3 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
assume not_zero_m: "\<not> is_zero_row_upt_k m k A"
    and zero_below_greatest: "\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A
\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)

goal (3 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; \<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (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::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using condition_3_part_3[OF rref i_le _ _ not_zero_m zero_below_greatest]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using not_zero_i_suc_k not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) B
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))

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

goal (2 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
assume not_zero_m: "\<not> is_zero_row_upt_k m k A"
    and greatest_eq_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A

goal (2 subgoals):
 1. \<And>m. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (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::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using condition_3_part_4[OF rref i_le _ _ not_zero_m greatest_eq_card]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using not_zero_i_suc_k not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) B
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))

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

goal (1 subgoal):
 1. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
fix m ma
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
assume not_zero_m: "\<not> is_zero_row_upt_k m k A"
    and greatest_not_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A"
    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"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>m ma. \<lbrakk>\<not> is_zero_row_upt_k m k A; Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A; (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma; A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
show "(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n \<noteq> 0)
    < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using condition_3_part_5[OF rref i_le _ _ not_zero_m greatest_not_card greatest_less_ma A_ma_k_not_zero]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using not_zero_i_suc_k not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) B
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)); \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))\<rbrakk> \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_4_part_1:
  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 not_zero_i_suc_k:  "\<not> is_zero_row_upt_k i (Suc k) B"
  and all_zero: "\<forall>m. is_zero_row_upt_k m k A"
  and all_zero_k: "\<forall>m. A $ m $ from_nat k = 0"
  shows "A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[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>m. is_zero_row_upt_k m k A

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

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have B_eq_A: "B=A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = A
[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))) = A
[PROOF STEP]
using all_zero_k
[PROOF STATE]
proof (prove)
using this:
\<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)

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))) = A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
B = A

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using B_eq_A all_zero all_zero_k is_zero_row_upt_k_suc not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
B = A
\<forall>m. is_zero_row_upt_k m k A
\<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)
\<lbrakk>is_zero_row_upt_k ?i ?k ?A; ?A $ ?i $ mod_type_class.from_nat ?k = (0::?'b)\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?i (Suc ?k) ?A
\<not> is_zero_row_upt_k i (Suc k) B

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 condition_4_part_2:
  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 not_zero_i_suc_k: "\<not> is_zero_row_upt_k i (Suc k) B"
  and i_not_j: "i \<noteq> j"
  and all_zero: "\<forall>m. is_zero_row_upt_k m k A"
  and Amk_not_zero: "A $ m $ from_nat k \<noteq> 0"
  shows "Gauss_Jordan_in_ij A 0 (from_nat k) $ j $ (LEAST n. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have i_eq_0: "i=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = (0::'rows)
[PROOF STEP]
using all_zero_imp_Gauss_Jordan_column_not_zero_in_row_0[OF all_zero _ Amk_not_zero] not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k ?i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)) \<Longrightarrow> ?i = (0::'rows)
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. i = (0::'rows)
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k ?i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k)) \<Longrightarrow> ?i = (0::'rows)
\<not> is_zero_row_upt_k i (Suc k) (snd (Gauss_Jordan_column_k (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, A) k))

goal (1 subgoal):
 1. i = (0::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i = (0::'rows)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have least_eq_k: "(LEAST n. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ n \<noteq> 0) = from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = mod_type_class.from_nat k
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ from_nat k \<noteq> 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 \<noteq> (0::'a)
[PROOF STEP]
unfolding i_eq_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using Amk_not_zero Gauss_Jordan_in_ij_1 least_mod_type zero_neq_one
[PROOF STATE]
proof (prove)
using this:
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
\<exists>n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n \<Longrightarrow> Gauss_Jordan_in_ij ?A ?i ?j $ ?i $ ?j = (1::?'a)
(0::?'a) \<le> ?n
(0::?'a) \<noteq> (1::?'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[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 \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
assume Gauss_Jordan_y_not_0: "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
show "from_nat k \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> y
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> mod_type_class.from_nat k \<le> y \<Longrightarrow> False
[PROOF STEP]
assume "\<not> from_nat k \<le> y"
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.from_nat k \<le> y

goal (1 subgoal):
 1. \<not> mod_type_class.from_nat k \<le> y \<Longrightarrow> False
[PROOF STEP]
hence "y < (from_nat k)"
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.from_nat k \<le> y

goal (1 subgoal):
 1. y < mod_type_class.from_nat k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y < mod_type_class.from_nat k

goal (1 subgoal):
 1. \<not> mod_type_class.from_nat k \<le> y \<Longrightarrow> False
[PROOF STEP]
hence to_nat_y_less_k: "to_nat y < k"
[PROOF STATE]
proof (prove)
using this:
y < mod_type_class.from_nat k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k
[PROOF STEP]
using to_nat_le
[PROOF STATE]
proof (prove)
using this:
y < mod_type_class.from_nat k
?y < mod_type_class.from_nat ?k \<Longrightarrow> mod_type_class.to_nat ?y < ?k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat y < k

goal (1 subgoal):
 1. \<not> mod_type_class.from_nat k \<le> y \<Longrightarrow> False
[PROOF STEP]
have "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y = (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero to_nat_y_less_k Amk_not_zero] all_zero to_nat_y_less_k
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y
\<forall>m. is_zero_row_upt_k m k A
mod_type_class.to_nat y < k

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

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y = (0::'a)

goal (1 subgoal):
 1. \<not> mod_type_class.from_nat k \<le> y \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Gauss_Jordan_y_not_0
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y = (0::'a)
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'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:
mod_type_class.from_nat k \<le> y

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

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ (LEAST n. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
unfolding least_eq_k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
apply (rule Gauss_Jordan_in_ij_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (0::'rows) \<le> n
 2. j \<noteq> (0::'rows)
[PROOF STEP]
using i_eq_0 i_not_j Amk_not_zero least_mod_type
[PROOF STATE]
proof (prove)
using this:
i = (0::'rows)
i \<noteq> j
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_4_part_3:
  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 rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_i_suc_k:  "\<not> is_zero_row_upt_k i (Suc k) B"
  and i_not_j: "i \<noteq> j"
  and not_zero_m: " \<not> is_zero_row_upt_k m k A"
  and zero_below_greatest: "\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
  shows "A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have ia2: "ia=to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
unfolding ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
using not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. (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) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have B_eq_A: "B=A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = A
[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 (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat k))) = A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>m\<ge>mod_type_class.from_nat (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A))). A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)) \<and> Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A \<longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)))) (mod_type_class.from_nat k) = A
[PROOF STEP]
unfolding from_nat_to_nat_greatest
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)) \<and> Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) = A
[PROOF STEP]
using zero_below_greatest
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. (\<exists>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)) \<and> Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) = A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B = A

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have rref_suc: "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[OF rref], auto intro!: not_zero_m)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. (GREATEST m. \<not> is_zero_row_upt_k m k A) < a \<Longrightarrow> is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. (GREATEST m. \<not> is_zero_row_upt_k m k A) < a \<Longrightarrow> is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
assume greatest_less_a: "(GREATEST m. \<not> is_zero_row_upt_k m k A) < a"
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < a

goal (1 subgoal):
 1. \<And>a. (GREATEST m. \<not> is_zero_row_upt_k m k A) < a \<Longrightarrow> is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "is_zero_row_upt_k a (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
proof (rule is_zero_row_upt_k_suc)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_zero_row_upt_k a k A
 2. A $ a $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
show "is_zero_row_upt_k a k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k a k A
[PROOF STEP]
using row_greater_greatest_is_zero[OF greatest_less_a]
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k a k A

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

goal (1 subgoal):
 1. A $ a $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
show "A $ a $ from_nat k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ a $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
using zero_below_greatest  le_Suc[OF greatest_less_a]
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> a

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k a (Suc k) A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A (Suc k)

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using rref_upt_condition4[OF rref_suc] not_zero_i_suc_k i_not_j
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
\<not> is_zero_row_upt_k i (Suc k) B
i \<noteq> j

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
unfolding B_eq_A
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
\<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]
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 condition_4_part_4:
  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 rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_i_suc_k:  "\<not> is_zero_row_upt_k i (Suc k) B"
  and i_not_j: "i \<noteq> j"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and greatest_eq_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A"
  shows "A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have ia2: "ia=to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
unfolding ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
using not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. (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) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have B_eq_A: "B=A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = A
[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 (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat k))) = A
[PROOF STEP]
unfolding from_nat_to_nat_greatest
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat k))) = A
[PROOF STEP]
using greatest_eq_card
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A

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

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have greatest_eq_minus_1: "(GREATEST n. \<not> is_zero_row_upt_k n k A) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)
[PROOF STEP]
using a_eq_minus_1 greatest_eq_card to_nat_plus_one_less_card
[PROOF STATE]
proof (prove)
using this:
\<forall>a. a + (1::?'a) = (0::?'a) \<longrightarrow> a = - (1::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A
\<forall>a. a + (1::?'a) \<noteq> (0::?'a) \<longrightarrow> mod_type_class.to_nat a + 1 < CARD(?'a)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a. a + (1::?'a) = (0::?'a) \<longrightarrow> a = - (1::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = CARD('rows)
\<forall>a. a + (1::?'a) \<noteq> (0::?'a) \<longrightarrow> mod_type_class.to_nat a + 1 < CARD(?'a)

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

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
have rref_suc: "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_all_rows_not_zero)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. reduced_row_echelon_form_upt_k A k
 2. \<forall>n. \<not> is_zero_row_upt_k n 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 rref
[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 (1 subgoal):
 1. \<forall>n. \<not> is_zero_row_upt_k n k A
[PROOF STEP]
show "\<forall>n. \<not> is_zero_row_upt_k n k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<not> is_zero_row_upt_k n k A
[PROOF STEP]
using Greatest_is_minus_1 greatest_eq_minus_1 greatest_ge_nonzero_row'[OF rref _] not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<forall>a. a \<le> - (1::?'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)
\<lbrakk>?i \<le> (GREATEST m. \<not> is_zero_row_upt_k m k A); \<not> (\<forall>a. is_zero_row_upt_k a k A)\<rbrakk> \<Longrightarrow> \<not> is_zero_row_upt_k ?i k A
\<not> is_zero_row_upt_k m k A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A (Suc k)

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using rref_upt_condition4[OF rref_suc]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc 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]
using not_zero_i_suc_k i_not_j
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
\<not> is_zero_row_upt_k i (Suc k) B
i \<noteq> j

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
unfolding B_eq_A i_not_j
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
\<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]
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