## 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):

docs#nat.bertrand

#### 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

#### 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