## Stream: new members

#### Adrian Chu (Jun 28 2019 at 14:35):

I am getting close to finishing proving my theorem

theorem mythm (n : ℕ) (r : fin n → ℕ) (s : ℕ)
(hn : n ≥ 1) (hr : ∀ i, r i ≥ 1) (hs : s ≥ 1)
(coprime : ∀ i : fin n, nat.gcd (r i) s = 1) :
∃ x : fin n → ℕ, ∃ y : ℕ,
(∀ i, x i ≥ 1) ∧ (finset.univ.sum (λ i, (x i)^(r i)) = y^s) := sorry


Now I have some lemmas remains to be proven. They all involves the recursive function n_lcm, as defined below.

def fin_n_to_list {n : ℕ} (x: fin n → ℕ) : list ℕ :=
(list.range n).map (λ i, if h : i < n then x ⟨i, h⟩ else 0)

def n_lcm {n : ℕ} (x : fin n → ℕ) : ℕ :=
list.foldl nat.lcm 1 (fin_n_to_list x)

lemma n_lcm_geq_1 {n : ℕ} (x : fin n → ℕ) (hx : ∀ i, x i ≥ 1):
n_lcm x ≥ 1 := sorry


I have read the chapter about induction TPIN a bit, but unfortunately have no idea on how to start proving the above lemma. Can anyone give some directions? Tganks

#### Kevin Buzzard (Jun 28 2019 at 14:37):

induction on n, and a proof for the n=2 case, will be the two ingredients that you need.

#### Adrian Chu (Jun 29 2019 at 08:45):

I start to see this is a big task. If we use induction, we at least need that lcm (a_1,...,a_n)=lcm(lcm(a_1,..a_(n-1)),a_n). and we dont yet have that either...

#### Mario Carneiro (Jun 29 2019 at 08:47):

You can use the multiset fold operation. It requires a proof that the operation is associative, but then you get that theorem for free

#### Kevin Buzzard (Jun 29 2019 at 18:48):

You should just need the base case and the n=2 case (for the inductive step). There will be some general theory in the library about how doing an operation to n things via folding is the same as doing it to n-1 things and then doing it once more. The proof will be short.

#### Kevin Buzzard (Jun 29 2019 at 18:50):

Well, the proof of the theorem for lists will be short. You'll then have to convert back to your fin n representation.

Last updated: May 13 2021 at 06:15 UTC