[STATEMENT]
lemma condition_4_part_5:
  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_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"
  shows "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ j $
  (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) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
have B_eq_Gauss: "B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding B Gauss_Jordan_column_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let i = fst (ia, A); A = snd (ia, A); from_nat_i = mod_type_class.from_nat i; from_nat_k = mod_type_class.from_nat k in if (\<forall>m\<ge>from_nat_i. A $ m $ from_nat_k = (0::'a)) \<or> i = nrows A then (i, A) else (i + 1, Gauss_Jordan_in_ij A from_nat_i from_nat_k)) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding ia2 Let_def fst_conv snd_conv
[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))) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
using greatest_not_card greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
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. 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))) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
by (auto simp add: from_nat_to_nat_greatest)
[PROOF STATE]
proof (state)
this:
B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
have suc_greatest_not_zero: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
using Suc_eq_plus1 suc_not_zero greatest_not_card
[PROOF STATE]
proof (prove)
using this:
Suc ?n = ?n + 1
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A

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

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
proof (cases "is_zero_row_upt_k i k A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k A

goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have zero_i_k_B: "is_zero_row_upt_k i k B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k B
[PROOF STEP]
unfolding B_eq_Gauss
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
by (rule is_zero_after_Gauss[OF True not_zero_m rref greatest_less_ma A_ma_k_not_zero])
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k B

goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
hence Gauss_Jordan_i_not_0: "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i) $ (from_nat k) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k B

goal (1 subgoal):
 1. 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 $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k B
\<not> is_zero_row_upt_k i (Suc k) B

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

goal (1 subgoal):
 1. 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 $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using is_zero_row_upt_k_suc
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
\<not> is_zero_row_upt_k i (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
\<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

goal (1 subgoal):
 1. 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 $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
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 $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have i_eq_greatest: "i = ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
assume i_not_greatest: "i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (state)
this:
i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
have "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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 $ 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> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 2. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
show "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST n. \<not> is_zero_row_upt_k n 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 n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
using greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
(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. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'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> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
show "i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
using i_not_greatest
[PROOF STATE]
proof (prove)
using this:
i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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 $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
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 $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Gauss_Jordan_i_not_0
[PROOF STATE]
proof (prove)
using this:
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 $ mod_type_class.from_nat k = (0::'a)
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 $ mod_type_class.from_nat k \<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:
i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have Gauss_Jordan_i_1: "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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 $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
unfolding i_eq_greatest
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_1 greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n \<Longrightarrow> Gauss_Jordan_in_ij ?A ?i ?j $ ?i $ ?j = (1::?'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. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
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 $ mod_type_class.from_nat k = (1::'a)

goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have Least_eq_k: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0) = from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. 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 $ ka \<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 ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'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 ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'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 ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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 $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_i_not_0
[PROOF STATE]
proof (prove)
using this:
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 $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. 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 $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
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 $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. 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 $ 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 ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'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_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
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 $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. 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 $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
thus "from_nat k \<le> y"
[PROOF STATE]
proof (prove)
using this:
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 $ y \<noteq> (0::'a)

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

goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> y
[PROOF STEP]
unfolding i_eq_greatest B_eq_Gauss
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) $ y \<noteq> (0::'a)
is_zero_row_upt_k ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) k (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> y
[PROOF STEP]
by (metis is_zero_row_upt_k_def not_less to_nat_le)
[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 ka. 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 $ ka \<noteq> (0::'a)) = mod_type_class.from_nat k

goal (2 subgoals):
 1. is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
 2. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
using A_ma_k_not_zero Gauss_Jordan_in_ij_0' Least_eq_k greatest_less_ma i_eq_greatest i_not_j
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
\<exists>n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n \<Longrightarrow> \<forall>a. a \<noteq> ?i \<longrightarrow> Gauss_Jordan_in_ij ?A ?i ?j $ a $ ?j = (0::?'a)
(LEAST ka. 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 $ ka \<noteq> (0::'a)) = mod_type_class.from_nat k
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
i \<noteq> j

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
obtain n where Ain_not_0: "A $ i $ n \<noteq> 0" and j_le_k: "to_nat n < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>A $ i $ n \<noteq> (0::'a); mod_type_class.to_nat n < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>A $ i $ n \<noteq> (0::'a); mod_type_class.to_nat n < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a))

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>A $ i $ n \<noteq> (0::'a); mod_type_class.to_nat n < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $ i $ n \<noteq> (0::'a)
mod_type_class.to_nat n < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have least_le_k: "to_nat (LEAST ka. A $ i $ ka \<noteq> 0) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
[PROOF STEP]
by (metis (lifting, mono_tags) Ain_not_0 neq_iff j_le_k less_trans not_less_Least to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have Least_eq: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0)
      = (LEAST ka. A $ i $ ka \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. 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 $ ka \<noteq> (0::'a)) = (LEAST ka. A $ i $ ka \<noteq> (0::'a))
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
 2. \<And>y. 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 $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> 0) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref False _ suc_greatest_not_zero least_le_k]
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))

goal (1 subgoal):
 1. 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'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. 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref] False
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'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)
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. 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 $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. 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 $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
assume Gauss_Jordan_y:"Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
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 $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. 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 $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "(LEAST ka. A $ i $ ka \<noteq> 0) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
proof (cases "to_nat y < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat y < k

goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by (metis (mono_tags) False least_le_k less_trans not_le_imp_less to_nat_from_nat to_nat_le)
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat y < k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
have "A $ i $ y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_y
[PROOF STATE]
proof (prove)
using this:
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 $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ suc_greatest_not_zero True]
[PROOF STATE]
proof (prove)
using this:
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 $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ y = A $ ?i $ y

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
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 $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ y = A $ ?i $ y
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

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

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by (rule Least_le)
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. 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 $ ka \<noteq> (0::'a)) = (LEAST ka. A $ i $ ka \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
have Gauss_Jordan_eq_A: "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> 0) =
      A $ j $ (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ suc_greatest_not_zero least_le_k]
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> 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 $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

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

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k 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) $ j $ (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)) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
unfolding Least_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using rref_upt_condition4[OF rref]
[PROOF STATE]
proof (prove)
using this:
\<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. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using False Gauss_Jordan_eq_A i_not_j
[PROOF STATE]
proof (prove)
using this:
\<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))
\<not> is_zero_row_upt_k i k A
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a))
i \<noteq> j

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_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"
  shows "B $ j $ (LEAST n. B $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> 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)
 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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> 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)
 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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
show "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]
using condition_4_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> 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 all_zero_k not_zero_i_suc_k least_mod_type
[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> A $ ?j $ (LEAST n. A $ ?i $ n \<noteq> (0::'a)) = (0::'a)
\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)
\<not> is_zero_row_upt_k i (Suc k) B
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ ?j $ (LEAST n. A $ ?i $ n \<noteq> (0::'a)) = (0::'a)
\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (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))
(0::?'a) \<le> ?n

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 (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> 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)
 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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> 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)
 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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> 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)
 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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
assume all_zero: "\<forall>m. is_zero_row_upt_k m k A"
    and Amk_not_zero: "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> 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)
 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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
show "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]
using condition_4_part_2[OF _ i_not_j all_zero Amk_not_zero]
[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> 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 (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]
using  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> 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)
\<not> is_zero_row_upt_k i (Suc k) B

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 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> 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)
\<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. 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 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 (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
show "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]
using condition_4_part_3[OF rref _ i_not_j not_zero_m zero_below_greatest]
[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> 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
[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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'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]
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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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))

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
show "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]
using  condition_4_part_4[OF rref _ i_not_j not_zero_m greatest_eq_card]
[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> 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
[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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'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]
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> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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))

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ j $
    (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) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
using  condition_4_part_5[OF rref _ i_not_j not_zero_m greatest_not_card greatest_less_ma A_ma_k_not_zero]
[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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
using 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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[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> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (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))

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ (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)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduced_row_echelon_form_upt_k_Gauss_Jordan_column_k:
  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"
  shows "reduced_row_echelon_form_upt_k B (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k B (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) B; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) B
 2. \<And>i. \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> B $ i $ (LEAST k. B $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<And>i. \<lbrakk>i < i + (1::'rows); \<not> is_zero_row_upt_k i (Suc k) B; \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B\<rbrakk> \<Longrightarrow> (LEAST n. B $ i $ n \<noteq> (0::'a)) < (LEAST n. B $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) B; i \<noteq> j\<rbrakk> \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show "\<And>i j. is_zero_row_upt_k i (Suc k) B \<Longrightarrow> i < j \<Longrightarrow> is_zero_row_upt_k j (Suc k) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) B; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) B
[PROOF STEP]
using condition_1 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reduced_row_echelon_form_upt_k ?A ?k; 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)); ?i < ?j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?j (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))
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
B \<equiv> snd (Gauss_Jordan_column_k (ia, A) k)
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i (Suc k) B; i < j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_zero_row_upt_k ?i (Suc k) B; ?i < ?j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?j (Suc k) B

goal (3 subgoals):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> B $ i $ (LEAST k. B $ i $ k \<noteq> (0::'a)) = (1::'a)
 2. \<And>i. \<lbrakk>i < i + (1::'rows); \<not> is_zero_row_upt_k i (Suc k) B; \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B\<rbrakk> \<Longrightarrow> (LEAST n. B $ i $ n \<noteq> (0::'a)) < (LEAST n. B $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) B; i \<noteq> j\<rbrakk> \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show "\<And>i. \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> B $ i $ (LEAST k. B $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> B $ i $ (LEAST k. B $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using condition_2 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reduced_row_echelon_form_upt_k ?A ?k; \<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))\<rbrakk> \<Longrightarrow> 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) $ ?i $ (LEAST 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) $ ?i $ k \<noteq> (0::?'a)) = (1::?'a)
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
B \<equiv> snd (Gauss_Jordan_column_k (ia, A) k)
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<And>i. \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> B $ i $ (LEAST k. B $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k ?i (Suc k) B \<Longrightarrow> B $ ?i $ (LEAST k. B $ ?i $ k \<noteq> (0::'a)) = (1::'a)

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < i + (1::'rows); \<not> is_zero_row_upt_k i (Suc k) B; \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B\<rbrakk> \<Longrightarrow> (LEAST n. B $ i $ n \<noteq> (0::'a)) < (LEAST n. B $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) B; i \<noteq> j\<rbrakk> \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show "\<And>i. i < i + 1 \<Longrightarrow> \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> \<not> is_zero_row_upt_k (i + 1) (Suc k) B \<Longrightarrow> (LEAST n. B $ i $ n \<noteq> 0) < (LEAST n. B $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < i + (1::'rows); \<not> is_zero_row_upt_k i (Suc k) B; \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B\<rbrakk> \<Longrightarrow> (LEAST n. B $ i $ n \<noteq> (0::'a)) < (LEAST n. B $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using condition_3 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reduced_row_echelon_form_upt_k ?A ?k; ?i < ?i + (1::?'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)); \<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. 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) $ ?i $ n \<noteq> (0::?'a)) < (LEAST n. 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) $ (?i + (1::?'rows)) $ n \<noteq> (0::?'a))
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
B \<equiv> snd (Gauss_Jordan_column_k (ia, A) k)
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < i + (1::'rows); \<not> is_zero_row_upt_k i (Suc k) B; \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B\<rbrakk> \<Longrightarrow> (LEAST n. B $ i $ n \<noteq> (0::'a)) < (LEAST n. B $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < ?i + (1::'rows); \<not> is_zero_row_upt_k ?i (Suc k) B; \<not> is_zero_row_upt_k (?i + (1::'rows)) (Suc k) B\<rbrakk> \<Longrightarrow> (LEAST n. B $ ?i $ n \<noteq> (0::'a)) < (LEAST n. B $ (?i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) B; i \<noteq> j\<rbrakk> \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
show "\<And>i j. \<not> is_zero_row_upt_k i (Suc k) B \<Longrightarrow> i \<noteq> j \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) B; i \<noteq> j\<rbrakk> \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using condition_4 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reduced_row_echelon_form_upt_k ?A ?k; \<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)); ?i \<noteq> ?j\<rbrakk> \<Longrightarrow> 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) $ ?j $ (LEAST n. 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) $ ?i $ n \<noteq> (0::?'a)) = (0::?'a)
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
B \<equiv> snd (Gauss_Jordan_column_k (ia, A) k)
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<not> is_zero_row_upt_k i (Suc k) B; i \<noteq> j\<rbrakk> \<Longrightarrow> B $ j $ (LEAST n. B $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> is_zero_row_upt_k ?i (Suc k) B; ?i \<noteq> ?j\<rbrakk> \<Longrightarrow> B $ ?j $ (LEAST n. B $ ?i $ n \<noteq> (0::'a)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_Gauss_condition_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes "\<forall>m. is_zero_row_upt_k m k A"
  and "\<forall>m\<ge>0. A $ m $ from_nat k = 0"
  shows "is_zero_row_upt_k m (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k m (Suc k) A
[PROOF STEP]
by (rule is_zero_row_upt_k_suc, auto simp add: assms least_mod_type)


[STATEMENT]
lemma foldl_Gauss_condition_2:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes k: "k < ncols A"
  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 "\<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
have to_nat_from_nat_k_suc: "to_nat (from_nat k::'columns) < (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
using to_nat_from_nat_id[OF k[unfolded ncols_def]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat k) = k

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

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
have A0k_eq_1: "(Gauss_Jordan_in_ij A 0 (from_nat k)) $ 0 $ (from_nat k) = 1"
[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 = (1::'a)
[PROOF STEP]
by (rule Gauss_Jordan_in_ij_1, auto intro!: Amk_not_zero least_mod_type)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k = (1::'a)

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
have "\<not> is_zero_row_upt_k 0 (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ j = (0::'a))
[PROOF STEP]
using A0k_eq_1 to_nat_from_nat_k_suc
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k = (1::'a)
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

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

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

goal:
No subgoals!
[PROOF STEP]
qed