357 from gcd have gcd3: "gcd num den = 1" |
357 from gcd have gcd3: "gcd num den = 1" |
358 by (simp add: gcd_commute_int[of den num]) |
358 by (simp add: gcd_commute_int[of den num]) |
359 from gcd2 have gcd4: "gcd b' a' = 1" |
359 from gcd2 have gcd4: "gcd b' a' = 1" |
360 by (simp add: gcd_commute_int[of a' b']) |
360 by (simp add: gcd_commute_int[of a' b']) |
361 have one: "num dvd b'" |
361 have one: "num dvd b'" |
362 by (rule coprime_dvd_mult_int[OF gcd3], simp add: dvd_def, rule exI[of _ a'], simp add: eq2 algebra_simps) |
362 by (metis coprime_dvd_mult_int[OF gcd3] dvd_triv_right eq2) |
363 have two: "b' dvd num" by (rule coprime_dvd_mult_int[OF gcd4], simp add: dvd_def, rule exI[of _ den], simp add: eq2 algebra_simps) |
363 have two: "b' dvd num" |
364 from one two |
364 by (metis coprime_dvd_mult_int[OF gcd4] dvd_triv_left eq2 zmult_commute) |
365 obtain k k' where k: "num = b' * k" and k': "b' = num * k'" |
365 from zdvd_antisym_abs[OF one two] b'p num |
366 unfolding dvd_def by auto |
366 have numb': "num = b'" by auto |
367 hence "num = num * (k * k')" by (simp add: algebra_simps) |
|
368 with num0 have prod: "k * k' = 1" by auto |
|
369 from zero_less_mult_iff[of b' k] b'p num k have kp: "k > 0" |
|
370 by auto |
|
371 from prod pos_zmult_eq_1_iff[OF kp, of k'] have "k = 1" by auto |
|
372 with k have numb': "num = b'" by auto |
|
373 with eq2 b'0 have "a' = den" by auto |
367 with eq2 b'0 have "a' = den" by auto |
374 with numb' adiv bdiv Pair show ?thesis by simp |
368 with numb' adiv bdiv Pair show ?thesis by simp |
375 qed |
369 qed |
376 qed |
370 qed |
377 qed |
371 qed |