A simple problem

Formalize and prove that the product of two consecutive natural numbers is even.

Exercise 21

Formalize and prove that the product of three consecutive natural numbers is divisible by 2.

Exercise 22

Formalize and prove that the product of three consecutive natural numbers is divisible by 3.

Exercise 23

Formalize and prove that the product of three consecutive natural numbers is divisible by 6.

Partial solution for Exercise 23

It seems natural to prove that the product of three consecutive natural numbers is divisible by 6 as a corollary of the two previous exercises, i.e., that the product of three consecutive natural numbers is divisible both by 2 and by 3. Or again, more generally:

Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3 :
  forall (n : nat)
         (q2 : nat),
    n = 2 * q2 ->
    forall q3 : nat,
      n = 3 * q3 ->
      exists q6 : nat,
        n = 6 * q6.

Proving this property, however, is not done by routine induction, and so we will revisit it in Week 11 (Exercise 15 and Exercise 16) once we have built more muscle.

Exercise 24

Formalize and prove that the product of four consecutive natural numbers is divisible by 2.

Exercise 25

Formalize and prove that the product of four consecutive natural numbers is divisible by 3.

Exercise 26

Formalize and prove that the product of four consecutive natural numbers is divisible by 4.

Exercise 27

Formalize and prove that the product of four consecutive natural numbers is divisible by 6.

Exercise 28

Formalize and prove that the product of four consecutive natural numbers is divisible by 8.

Exercise 29

Formalize and prove that the product of four consecutive natural numbers is divisible by 12.

Exercise 30

Formalize and prove that the product of four consecutive natural numbers is divisible by 24.

Exercise 31

Formalize and prove that the product of five consecutive natural numbers is divisible by 120.

Interlude

Alfrothul: Wow.

Dana: Right.

Alfrothul: We have seen these numbers before.

Dana: You mean 2, 6, 24, and 120?

Alfrothul: Yes, the biggest of the divisors.

Bong-sun: Which begs the question.

Anton: The question?

Bong-sun: Well, if all these products are divisible, what is the result of the divisions?

Loki: Need a hand?

Anton (prudently): Er, yes?

Loki: Let me add one more exercise.

Exercise 32

Formalize and prove that the product of six consecutive natural numbers is divisible by 720.

Postlude

Mimer: Why, thank you, Loki.

Loki: You are most welcome.

Dana: So 2, 6, 24, 120, and 720, eh.

Alfrothul: We have seen these numbers before.

Exercise 33

Perusing all the exercises above (without solving them, unless of course you absolutely need to) begs the following question:

Since the product of consecutive numbers is divisible by such other numbers, the result of these divisions by the largest possible such other number (i.e.,

• 2 for the product of two consecutive numbers,
• 6 for the product of three consecutive numbers,
• 24 for the product of four consecutive numbers,
• 120 for the product of five consecutive numbers,
• 720 for the product of six consecutive numbers,
• etc.)

is an integer (well, a natural number), because that’s what it means to be divisible.

In other words,

• when we divide the product of two consecutive natural numbers by 2, we get an integer,
• when we divide the product of three consecutive natural numbers by 6, we get an integer,
• when we divide the product of four consecutive natural numbers by 24, we get an integer,
• when we divide the product of five consecutive natural numbers by 120, we get an integer,
• etc.

What is this integer? How would you characterize it?

Credit

Thanks are due to Yves Bertot for the initial simple problem at this stage of the lecture notes.

Version

Added the partial solution for Exercise 23 [23 May 2025]

Expanded the statement of Exercise 33 in an attempt to clarify it [21 Mar 2025]

Added “(i.e., 2 for the product of two consecutive numbers, etc.)” in the statement of Exercise 33 [10 Mar 2025]

Created [07 Mar 2025]