equal
deleted
inserted
replaced
157 hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def) |
157 hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def) |
158 with False show ?thesis by auto |
158 with False show ?thesis by auto |
159 next |
159 next |
160 case True |
160 case True |
161 then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast |
161 then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast |
162 def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
162 define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)" |
163 def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
163 define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)" |
164 have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
164 have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
165 apply (subst n_def) |
165 apply (subst n_def) |
166 apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) |
166 apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) |
167 apply (rule exI[of _ l\<^sub>0]) |
167 apply (rule exI[of _ l\<^sub>0]) |
168 apply (simp add: l\<^sub>0_props) |
168 apply (simp add: l\<^sub>0_props) |