Stream: maths

Topic: a*a = b*c -> gcd a b = min a b

Rick Love (Aug 15 2020 at 13:48):

I'm trying to prove the following, but I am stuck. I'm not sure how to proceed.

A proof in words would be something like:

• get all prime factors for both sides
• the prime factors must match
• the union of all factors in a * a = b * c
• the common factors a,b + common factors a,c = all factors
• common factors a,b = min a,b

However, I don't know how to break the equality into it's factors and prove their intersection in lean

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

cases eq_or_not a b with ab_eq ab_neq,
-- case a = b
{
rw ab_eq,
rw min_self,
apply gcd_eq_left,
refl,
},

cases le_or_gt a b with ab_le ab_gt,
-- case a < b
{
have haltb : a < b, {apply le_and_ne_then_lt, split, apply ab_le, apply ab_neq,},
rw min_eq_left ab_le,
apply gcd_eq_left,
apply dvd.intro k,

-- revert a_1,
-- contrapose,
-- intros,
-- rw a_1,

-- rw nat.div,
sorry,
},

-- case a > b
have hageb : a >= b, {apply le_of_lt ab_gt},
rw min_eq_right hageb,
apply gcd_eq_right,
sorry,

-- case a > b

-- split,
-- apply dvd.intro a,
-- cc,

-- split,
-- apply dvd.intro d,
-- cc,

-- apply dvd.intro c,
-- cc,
end


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

Actually starting to make progress now that I had to think about how to do that in words:

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

let faa := factors (a*a),
let fbc := factors (b*c),
have h_faa_fbc : faa = fbc := by { dsimp [faa, fbc], rw h,},

-- have
end


Kevin Buzzard (Aug 15 2020 at 14:02):

How about 12^2=9*16?

Kevin Buzzard (Aug 15 2020 at 14:03):

Or even 6^2=9*4?

Last updated: May 14 2021 at 19:21 UTC