[STATEMENT]
lemma condition_2_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 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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ ka \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have ia2: "ia = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = 0
[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) = 0
[PROOF STEP]
using all_zero
[PROOF STATE]
proof (prove)
using this:
\<forall>m. 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) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ia = 0

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have B_eq: "B = Gauss_Jordan_in_ij A 0 (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding B Gauss_Jordan_column_k_def
[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 (0::'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 0. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> 0 = nrows A then (0, A) else (0 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
using Amk_not_zero least_mod_type
[PROOF STATE]
proof (prove)
using this:
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

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

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

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have i_eq_0: "i=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = (0::'rows)
[PROOF STEP]
using Amk_not_zero B_eq all_zero condition_1_part_2 from_nat_0 not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
B = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
\<forall>m. is_zero_row_upt_k m k A
\<lbrakk>?j \<noteq> (0::?'rows); \<forall>m. is_zero_row_upt_k m ?k ?A; ?A $ ?m $ mod_type_class.from_nat ?k \<noteq> (0::?'a)\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?j (Suc ?k) (Gauss_Jordan_in_ij ?A (mod_type_class.from_nat 0) (mod_type_class.from_nat ?k))
mod_type_class.from_nat 0 = (0::?'a)
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. i = (0::'rows)
[PROOF STEP]
by metis
[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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have Least_eq: "(LEAST ka. Gauss_Jordan_in_ij A 0 (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 (0::'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 (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]
have "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]
using Gauss_Jordan_in_ij_1 Amk_not_zero least_mod_type
[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)
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

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 blast
[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 (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]
thus "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ from_nat k \<noteq> 0"
[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)

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)
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)

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 simp
[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 not_zero_gauss: "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: "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 force
[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]
have "Gauss_Jordan_in_ij A 0 (from_nat k) $ 0 $ y = A $ 0 $ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ y = A $ (0::'rows) $ y
[PROOF STEP]
by (rule Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero to_nat_le[OF y] Amk_not_zero])
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ y = A $ (0::'rows) $ y

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

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

goal (1 subgoal):
 1. A $ (0::'rows) $ y = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<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. A $ (0::'rows) $ y = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ y = (0::'a)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) < i
[PROOF STEP]
using le_Suc' True
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> i
\<lbrakk>?a + (1::?'a) \<le> ?b; mod_type_class.to_nat ?a + 1 < CARD(?'a)\<rbrakk> \<Longrightarrow> ?a < ?b
mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows)

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

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

goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
using not_greater_Greatest
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < i
(GREATEST x. ?P x) < ?k \<Longrightarrow> \<not> ?P ?k

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

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

goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) A
[PROOF STEP]
proof (unfold is_zero_row_upt_k_def, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a); is_zero_row_upt_k i k A; mod_type_class.to_nat j < Suc k\<rbrakk> \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
fix j::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a); is_zero_row_upt_k i k A; mod_type_class.to_nat j < Suc k\<rbrakk> \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
assume "to_nat j < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < Suc k

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

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

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

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

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
by (metis from_nat_to_nat_id le_neq_implies_less not_le not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
A $ i $ j = (0::'a)

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

goal (1 subgoal):
 1. \<not> i < (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:
is_zero_row_upt_k i (Suc k) A

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> (GREATEST n. \<not> is_zero_row_upt_k n k A)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using greatest_ge_nonzero_row'[OF rref] not_zero_m
[PROOF STATE]
proof (prove)
using this:
i \<le> (GREATEST n. \<not> is_zero_row_upt_k n k A)
\<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. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

goal (2 subgoals):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows) \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 2. \<not> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows) \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k 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)

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows) \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows) \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows)

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

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < CARD('rows) \<Longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
proof (rule not_is_zero_row_upt_suc)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row_upt_k i (Suc k) A
 2. \<forall>i. A $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
show "\<not> is_zero_row_upt_k i (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i (Suc k) A
[PROOF STEP]
using not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i (Suc k) B

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

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

goal (1 subgoal):
 1. \<forall>i. A $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
show "\<forall>i. A $ i $ from_nat k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. A $ i $ mod_type_class.from_nat k = (0::'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. \<forall>i. A $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
unfolding greatest_plus_one_eq_0
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>0::'rows. A $ m $ mod_type_class.from_nat k = (0::'a)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

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

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k 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)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_2_part_4:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  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 $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_zero_row_upt_k i k A \<Longrightarrow> False
[PROOF STEP]
assume zero_i: "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k A

goal (1 subgoal):
 1. is_zero_row_upt_k i k A \<Longrightarrow> False
[PROOF STEP]
hence zero_minus_1: "is_zero_row_upt_k (-1) k A"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k A

goal (1 subgoal):
 1. is_zero_row_upt_k (- (1::'rows)) k A
[PROOF STEP]
using rref_upt_condition1[OF rref]
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k A
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)

goal (1 subgoal):
 1. is_zero_row_upt_k (- (1::'rows)) k A
[PROOF STEP]
using Greatest_is_minus_1 neq_le_trans
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k A
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
\<forall>a. a \<le> - (1::?'a)
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

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

goal (1 subgoal):
 1. is_zero_row_upt_k i k A \<Longrightarrow> False
[PROOF STEP]
have "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
using greatest_plus_one_eq_0[OF greatest_eq_card]
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)

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

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

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

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

goal (1 subgoal):
 1. is_zero_row_upt_k i k A \<Longrightarrow> False
[PROOF STEP]
have "\<not> is_zero_row_upt_k (GREATEST n. \<not> is_zero_row_upt_k n k A) k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (GREATEST n. \<not> is_zero_row_upt_k n k A) k A
[PROOF STEP]
by (rule greatest_ge_nonzero_row'[OF rref _ ], auto intro!: not_zero_m)
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (GREATEST n. \<not> is_zero_row_upt_k n k A) k A

goal (1 subgoal):
 1. is_zero_row_upt_k i k A \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k (GREATEST n. \<not> is_zero_row_upt_k n k A) k A

goal (1 subgoal):
 1. False
[PROOF STEP]
using zero_minus_1
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k (GREATEST n. \<not> is_zero_row_upt_k n k A) k A
is_zero_row_upt_k (- (1::'rows)) k A

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding greatest_eq_minus_1
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k (- (1::'rows)) k A
is_zero_row_upt_k (- (1::'rows)) k A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k 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)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ ka \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using condition_2_part_2[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> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ ka \<noteq> (0::'a)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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) $ ?i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ ka \<noteq> (0::'a)) = (1::'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) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'a)
[PROOF STEP]
show "A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using condition_2_part_3[OF rref _ not_zero_m zero_below_greatest] 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 $ ?i $ (LEAST k. A $ ?i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ ?i $ (LEAST k. A $ ?i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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 $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'a)
[PROOF STEP]
show "A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using condition_2_part_4[OF rref not_zero_m greatest_eq_card]
[PROOF STATE]
proof (prove)
using this:
A $ ?i $ (LEAST k. A $ ?i $ k \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'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) $ i $ (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)) = (1::'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) $ i $ (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)) = (1::'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) $ i $ (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)) = (1::'a)
[PROOF STEP]
assume not_zero_m: "\<not> is_zero_row_upt_k m k A"
    and greatest_noteq_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) $ i $ (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)) = (1::'a)
[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. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0) = 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 $ (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)) = (1::'a)
[PROOF STEP]
using condition_2_part_5[OF rref _ not_zero_m greatest_noteq_card greatest_less_ma A_ma_k_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> 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. 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)) = (1::'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) $ i $ (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)) = (1::'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) $ ?i $ (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)) = (1::'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) $ i $ (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)) = (1::'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 $ (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)) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
by (metis less_SucE to_nat_from_nat)
[PROOF STATE]
proof (state)
this:
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]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
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]
using not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) B
\<not> is_zero_row_upt_k i (Suc k) B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_3_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 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"
  and all_zero: "\<forall>m. is_zero_row_upt_k m k A"
  and Amk_notzero: "A $ m $ from_nat k \<noteq> 0"
  shows "(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]
proof -
[PROOF STATE]
proof (state)
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]
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. (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]
have B_eq_Gauss: "B = Gauss_Jordan_in_ij A 0 (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> 0 = nrows A then (0, A) else (0 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)
[PROOF STEP]
using all_zero Amk_notzero least_mod_type
[PROOF STATE]
proof (prove)
using this:
\<forall>m. is_zero_row_upt_k m k A
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)
(0::?'a) \<le> ?n

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

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

goal (1 subgoal):
 1. (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]
have "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_notzero] 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. (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]
moreover
[PROOF STATE]
proof (state)
this:
i = (0::'rows)

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]
have "i+1=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + (1::'rows) = (0::'rows)
[PROOF STEP]
using all_zero_imp_Gauss_Jordan_column_not_zero_in_row_0[OF all_zero _ Amk_notzero] not_zero_suc_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 + (1::'rows)) (Suc k) B

goal (1 subgoal):
 1. i + (1::'rows) = (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 + (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. i + (1::'rows) = (0::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i + (1::'rows) = (0::'rows)

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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i = (0::'rows)
i + (1::'rows) = (0::'rows)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = (0::'rows)
i + (1::'rows) = (0::'rows)

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 i_le
[PROOF STATE]
proof (prove)
using this:
i = (0::'rows)
i + (1::'rows) = (0::'rows)
i < i + (1::'rows)

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]
by auto
[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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_3_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 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"
  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 "(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]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. reduced_row_echelon_form_upt_k A k
 2. \<not> (\<forall>a. is_zero_row_upt_k a k A)
 3. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
using 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 (2 subgoals):
 1. \<not> (\<forall>a. is_zero_row_upt_k a k A)
 2. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "\<not> (\<forall>a. is_zero_row_upt_k a k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a k A)
[PROOF STEP]
using not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k m k A

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

goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
show "\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
proof (clarify)
[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::'rows
[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 greatest_less_a row_greater_greatest_is_zero
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) < a
(GREATEST m. \<not> is_zero_row_upt_k m ?k ?A) < ?i \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A

goal (1 subgoal):
 1. is_zero_row_upt_k a k A
[PROOF STEP]
by fast
[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  le_Suc[OF greatest_less_a] zero_below_greatest
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> 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 (1 subgoal):
 1. A $ a $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
by fast
[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:
\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A (Suc 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]
show ?thesis
[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 rref_upt_condition3[OF rref_suc] i_le not_zero_i_suc_k not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i (Suc k) A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
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

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_eq_A
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i (Suc k) A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
i < i + (1::'rows)
\<not> is_zero_row_upt_k i (Suc k) A
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) 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]
by blast
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_3_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 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"
  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 "(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]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (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. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[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 rref_upt_condition3[OF rref_suc] i_le not_zero_i_suc_k not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i (Suc k) A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
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

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_eq_A
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i (Suc k) A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
i < i + (1::'rows)
\<not> is_zero_row_upt_k i (Suc k) A
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) 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]
by blast
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed