[STATEMENT]
lemma condition_1_part_2:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes j_not_zero: "j \<noteq> 0"
  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 "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A (from_nat 0) (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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))
[PROOF STEP]
proof (unfold is_zero_row_upt_k_def, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
fix ja::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
assume ja_less_suc_k: "to_nat ja < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ja < Suc k

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

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
have "Gauss_Jordan_in_ij A (from_nat 0) (from_nat k) $ j $ ja = A $ j $ ja"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = A $ j $ ja
[PROOF STEP]
unfolding from_nat_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ j $ ja = A $ j $ ja
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero True Amk_not_zero]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ ja = A $ ?i $ ja

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

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = A $ j $ ja

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
using all_zero True
[PROOF STATE]
proof (prove)
using this:
\<forall>m. is_zero_row_upt_k m k A
mod_type_class.to_nat ja < k

goal (1 subgoal):
 1. A $ j $ ja = (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 ja < k

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A (from_nat 0) (from_nat k) $ j $ ja = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
unfolding k_eq_ja from_nat_to_nat_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) ja $ j $ ja = (0::'a)
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> mod_type_class.from_nat 0 \<le> n
 2. j \<noteq> mod_type_class.from_nat 0
[PROOF STEP]
show "\<exists>n. A $ n $ ja \<noteq> 0 \<and> from_nat 0 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> mod_type_class.from_nat 0 \<le> n
[PROOF STEP]
using least_mod_type Amk_not_zero
[PROOF STATE]
proof (prove)
using this:
(0::?'a) \<le> ?n
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> mod_type_class.from_nat 0 \<le> n
[PROOF STEP]
unfolding k_eq_ja from_nat_to_nat_id from_nat_0
[PROOF STATE]
proof (prove)
using this:
(0::?'a) \<le> ?n
A $ m $ ja \<noteq> (0::'a)

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

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

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat 0
[PROOF STEP]
unfolding from_nat_0
[PROOF STATE]
proof (prove)
using this:
j \<noteq> (0::'rows)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_1_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_less_j: "i<j"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and zero_below_greatest: "\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
  and zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B"
  shows "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
proof (unfold is_zero_row_upt_k_def, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
fix ja::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
assume ja_less_suc_k: "to_nat ja < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ja < Suc k

goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
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. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (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. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
have zero_ikA: "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
using zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) B

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

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

goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
hence zero_jkA: "is_zero_row_upt_k j 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 j k A
[PROOF STEP]
using rref_upt_condition1[OF rref] i_less_j
[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)
i < j

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> A $ j $ ja = (0::'a)
[PROOF STEP]
have "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> j
[PROOF STEP]
proof (rule le_Suc, rule GreatestI2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row_upt_k ?a2 k A
 2. \<And>x. \<not> is_zero_row_upt_k x k A \<Longrightarrow> x < j
[PROOF STEP]
show "\<not> is_zero_row_upt_k m k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k m 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> is_zero_row_upt_k m k A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. \<And>x. \<not> is_zero_row_upt_k x k A \<Longrightarrow> x < j
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<not> is_zero_row_upt_k x k A \<Longrightarrow> x < j
[PROOF STEP]
assume not_zero_xkA: "\<not> is_zero_row_upt_k x k A"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k x k A

goal (1 subgoal):
 1. \<And>x. \<not> is_zero_row_upt_k x k A \<Longrightarrow> x < j
[PROOF STEP]
show "x < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < j
[PROOF STEP]
using rref_upt_condition1[OF rref] not_zero_xkA zero_jkA neq_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
\<not> is_zero_row_upt_k x k A
is_zero_row_upt_k j k A
(?x \<noteq> ?y) = (?x < ?y \<or> ?y < ?x)

goal (1 subgoal):
 1. x < j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x < j

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_1_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 zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B"
  and i_less_j: "i<j"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and greatest_eq_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A"
  shows "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) 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. is_zero_row_upt_k j (Suc k) 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 nrows_def
[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
nrows ?A = CARD(?'rows)

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

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
have rref_Suc: "reduced_row_echelon_form_upt_k A (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A (Suc k)
[PROOF STEP]
proof (rule rref_suc_if_zero_below_greatest[OF rref])
[PROOF STATE]
proof (state)
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 "\<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
using greatest_eq_card not_less_eq to_nat_less_card to_nat_mono nrows_def
[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
(\<not> ?m < ?n) = (?n < Suc ?m)
mod_type_class.to_nat ?j < CARD(?'a)
?a < ?b \<Longrightarrow> mod_type_class.to_nat ?a < mod_type_class.to_nat ?b
nrows ?A = CARD(?'rows)

goal (1 subgoal):
 1. \<forall>a>GREATEST m. \<not> is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A
[PROOF STEP]
by metis
[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 (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a 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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A (Suc k)

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
using zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) B

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_1_part_5:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia\<equiv>(if \<forall>m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
  defines B:"B \<equiv>(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B"
  and i_less_j: "i<j"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and greatest_not_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A"
  and greatest_less_ma: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> ma"
  and A_ma_k_not_zero: "A $ ma $ from_nat k \<noteq> 0"
  shows "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
proof (subst (1) is_zero_row_upt_k_def, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
fix ja::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
assume ja_less_suc_k: "to_nat ja < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ja < Suc k

goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (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. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
have B_eq_Gauss_ij: "B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding B Gauss_Jordan_column_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let i = fst (ia, A); A = snd (ia, A); from_nat_i = mod_type_class.from_nat i; from_nat_k = mod_type_class.from_nat k in if (\<forall>m\<ge>from_nat_i. A $ m $ from_nat_k = (0::'a)) \<or> i = nrows A then (i, A) else (i + 1, Gauss_Jordan_in_ij A from_nat_i from_nat_k)) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding ia2 Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
using greatest_not_card greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

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

goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
have zero_ikA: "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
proof (unfold is_zero_row_upt_k_def, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
fix a::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
assume a_less_k: "to_nat a < k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat a < k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
have "A $ i $ a = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ a = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ a
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_preserves_previous_elements[symmetric])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. reduced_row_echelon_form_upt_k A k
 2. \<not> is_zero_row_upt_k ?a k A
 3. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 4. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 5. mod_type_class.to_nat a < k
[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 (4 subgoals):
 1. \<not> is_zero_row_upt_k ?a k A
 2. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 3. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 4. mod_type_class.to_nat a < k
[PROOF STEP]
show "\<not> is_zero_row_upt_k m k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k m 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> is_zero_row_upt_k m k A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A

goal (3 subgoals):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 2. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 3. mod_type_class.to_nat a < k
[PROOF STEP]
show "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

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

goal (2 subgoals):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 2. mod_type_class.to_nat a < k
[PROOF STEP]
show "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
using suc_not_zero greatest_not_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A

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

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

goal (1 subgoal):
 1. mod_type_class.to_nat a < k
[PROOF STEP]
show "to_nat a < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat a < k
[PROOF STEP]
using a_less_k
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a < k

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

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

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

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ a = (0::'a)
[PROOF STEP]
unfolding B_eq_Gauss_ij[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B $ i $ a = (0::'a)
[PROOF STEP]
using zero_i_suc_k a_less_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) B
mod_type_class.to_nat a < k

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

goal (1 subgoal):
 1. B $ i $ a = (0::'a)
[PROOF STEP]
by simp
[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 $ a = (0::'a)

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

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

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

goal (1 subgoal):
 1. \<And>ja. mod_type_class.to_nat ja < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
hence zero_jkA: "is_zero_row_upt_k j 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 j k A
[PROOF STEP]
using rref_upt_condition1[OF rref] i_less_j
[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)
i < j

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

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

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
have "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ j $ ja = A $ j $ ja"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = A $ j $ ja
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_preserves_previous_elements)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. reduced_row_echelon_form_upt_k A k
 2. \<not> is_zero_row_upt_k ?a k A
 3. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 4. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 5. mod_type_class.to_nat ja < k
[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 (4 subgoals):
 1. \<not> is_zero_row_upt_k ?a k A
 2. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 3. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 4. mod_type_class.to_nat ja < k
[PROOF STEP]
show "\<not> is_zero_row_upt_k m k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k m 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> is_zero_row_upt_k m k A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A

goal (3 subgoals):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 2. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 3. mod_type_class.to_nat ja < k
[PROOF STEP]
show "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

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

goal (2 subgoals):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 2. mod_type_class.to_nat ja < k
[PROOF STEP]
show "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
using suc_not_zero greatest_not_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A

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

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

goal (1 subgoal):
 1. mod_type_class.to_nat ja < k
[PROOF STEP]
show "to_nat ja < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat ja < k
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ja < k

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

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

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

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ ja = (0::'a)
[PROOF STEP]
using zero_jkA True
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k j k A
mod_type_class.to_nat ja < k

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

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

goal (2 subgoals):
 1. mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
 2. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)

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

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
hence k_eq_ja: "k = to_nat ja"
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat ja < k

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

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat ja < k \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ j $ ja = (0::'a)
[PROOF STEP]
proof (unfold k_eq_ja from_nat_to_nat_id, rule Gauss_Jordan_in_ij_0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows) \<le> n
 2. j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows)
[PROOF STEP]
show "\<exists>n. A $ n $ ja \<noteq> 0 \<and> (GREATEST n. \<not> is_zero_row_upt_k n (to_nat ja) A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows) \<le> n
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma k_eq_ja to_nat_from_nat
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
k = mod_type_class.to_nat ja
mod_type_class.to_nat ?j = ?k \<Longrightarrow> mod_type_class.from_nat ?k = ?j

goal (1 subgoal):
 1. \<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. A $ n $ ja \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows)
[PROOF STEP]
show "j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n (to_nat ja) A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows)
[PROOF STEP]
proof (unfold k_eq_ja[symmetric], rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (state)
this:
\<not> j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

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

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

goal (1 subgoal):
 1. \<not> j \<noteq> (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"
[PROOF STATE]
proof (prove)
using this:
j = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

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

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

goal (1 subgoal):
 1. \<not> j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
hence i_le_greatest: "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 le_Suc not_less
[PROOF STATE]
proof (prove)
using this:
i < (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
?a < ?b \<Longrightarrow> ?a + (1::?'a) \<le> ?b
(\<not> ?x < ?y) = (?y \<le> ?x)

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using zero_ikA
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A
is_zero_row_upt_k i 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:
j \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n (mod_type_class.to_nat ja) A) + (1::'rows)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (5 subgoals):
 1. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; \<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a)\<rbrakk> \<Longrightarrow> is_zero_row_upt_k j (Suc k) A
 2. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; mod_type_class.from_nat 0 \<le> m; 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))
 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
show "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
using condition_1_part_1[OF zero_k all_zero]
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k ?j (Suc k) A

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

goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; mod_type_class.from_nat 0 \<le> m; 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))
 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; mod_type_class.from_nat 0 \<le> m; 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))
 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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; mod_type_class.from_nat 0 \<le> m; 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))
 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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; mod_type_class.from_nat 0 \<le> m; 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))
 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
have j_not_0: "j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<noteq> (0::'rows)
[PROOF STEP]
using i_less_j least_mod_type not_le
[PROOF STATE]
proof (prove)
using this:
i < j
(0::?'a) \<le> ?n
(\<not> ?x \<le> ?y) = (?y < ?x)

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

goal (4 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. is_zero_row_upt_k m k A; mod_type_class.from_nat 0 \<le> m; 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))
 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
show "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A (from_nat 0) (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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))
[PROOF STEP]
using condition_1_part_2[OF j_not_0 all_zero Amk_not_zero]
[PROOF STATE]
proof (prove)
using this:
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))

goal (1 subgoal):
 1. 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))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
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))

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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
assume not_zero_mkA: "\<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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
show "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
using condition_1_part_3[OF rref i_less_j not_zero_mkA zero_below_greatest] zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
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> is_zero_row_upt_k j (Suc k) A
is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
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> is_zero_row_upt_k j (Suc k) A
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. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
show "is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
using condition_1_part_4[OF rref _ i_less_j not_zero_m greatest_eq_card] zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
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> is_zero_row_upt_k j (Suc k) A
is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
unfolding B ia nrows_def
[PROOF STATE]
proof (prove)
using this:
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> is_zero_row_upt_k j (Suc k) A
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. is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j (Suc k) 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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
assume not_zero_m: "\<not> is_zero_row_upt_k m k A"
    and greatest_not_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A"
and greatest_less_ma: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> ma"
    and A_ma_k_not_zero: "A $ ma $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

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

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

goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
unfolding B ia
[PROOF STATE]
proof (prove)
using this:
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> is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
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. is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma condition_2_part_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia\<equiv>(if \<forall>m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
  defines B:"B\<equiv>(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes not_zero_i_suc_k: "\<not> is_zero_row_upt_k i (Suc k) B"
  and all_zero: "\<forall>m. is_zero_row_upt_k m k A"
  and all_zero_k: "\<forall>m. A $ m $ from_nat k = 0"
  shows "A $ 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 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = 0
[PROOF STEP]
using ia all_zero
[PROOF STATE]
proof (prove)
using this:
ia \<equiv> if \<forall>m. is_zero_row_upt_k m k A then 0 else mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
\<forall>m. is_zero_row_upt_k m k A

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

goal (1 subgoal):
 1. A $ 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 0. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> 0 = nrows A then (0, A) else (0 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat 0) (mod_type_class.from_nat k))) = A
[PROOF STEP]
using all_zero_k
[PROOF STATE]
proof (prove)
using this:
\<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)

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

goal (1 subgoal):
 1. A $ 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]
using all_zero_k condition_1_part_1[OF _ all_zero] not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
\<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)
\<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a) \<Longrightarrow> is_zero_row_upt_k ?j (Suc k) 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_eq_A
[PROOF STATE]
proof (prove)
using this:
\<forall>m. A $ m $ mod_type_class.from_nat k = (0::'a)
\<forall>m\<ge>mod_type_class.from_nat 0. A $ m $ mod_type_class.from_nat k = (0::'a) \<Longrightarrow> is_zero_row_upt_k ?j (Suc k) A
\<not> is_zero_row_upt_k i (Suc k) A

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

goal:
No subgoals!
[PROOF STEP]
qed