# Zulip Chat Archive

## Stream: new members

### Topic: Hints/Suggestions

#### Newell Jensen (Apr 08 2023 at 06:22):

I have been trying to prove the simple fact that a prime `p`

less than `n`

is less than `n#`

, which is product of all primes less than or equal to `n`

. Should be super straight forward one would think (and maybe it is but I haven't seen the light) and could use some guidance. I would think that I would need to use the proof that `{p}`

is actually prime at this point somehow. Is there a more straightforward way to do this?

```
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.NumberTheory.Primorial
local notation x "#" => primorial x
-- Need p ∣ n# first
--example (n : Nat) (h : 0 < n#) : p ∣ n# → p ≤ n# := Nat.le_of_dvd h
-- def primorial (n : ℕ) : ℕ :=
-- ∏ p in filter Nat.Prime (range (n + 1)), p
example (n p : Nat) (pp : Nat.Prime p) (hp : p < n) : p ∣ n# := by
use (∏ i in Finset.filter Nat.Prime (Finset.range (n + 1)) \ {p}, i)
unfold primorial
sorry
```

#### Ruben Van de Velde (Apr 08 2023 at 06:34):

Maybe docs#finset.dvd_prod_of_mem could help

#### Newell Jensen (Apr 08 2023 at 06:44):

I actually was trying to use that earlier but didn't figure it out. Will give it another go.

#### Ruben Van de Velde (Apr 08 2023 at 06:51):

(the lean 4 version, of course. I wasn't paying enough attention)

#### Kevin Buzzard (Apr 08 2023 at 07:20):

Why not just prove `n<=n#`

? Then you don't need anything about p at all.

#### Kevin Buzzard (Apr 08 2023 at 07:22):

Did we ever get that there's always a prime between n and 2n? There was a PR about that for ages. Then n<=n# should be easy by strong induction

#### Mario Carneiro (Apr 08 2023 at 07:25):

#### Kevin Buzzard (Apr 08 2023 at 07:27):

I guess this isn't really the super straightforward approach though. You can prove that `2*2^t<=(2^t)#`

by induction on t>=3 or whatever using Bertrand and then n<=n# follows. But for this question the elementary approach above will work fine and probably my suggestion, whilst perhaps useful for the library, is just a distraction.

#### Kevin Buzzard (Apr 08 2023 at 07:31):

Elementary approach: I would instead prove that if p>2 is prime then 2p divides p#, then prove that if a<=b then a# divides b#. Those lemmas should see you on your way

#### Kevin Buzzard (Apr 08 2023 at 07:34):

Then if 2<p<n we have 2p divides n# so p<n#, and for 2 you just need that 6 divides 3# so 6<=n#

#### Kevin Buzzard (Apr 08 2023 at 07:35):

(0 < n# is the other thing you need)

#### Kevin Buzzard (Apr 08 2023 at 07:37):

The reason the argument is not completely trivial is that if we replace the set of prime numbers with some random infinite set X and define Xorials the same way then the result is not true, eg if X={2,5,7,...} then 3#=2 is not strictly greater than 2

#### Kevin Buzzard (Apr 08 2023 at 07:38):

Aka you say this is a simple fact but where is your rigorous paper proof? Or do you just have a proof of the form "for n large this is obvious and for n small check by hand"?

#### Newell Jensen (Apr 08 2023 at 07:41):

`n#`

grows really fast compared to `n`

, hence the remark.

#### Newell Jensen (Apr 08 2023 at 07:44):

I don't have much experience with `Finset`

and so that is what was causing me some pain. Right now I am just trying to figure out how to actually show something divides the primorial. As mentioned there is `dvd_prod_of_mem`

but that needs a proof that `p`

is in the filtered `Finset`

and I think I need to have an instance of that membership somehow? Now sure...still trying to figure it out.

#### Mario Carneiro (Apr 08 2023 at 07:46):

You definitely need something about there being enough primes, since if you replace the set of primes with a random other set of natural numbers it's not necessarily true

#### Kevin Buzzard (Apr 08 2023 at 07:46):

Yeah that's exactly the kind of "this is obvious so let's not write down the details" proof that you can't formalise, because formalisation involves writing down the details. My sketch above should hopefully turn into a rigorous proof which isn't hard to formalise but note that with my X example above it's also true that n# grows really fast with n. Another bad example would be X is all the primes up to 1000 and then skip all the primes up to N=10^10^10^10 and then start again with the remaining primes, then n<=n# is false for n=N-1 and you say "well obviously the primes don't look like that" and I say "yeah but that's the prime number theorem"

#### Mario Carneiro (Apr 08 2023 at 07:47):

actually the PNT doesn't even help here since it's an asymptotic statement - it is consistent with your hypothetical

#### Mario Carneiro (Apr 08 2023 at 07:49):

A number which divides a primorial is necessarily squarefree, but I don't think there is much else you can say about such numbers

#### Mario Carneiro (Apr 08 2023 at 07:50):

Your original statement sounds very simple though: `p < n`

implies `p | n#`

because `p`

is one of the factors involved in the definition of `n#`

#### Yaël Dillies (Apr 08 2023 at 07:55):

```
import number_theory.primorial
open finset
example (n p : ℕ) (hp : p.prime) (hpn : p ≤ n) : p ∣ primorial n :=
dvd_prod_of_mem _ $ mem_filter.2 ⟨mem_range.2 $ nat.lt_succ_iff.2 hpn, hp⟩
```

#### Newell Jensen (Apr 08 2023 at 07:56):

I hope one day I can figure this stuff out as fast. Thanks, will try and digest what you did here.

#### Notification Bot (Apr 08 2023 at 08:00):

Newell Jensen has marked this topic as resolved.

#### Ruben Van de Velde (Apr 08 2023 at 08:00):

But note that p dvd n# only implies p<=n#, not immediately p<n#, which you were talking about earlier

#### Newell Jensen (Apr 08 2023 at 08:02):

Yeah I am aware of that. I was just trying to get past this hurdle at this point. Appreciate everyone's comments, thanks again.

#### Mario Carneiro (Apr 08 2023 at 08:15):

it's not hard to prove that `2 < p <= n`

implies `2 * p | n#`

by something similar to Yael's proof though

#### Mario Carneiro (Apr 08 2023 at 08:15):

and for p = 2 the claim p < n# is false

#### Newell Jensen (Apr 08 2023 at 08:20):

@Yaël Dillies the dollar sign in the middle of the angles brackets is throwing me off. My understanding is that $ is for not having to have parenthesis when you are nesting them to the right. When I do a simple substitution of "(" for the dollar signs and ")" at the very end (same amount to balance them), it isn't working.

#### Notification Bot (Apr 08 2023 at 08:22):

Newell Jensen has marked this topic as unresolved.

#### Yaël Dillies (Apr 08 2023 at 08:25):

Here's the equivalent dollar-less proof.

```
import number_theory.primorial
open finset
example (n p : ℕ) (hp : p.prime) (hpn : p ≤ n) : p ∣ primorial n :=
dvd_prod_of_mem _ (mem_filter.2 ⟨mem_range.2 (nat.lt_succ_iff.2 hpn), hp⟩)
```

Probably you tried doing `dvd_prod_of_mem _ (mem_filter.2 ⟨mem_range.2 (nat.lt_succ_iff.2 hpn, hp⟩))`

instead?

#### Newell Jensen (Apr 08 2023 at 08:26):

I tried that and some other variations :)

#### Newell Jensen (Apr 08 2023 at 08:27):

So how did you know dollar sign in the middle would do that? Is it because it closed off a function with an argument? Seems to be the case.

#### Newell Jensen (Apr 08 2023 at 08:28):

Seems that is how the $ works in general if that is the case. I had previously assumed it put all the end parenthesis at the very end.

#### Ruben Van de Velde (Apr 08 2023 at 08:32):

Yeah, the dollar sign is basically "function call, but wrap the rest of the expression in parentheses". Impossible to search for, sadly

#### Kevin Buzzard (Apr 08 2023 at 09:00):

Mario Carneiro said:

and for p = 2 the claim p < n# is false

The original claim is true because p < n so n>=3 so n# is a multiple of 6. But it's this sort of technical detail ("edge cases") which mathematicians are very keen to brush off as "needing no proof" and for which theorem provers demand the details. This is why I tried to come up with a more conceptual argument.

#### Kevin Buzzard (Apr 08 2023 at 09:05):

@Newell Jensen here's Yael's proof unpicked into Lean 4 tactic mode:

```
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.NumberTheory.Primorial
local notation x "#" => primorial x
open Finset
example (n p : Nat) (pp : Nat.Prime p) (hp : p < n) : p ∣ n# := by
apply dvd_prod_of_mem
rw [mem_filter]
refine ⟨?_, pp⟩
rw [mem_range]
rw [Nat.lt_succ_iff]
exact hp.le -- dot notation trick
```

When I was learning I found it far easier to write the tactic mode proof first and then, if I wanted the extra exercise, I'd trasnslate it into term mode. After you get better and get the hang of the `_`

tricks you find that you can write the term mode proof directly.

#### Newell Jensen (Apr 08 2023 at 09:08):

@Kevin Buzzard Yes, one step at a time. I think another thing limiting me is just me not knowing mathlib as well either. Takes time. Gotta put in the work, no other way around it.

#### Newell Jensen (Apr 08 2023 at 09:10):

And yes, fully agree with you about the details. It is this very reason that I am trying to learn Lean.

#### Kevin Buzzard (Apr 08 2023 at 09:15):

You *don't have to know mathlib*. You just have to know the underlying philosophy of mathlib. This is a really important lesson. Got a goal of the form `p ∈ range (n + 1)`

? Rewrite with a lemma called `mem_range`

or `mem_range_iff`

. It will be there. Got a goal of the form ` p ∈ filter Nat.Prime (range (n + 1))`

? Rewrite with a lemma called `mem_filter`

. You have to trust that the lemmas you want are there, and because this is what we're striving for, they often are.

Last updated: Dec 20 2023 at 11:08 UTC