## Stream: new members

### Topic: Quickest way to resolve exponent inequalities

#### Gareth Ma (Jan 22 2023 at 23:14):

Hi, it's me again :P I am working on properties of Mersenne primes i.e. primes in the form of 2^n - 1. One property is that n must be a prime. While working on it, I have to deal with a lot of 2^x, and combined with the subtraction over natural numbers, it is causing me quite a lot of pain :tear: Is that normal? As in, is there any simpler way to prove that 2 <= d => 1 < 2^d - 1 directly, whether through a simp or some other method?

Here is my code, it's all quite elementary number theory, so hope someone can take a look, especially the parts where I marked with TODO, such as stating 4 - 1 <= 2^d - 1 as a lemma. Thanks!!

-- Thank you to Kevin Buzzard, Niels Voss and Yaël Dillies for helping with this!
theorem mersenne_div {m n : ℕ} (h : m ∣ n) : mersenne m ∣ mersenne n :=
begin
rcases h with ⟨k, rfl⟩,
simpa only [mersenne, pow_mul, one_pow] using nat_sub_dvd_pow_sub_pow _ 1 _,
end

-- 2^n - 1 is Mersenne prime implies n is prime
theorem mersenne_theorem {n : ℕ} (h : nat.prime (mersenne n)) : nat.prime n :=
begin
-- Auxillary lemma
have two_le_n : 2 ≤ n,
{
push_neg at h',

-- TODO: Simplify this, seems repetitive
cases nat.lt_succ_iff.1 h' with _ h',
{ simp [mersenne, nat.not_prime_one] at h, exact h, },
{ simp [mersenne, nat.eq_zero_of_le_zero h', nat.not_prime_zero] at h, exact h, }
},

-- Assume n is composite
rcases nat.exists_dvd_of_not_prime _ n_comp with ⟨d, d_div, d_ne_one, d_ne_n⟩,

-- TODO: Remove these...
have d_ne_zero : d ≠ 0,
{ by_contradiction, rw h at d_div, rw zero_dvd_iff at d_div, linarith, },
have one_le_pow_two_d : 1 ≤ 2 ^ d,
{ apply nat.one_le_pow, omega, },
have two_le_d : 2 ≤ d,
{ cases d, omega, cases d; omega,},
have four_sub_one_le_pow_two_sub_one: 4 - 1 ≤ 2 ^ d - 1,
{
change 2 ^ 2 - 1 ≤ 2 ^ d - 1,
rw nat.sub_le_sub_iff_right,
exact pow_le_pow (by linarith) two_le_d,
exact nat.one_le_pow d 2 zero_lt_two,
},

-- Then mersenne n is not prime
rcases mersenne_div d_div with ⟨md, hmd⟩,
have : ¬nat.prime (mersenne n),
{
apply nat.not_prime_mul' hmd.symm,
{
unfold mersenne,

-- TODO: Remove this...
calc
1 < 4 - 1 : by simp
... ≤ 2 ^ d - 1 : by { simp [four_sub_one_le_pow_two_sub_one] },
},
{
-- Ruling out cases where (mersenne n / mersenne d) <= 2
push_neg at H,
cases md,
{ simp [hmd] at h, exact nat.not_prime_zero h, },
{
unfold mersenne at hmd,
rw [nat.succ_le_iff, nat.lt_one_iff] at H,
simp [H] at hmd,
-- TODO: Here I am proving 2 ^ n - 1 = 2 ^ d - 1 => n = d ... Is there better way?
rw [tsub_left_inj (nat.one_le_pow n 2 zero_lt_two) one_le_pow_two_d, eq_comm] at hmd,
exact d_ne_n (nat.pow_right_injective rfl.ge hmd),
}
}
},

exact this h,
exact two_le_n,
end


#### Yaël Dillies (Jan 22 2023 at 23:38):

You should probably work over int to use the proper subtraction.

#### Yaël Dillies (Jan 22 2023 at 23:39):

Subtraction on nat is very well behaved from the order theoretic point of view, not so much from the algebraic one.

#### Gareth Ma (Jan 22 2023 at 23:44):

The thing is mersenne is currently defined as def mersenne (p : ℕ) : ℕ := 2^p - 1, and it is used everywhere in the lucas_* code. Should I change that? Or just cast to the int's and work on that?

#### Kevin Buzzard (Jan 23 2023 at 01:00):

Just cast to int and prove mersenne n as integer is 2^n-1 with integer subtraction. Natural subtraction is awful I agree.

#### Yaël Dillies (Jan 23 2023 at 07:30):

If that makes you feel better, you could define int.mersenne and show casting nat.mersenne to int gives you int.mersenne.

Last updated: Dec 20 2023 at 11:08 UTC