## Stream: maths

### Topic: a*a = b*c -> gcd a b > 1

#### Rick Love (Aug 15 2020 at 14:12):

Good point, my final conclusion should be gcd a b > 1 (Corrected the title)

#### Rick Love (Aug 15 2020 at 14:14):

That also assumes a,b,c > 1

#### Rick Love (Aug 15 2020 at 14:18):

Ok, here is a better approach:

-- 4 * 4 = 2 * 8  -> gcd a b = 2 gcd a c = 4
-- 6 * 6 = 4 * 9  -> gcd a b = 2 gcd a c = 3
theorem multiple_factors_then_gcd (a b c k : nat):
a > 1 -> b > 1 -> c > 1 ->
a*a = b*c ->
gcd a b > 1 :=
begin
intros ha hb hc h,

let faa := factors (a*a),
let fbc := factors (b*c),
let fa := factors (a),
let fb := factors (b),
let fc := factors (c),
have h_faa_fbc : faa = fbc := by { dsimp [faa, fbc], rw h,},
have h_faa_fa_fa : faa = list.append fa fa := by {
-- cc,
-- Is there an operation for factors(a*a) = factors(a) ∧ factors(a)
sorry,
},

-- have
sorry,

end


#### Kevin Buzzard (Aug 15 2020 at 14:22):

If all you want to do is prove the gcd is bigger than one then you can just prove that if b>1 then it has a prime factor and this prime factor divides a^2 and hence a

#### Kevin Buzzard (Aug 15 2020 at 14:22):

I should think these facts are already in mathlib

#### Rick Love (Aug 15 2020 at 14:25):

Right, I was trying to use dvd and gcd, but I'll take a look at the prime functions. That's probably the missing piece 'prime factor divides a^2 and hence a'

#### Kenny Lau (Aug 15 2020 at 17:19):

if gcd a b <= 1 then gcd a b = 0 or gcd a b = 1.

In the first case, we have a = 0 or b = 0, contradiction.

In the second case, we have gcd (a * a) b = 1, so gcd (b * c) b = 1, so b = 1, contradiction.

#### Kenny Lau (Aug 15 2020 at 17:19):

no primes required

#### Rick Love (Aug 15 2020 at 17:38):

@Kenny Lau even with that, the difficulty is programming it in lean. How would you write that? Specifically how would you set up a proof by contradiction like this. (Note, I've done plenty of rw apply, etc, but still new to using exfalso and a contradiction).

#### Kenny Lau (Aug 15 2020 at 17:47):

  generalize hg : gcd a b = g,
by_contra h,
cases g with g,


(not tested)

#### Rick Love (Aug 15 2020 at 17:54):

Well that's giving me:
image.png

How do I pull the h out to work with it?

#### Johan Commelin (Aug 15 2020 at 17:59):

What do you mean with "pull out"? Does push_neg help?

#### Kenny Lau (Aug 15 2020 at 17:59):

what's your goal state before my invocations?

#### Rick Love (Aug 15 2020 at 19:52):

Johan Commelin said:

What do you mean with "pull out"? Does push_neg help?

Yeah, that helps. I'd just been using simp, but this gives better control.

Last updated: May 11 2021 at 16:22 UTC