# Zulip Chat Archive

## 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):

you can start with:

```
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