divisibility - stuck on beginner problem

Stream: new members

[rzeta0]

I want to prove that $7|n \land 9|n \implies 63|n$,

I have the following goal state:

n c1 : ℤ
hc1 : n = 7 * c1
c2 : ℤ
hc2 : n = 9 * c2
⊢ ∃ c, n = 63 * c

I am stuck because my brain wants to solve the problem using the fundamental theorem of arithmetic - prime factors.

But that isn't the strategy suggested by any of the previous content of Mechanics of Proofs - which most uses "substitution".

---

If instead I needed to prove that $8|n \land 2|n \implies 4|n$ then I can see the path that uses "substitution".

I guess it is a maths insight I'm not seeing, rather than anything about lean/mathlib.

[Derek Rhodes]

These ones are tricky! Without giving it away, the last step is factoring 63 out of a difference, with your choice of variable names it looks like 63 * (?*c1 - ?*c2) to satisfy the divisibility.

But, I think your next step should be to establish on paper that:

9 * n = 63 * c1
7 * n = 63 * c2

Then find an expression for n itself with 36*n - 35*n and use a calc block to finish it.

[Zhang Qinchuan]

You can use theorem docs#Int.modEq_and_modEq_iff_modEq_mul .

import Mathlib

example (n : ℤ) (h1 : 7 ∣ n) (h2 : 9 ∣ n) : 63 ∣ n := by
  rw [Int.dvd_iff_emod_eq_zero] at h1 h2 ⊢
  change _ ≡ 0 [ZMOD _] at h1 h2 ⊢
  rw [show (63 : ℤ) = 7 * 9 by norm_num, ← Int.modEq_and_modEq_iff_modEq_mul]
  . exact ⟨h1, h2⟩
  . norm_num

[rzeta0]

Derek Rhodes said:

These ones are tricky! Without giving it away, the last step is factoring 63 out of a difference, with your choice of variable names it looks like 63 * (?*c1 - ?*c2) to satisfy the divisibility.

But, I think your next step should be to establish on paper that:

9 * n = 63 * c1
7 * n = 63 * c2

Then find an expression for n itself with 36*n - 35*n and use a calc block to finish it.

Thanks for the hint. I gotta say, I don't find these types of exercises very educational or satisfying. It seems a algebra torture to see if you can find the right combination...

[Derek Rhodes]

There is a bit of trial an error, I hopped over to python and wrote a nested for loop to find the factors.

[Kyle Miller]

Here's a "I've taught number theory before" solution:

example (n c1 : ℤ) (hc1 : n = 7 * c1) (c2 : ℤ) (hc2 : n = 9 * c2) : ∃ c, n = 63 * c := by
  use 4 * c2 - 3 * c1
  convert_to n = 4 * 7 * (9 * c2) - 3 * 9 * (7 * c1)
  · ring
  rw [← hc2, ← hc1]
  ring

It's like Derek's, but I started with using the extended Euclidean algorithm to get 4 * 7 - 3 * 9 = 1 (the fact 7 and 9 are coprime means there has to exist some constants a and b such that a * 7 + b * 9 = 1, that's Bézout's identity).

Then I calculated
$n = (4\cdot 7-3\cdot 9)n = 4\cdot 7n - 3\cdot 9n = 4\cdot 7\cdot 9c_2-3\cdot 9\cdot 7c_1=63(4c_2-3c_1)$
so using $c=4c_2-3c_1$ will work.

If you haven't seen this stuff before, it can feel like it's really out of left field!

[rzeta0]

Derek Rhodes said:

There is a bit of trial an error, I hopped over to python and wrote a nested for loop to find the factors.

I've used (horror!) a spreadsheet to trial/error coefficients for some of the other exercises that are similarly "find the right combination".

I'm determined not to skip any exercise so I'll persevere.

Thanks for the ideas everyone

[Johan Commelin]

So a key takeaway from Kyle's message is to read about the Euclidean algorithm, if you haven't seen that before.

[Johan Commelin]

(Which is the main ingredient in unique prime factorisation of integers)

[Derek Rhodes]

That is no doubt sound advice, however this particular exercise is from chapter 3.5, where as Euclid is covered later in chapter 7.2. In the author's defense, it's not uncommon for good teachers to show the hard way in order to motivate the value of the easier way.