## Stream: maths

### Topic: By schoolkid

#### Chris Hughes (Nov 13 2019 at 00:57):

A 12 year old just got a prize for proving this.

example : ∀ n : ℕ, 7 ∣ n ↔ 7 ∣ (n / 10 + 5 * (n % 10))


This can be turned into a Presburger formula right? Should omega be able to do it?

I tried turning it into a Presburger formula, but it didn't seem to work.

import tactic.omega
open nat
example (n : ℕ) : 7 ∣ n ↔ 7 ∣ (n / 10 + 5 * (n % 10)) :=
begin
rw [dvd_iff_mod_eq_zero, dvd_iff_mod_eq_zero],
have := nat.mod_lt n (show 0 < 7, by norm_num),
have := nat.mod_lt n (show 0 < 10, by norm_num),
have := nat.mod_lt (n / 10 + 5 * (n % 10)) (show 7 > 0, by norm_num),
have := nat.mod_add_div (n / 10 + 5 * (n % 10)) 7,
repeat { revert this },
generalize : n % 7 = a,
generalize : n / 7 = b,
generalize : n / 10 = c,
generalize : n % 10 = d,
generalize : (c + 5 * d) % 7 = e,
generalize : (c + 5 * d) / 7 = f,
omega -- doesn't work
end


#### Kevin Buzzard (Nov 13 2019 at 07:33):

I would not be surprised if you could find some previous reference to this test in some popular maths book from the 50s, it's very dangerous calling it a new formula. But good on him. It's 7|10x+y iff 7|x+5y. If you apply the test to 14 you get 21.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 19:34):

It's m | a x + b y iff m | (an-br) x + bn y for hcf(m, n) = 1 (or something like that). I think this stuff is taught in high school.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 19:34):

What's omega?

#### Johan Commelin (Nov 14 2019 at 19:34):

A tactic that proves statements in the language of the ordered group of integers

#### Johan Commelin (Nov 14 2019 at 19:35):

So you are allowed to add and compare integers using ≤ but you can only multiply with constants

Last updated: May 14 2021 at 20:13 UTC