[STATEMENT]
lemma is_solution_solve_system:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  shows "is_solution x A b = is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution x A b = is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
using solve_system_imp_is_solution is_solution_imp_solve_system
[PROOF STATE]
proof (prove)
using this:
is_solution ?x (fst (solve_system ?A ?b)) (snd (solve_system ?A ?b)) \<Longrightarrow> is_solution ?x ?A ?b
is_solution ?x ?A ?b \<Longrightarrow> is_solution ?x (fst (solve_system ?A ?b)) (snd (solve_system ?A ?b))

goal (1 subgoal):
 1. is_solution x A b = is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
by blast


[STATEMENT]
lemma inconsistent: "inconsistent A b = (\<not> (\<exists>x. is_solution x A b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsistent A b = (\<nexists>x. is_solution x A b)
[PROOF STEP]
unfolding inconsistent_def consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nexists>x. is_solution x A b) = (\<nexists>x. is_solution x A b)
[PROOF STEP]
by simp


[STATEMENT]
lemma solve_consistent_rref_code[code abstract]:
  shows "vec_nth (solve_consistent_rref A b) = (% j. if (\<exists>i. A $ i $ j = 1 \<and> j=(LEAST n. A $ i $ n \<noteq> 0)) then b $ (THE i. A $ i $ j = 1) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (solve_consistent_rref A b) = (\<lambda>j. if \<exists>i. A $ i $ j = (1::'b) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'b)) then b $ (THE i. A $ i $ j = (1::'b)) else (0::'b))
[PROOF STEP]
unfolding solve_consistent_rref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>j. if \<exists>i. A $ i $ j = (1::'b) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'b)) then b $ (THE i. A $ i $ j = (1::'b)) else (0::'b)) = (\<lambda>j. if \<exists>i. A $ i $ j = (1::'b) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'b)) then b $ (THE i. A $ i $ j = (1::'b)) else (0::'b))
[PROOF STEP]
by auto


[STATEMENT]
lemma rank_ge_imp_is_solution:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes con: "rank A \<ge> (if (\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0)
                                            then (to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1) else 0)"
  shows "is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b
[PROOF STEP]
have "is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b)
[PROOF STEP]
proof (unfold is_solution_def solve_consistent_rref_def, subst matrix_vector_mult_def, vector, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ i $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ i
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ i $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ i
[PROOF STEP]
let ?f="\<lambda>j. Gauss_Jordan A $ a $ j *
      (if \<exists>i. Gauss_Jordan A $ i $ j = 1 \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> 0)
        then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = 1) else 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ i $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ i
[PROOF STEP]
show "sum ?f UNIV = (P_Gauss_Jordan A *v b) $ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
proof (cases "A=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = 0

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence rank_A_eq_0:"rank A = 0"
[PROOF STATE]
proof (prove)
using this:
A = 0

goal (1 subgoal):
 1. rank A = 0
[PROOF STEP]
using rank_0
[PROOF STATE]
proof (prove)
using this:
A = 0
rank 0 = 0

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

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "(P_Gauss_Jordan A *v b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P_Gauss_Jordan A *v b = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P_Gauss_Jordan A *v b \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume not_zero: "P_Gauss_Jordan A *v b \<noteq> 0"
[PROOF STATE]
proof (state)
this:
P_Gauss_Jordan A *v b \<noteq> 0

goal (1 subgoal):
 1. P_Gauss_Jordan A *v b \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence ex_a: "\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
P_Gauss_Jordan A *v b \<noteq> 0

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)
[PROOF STEP]
by (metis vec_eq_iff zero_index)
[PROOF STATE]
proof (state)
this:
\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)

goal (1 subgoal):
 1. P_Gauss_Jordan A *v b \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using con
[PROOF STATE]
proof (prove)
using this:
(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding if_P[OF ex_a]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 \<le> rank A

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding rank_A_eq_0
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 \<le> 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P_Gauss_Jordan A *v b = 0

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P_Gauss_Jordan A *v b = 0

goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
unfolding A_0_imp_Gauss_Jordan_0[OF True]
[PROOF STATE]
proof (prove)
using this:
P_Gauss_Jordan A *v b = 0

goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. 0 $ a $ j * (if \<exists>i. 0 $ i $ j = (1::'a) \<and> j = (LEAST n. 0 $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. 0 $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A \<noteq> 0

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
note A_not_zero=False
[PROOF STATE]
proof (state)
this:
A \<noteq> 0

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
define not_zero_positions_row_a where "not_zero_positions_row_a = {j. Gauss_Jordan A $ a $ j \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a = {j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
define zero_positions_row_a where "zero_positions_row_a = {j. Gauss_Jordan A $ a $ j = 0}"
[PROOF STATE]
proof (state)
this:
zero_positions_row_a = {j. Gauss_Jordan A $ a $ j = (0::'a)}

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have UNIV_rw: "UNIV = not_zero_positions_row_a \<union> zero_positions_row_a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = not_zero_positions_row_a \<union> zero_positions_row_a
[PROOF STEP]
unfolding zero_positions_row_a_def not_zero_positions_row_a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} \<union> {j. Gauss_Jordan A $ a $ j = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNIV = not_zero_positions_row_a \<union> zero_positions_row_a

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have disj: "not_zero_positions_row_a \<inter> zero_positions_row_a = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_zero_positions_row_a \<inter> zero_positions_row_a = {}
[PROOF STEP]
unfolding zero_positions_row_a_def not_zero_positions_row_a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} \<inter> {j. Gauss_Jordan A $ a $ j = (0::'a)} = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a \<inter> zero_positions_row_a = {}

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have sum_zero: "(sum ?f zero_positions_row_a) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (0::'a)
[PROOF STEP]
by (unfold zero_positions_row_a_def, rule sum.neutral, fastforce)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (0::'a)

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "sum ?f (UNIV::'cols set)=sum ?f (not_zero_positions_row_a \<union> zero_positions_row_a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))
[PROOF STEP]
unfolding UNIV_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "... = sum ?f (not_zero_positions_row_a) + (sum ?f zero_positions_row_a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))
[PROOF STEP]
by (rule sum.union_disjoint[OF _ _ disj], simp+)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a \<union> zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "... = sum ?f (not_zero_positions_row_a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))
[PROOF STEP]
unfolding sum_zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (0::'a) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "... = (P_Gauss_Jordan A *v b) $ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
proof (cases "not_zero_positions_row_a = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. not_zero_positions_row_a = {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a = {}

goal (2 subgoals):
 1. not_zero_positions_row_a = {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
note zero_row_a=True
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a = {}

goal (2 subgoals):
 1. not_zero_positions_row_a = {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
proof (cases "\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)

goal (2 subgoals):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence "(P_Gauss_Jordan A *v b) $ a = 0"
[PROOF STATE]
proof (prove)
using this:
\<nexists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)

goal (1 subgoal):
 1. (P_Gauss_Jordan A *v b) $ a = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (2 subgoals):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
using this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. (\<Sum>j\<in>{}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have rank_not_0: "rank A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A \<noteq> 0
[PROOF STEP]
by (metis A_not_zero less_not_refl3 rank_Gauss_Jordan rank_greater_zero)
[PROOF STATE]
proof (state)
this:
rank A \<noteq> 0

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have greatest_less_a: "(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < a
[PROOF STEP]
proof (unfold is_zero_row_def, rule greatest_less_zero_row)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
 2. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A)
 3. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
show " reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
[PROOF STEP]
using rref_Gauss_Jordan
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form (Gauss_Jordan ?A)

goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
[PROOF STEP]
unfolding reduced_row_echelon_form_def
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k (Gauss_Jordan ?A) (ncols (Gauss_Jordan ?A))

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

goal (2 subgoals):
 1. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A)
 2. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
show "is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A)
[PROOF STEP]
by (metis (mono_tags) Collect_empty_eq is_zero_row_upt_ncols not_zero_positions_row_a_def zero_row_a)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
show "\<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
by (metis False Gauss_Jordan_not_0 is_zero_row_upt_ncols vec_eq_iff zero_index)
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < a

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence "to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < to_nat a"
[PROOF STATE]
proof (prove)
using this:
(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < a

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < mod_type_class.to_nat a
[PROOF STEP]
using to_nat_mono
[PROOF STATE]
proof (prove)
using this:
(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < a
?a < ?b \<Longrightarrow> mod_type_class.to_nat ?a < mod_type_class.to_nat ?b

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < mod_type_class.to_nat a
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < mod_type_class.to_nat a

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence rank_le_to_nat_a: "rank A \<le> to_nat a"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < mod_type_class.to_nat a

goal (1 subgoal):
 1. rank A \<le> mod_type_class.to_nat a
[PROOF STEP]
unfolding rank_eq_suc_to_nat_greatest[OF A_not_zero]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < mod_type_class.to_nat a

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1 \<le> mod_type_class.to_nat a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rank A \<le> mod_type_class.to_nat a

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) < to_nat a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a
[PROOF STEP]
using con
[PROOF STATE]
proof (prove)
using this:
(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a
[PROOF STEP]
unfolding if_P[OF True]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 \<le> rank A

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a
[PROOF STEP]
using rank_le_to_nat_a
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 \<le> rank A
rank A \<le> mod_type_class.to_nat a

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence "(GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) < a"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < mod_type_class.to_nat a

goal (1 subgoal):
 1. (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < a
[PROOF STEP]
by (metis not_le to_nat_mono')
[PROOF STATE]
proof (state)
this:
(GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < a

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence "(P_Gauss_Jordan A *v b) $ a = 0"
[PROOF STATE]
proof (prove)
using this:
(GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < a

goal (1 subgoal):
 1. (P_Gauss_Jordan A *v b) $ a = (0::'a)
[PROOF STEP]
using not_greater_Greatest
[PROOF STATE]
proof (prove)
using this:
(GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) < a
(GREATEST x. ?P x) < ?k \<Longrightarrow> \<not> ?P ?k

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

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
unfolding zero_row_a
[PROOF STATE]
proof (prove)
using this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. (\<Sum>j\<in>{}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a \<noteq> {}

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
note not_empty=False
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a \<noteq> {}

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have not_zero_positions_row_a_rw: "not_zero_positions_row_a = {LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0} \<union> (not_zero_positions_row_a - {LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_zero_positions_row_a = {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} \<union> (not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)})
[PROOF STEP]
unfolding not_zero_positions_row_a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} = {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} \<union> ({j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)})
[PROOF STEP]
by (metis (mono_tags) Collect_cong False LeastI_ex bot_set_def empty_iff insert_Diff_single insert_absorb insert_is_Un mem_Collect_eq not_zero_positions_row_a_def)
[PROOF STATE]
proof (state)
this:
not_zero_positions_row_a = {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)} \<union> (not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)})

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have sum_zero': "sum ?f (not_zero_positions_row_a - {LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0}) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (0::'a)
[PROOF STEP]
by (rule sum.neutral, auto, metis is_zero_row_def' rref_Gauss_Jordan rref_condition4_explicit zero_neq_one)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (0::'a)

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "sum ?f (not_zero_positions_row_a) = sum ?f {LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0} + sum ?f (not_zero_positions_row_a - {LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))
[PROOF STEP]
by (subst not_zero_positions_row_a_rw, rule sum.union_disjoint[OF _ _ _], simp+)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a)))

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "... = ?f (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a))
[PROOF STEP]
using sum_zero'
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a))

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) + (\<Sum>j\<in>not_zero_positions_row_a - {LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)}. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a))

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "... = (P_Gauss_Jordan A *v b) $ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
proof (cases "\<exists>i. (Gauss_Jordan A) $ i $ (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0) = 1 \<and> (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0) = (LEAST n. (Gauss_Jordan A) $ i $ n \<noteq> 0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have A_least_eq_1: "(Gauss_Jordan A) $ a $ (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by (metis (mono_tags) empty_Collect_eq is_zero_row_def' not_empty not_zero_positions_row_a_def rref_Gauss_Jordan rref_condition2_explicit)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)

goal (2 subgoals):
 1. \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)

goal (2 subgoals):
 1. \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "(THE i. (Gauss_Jordan A) $ i $ (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0) = 1) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) = a
[PROOF STEP]
proof (rule the_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)
 2. \<And>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<Longrightarrow> i = a
[PROOF STEP]
show "(Gauss_Jordan A) $ a $ (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using A_least_eq_1
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)

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

goal (1 subgoal):
 1. \<And>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<Longrightarrow> i = a
[PROOF STEP]
show "\<And>i. (Gauss_Jordan A) $ i $ (LEAST j. (Gauss_Jordan A) $ a $ j \<noteq> 0) = 1 \<Longrightarrow> i = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<Longrightarrow> i = a
[PROOF STEP]
by (metis calculation is_zero_row_def' rref_Gauss_Jordan rref_condition4_explicit zero_neq_one)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ ?i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<Longrightarrow> ?i = a

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

goal (2 subgoals):
 1. \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
 2. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)
(THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)
(THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) = a

goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
unfolding if_P[OF True]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)
(THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) = a

goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
have "is_zero_row a (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row a (Gauss_Jordan A)
[PROOF STEP]
using False rref_Gauss_Jordan rref_condition2
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a))
reduced_row_echelon_form (Gauss_Jordan ?A)
reduced_row_echelon_form ?A \<Longrightarrow> \<forall>i. \<not> is_zero_row i ?A \<longrightarrow> ?A $ i $ (LEAST k. ?A $ i $ k \<noteq> (0::?'a)) = (1::?'a)

goal (1 subgoal):
 1. is_zero_row a (Gauss_Jordan A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_zero_row a (Gauss_Jordan A)

goal (1 subgoal):
 1. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
hence "(P_Gauss_Jordan A *v b) $ a = 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row a (Gauss_Jordan A)

goal (1 subgoal):
 1. (P_Gauss_Jordan A *v b) $ a = (0::'a)
[PROOF STEP]
by (metis (mono_tags) IntI disj empty_iff insert_compr insert_is_Un is_zero_row_def' mem_Collect_eq not_zero_positions_row_a_rw zero_positions_row_a_def)
[PROOF STATE]
proof (state)
this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. \<nexists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
unfolding if_not_P[OF False]
[PROOF STATE]
proof (prove)
using this:
(P_Gauss_Jordan A *v b) $ a = (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (0::'a) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ a $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) * (if \<exists>i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a) \<and> (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ (LEAST j. Gauss_Jordan A $ a $ j \<noteq> (0::'a)) = (1::'a)) else (0::'a)) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. not_zero_positions_row_a \<noteq> {} \<Longrightarrow> (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. (\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>not_zero_positions_row_a. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
show "sum ?f UNIV = (P_Gauss_Jordan A *v b) $ a"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. Gauss_Jordan A $ a $ j * (if \<exists>i. Gauss_Jordan A $ i $ j = (1::'a) \<and> j = (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = (1::'a)) else (0::'a))) = (P_Gauss_Jordan A *v b) $ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b)

goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b)

goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b
[PROOF STEP]
apply (subst is_solution_solve_system)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b) \<Longrightarrow> is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
unfolding solve_system_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b) \<Longrightarrow> is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (snd (Gauss_Jordan_PA A)) (fst (Gauss_Jordan_PA A) *v b)
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b) \<Longrightarrow> is_solution (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsistent_imp_rank_less:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes inc: "inconsistent A b"
  shows "rank A < (if (\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) then (to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0 then to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1 else 0)"
[PROOF STATE]
proof (state)
this:
\<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. \<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<Longrightarrow> False
[PROOF STEP]
hence "(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0 then to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1 else 0) \<le> rank A"
[PROOF STATE]
proof (prove)
using this:
\<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A

goal (1 subgoal):
 1. \<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<Longrightarrow> False
[PROOF STEP]
hence "consistent A b"
[PROOF STATE]
proof (prove)
using this:
(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A

goal (1 subgoal):
 1. consistent A b
[PROOF STEP]
using rank_ge_imp_consistent
[PROOF STATE]
proof (prove)
using this:
(if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A
(if \<exists>a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a)) + 1 else 0) \<le> rank ?A \<Longrightarrow> consistent ?A ?b

goal (1 subgoal):
 1. consistent A b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consistent A b

goal (1 subgoal):
 1. \<not> rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
consistent A b

goal (1 subgoal):
 1. False
[PROOF STEP]
using inc
[PROOF STATE]
proof (prove)
using this:
consistent A b
inconsistent A b

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding inconsistent_def
[PROOF STATE]
proof (prove)
using this:
consistent A b
\<not> consistent A b

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

goal:
No subgoals!
[PROOF STEP]
qed