# Zulip Chat Archive

## 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,
{
by_contradiction h',
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
by_contradiction n_comp,
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
by_contradiction H,
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