equal
deleted
inserted
replaced
39 from a have b: "?S \<noteq> {}" by (simp) |
39 from a have b: "?S \<noteq> {}" by (simp) |
40 have c: "finite (?S)" by (simp add: finite_nonzero_positions) |
40 have c: "finite (?S)" by (simp add: finite_nonzero_positions) |
41 from hyp have d: "Max (?S) < m" by (simp add: a nrows_def) |
41 from hyp have d: "Max (?S) < m" by (simp add: a nrows_def) |
42 have "m \<notin> ?S" |
42 have "m \<notin> ?S" |
43 proof - |
43 proof - |
44 have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_le[OF |
44 have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_ge[OF c b]) |
45 c b]) |
|
46 moreover from d have "~(m <= Max ?S)" by (simp) |
45 moreover from d have "~(m <= Max ?S)" by (simp) |
47 ultimately show "m \<notin> ?S" by (auto) |
46 ultimately show "m \<notin> ?S" by (auto) |
48 qed |
47 qed |
49 thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect) |
48 thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect) |
50 qed |
49 qed |