p : ℕ
w : 1 < p
p' : ℕ := p - 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
p : ℕ
w : 1 < p
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
let p' := p - 2
p : ℕ
w : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
p : ℕ
w : 1 < p
p' : ℕ := p - 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
have z : p = p' + 2 := (tsub_eq_iff_eq_add_of_le w.nat_succ_le).mp rfl
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
p : ℕ
w : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
have w : 1 < p' + 2 := Nat.lt_of_sub_eq_succ rfl
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ ¬Nat.Prime (mersenne p) → ¬LucasLehmerTest p
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
contrapose
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne p)
t : LucasLehmerTest p
⊢ False
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ ¬Nat.Prime (mersenne p) → ¬LucasLehmerTest p
intro a t
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest p
⊢ False
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne p)
t : LucasLehmerTest p
⊢ False
rw [z] at a
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
⊢ False
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest p
⊢ False
rw [z] at t
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
⊢ False
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
⊢ False
have h₁ := order_ineq p' t
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : Nat.minFac (mersenne (p' + 2)) ^ 2 ≤ mersenne (p' + 2)
⊢ False
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
⊢ False
have h₂ := Nat.minFac_sq_le_self (mersenne_pos (Nat.lt_of_succ_lt w)) a
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : Nat.minFac (mersenne (p' + 2)) ^ 2 ≤ mersenne (p' + 2)
h : 2 ^ (p' + 2) < mersenne (p' + 2)
⊢ False
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : Nat.minFac (mersenne (p' + 2)) ^ 2 ≤ mersenne (p' + 2)
⊢ False
have h := lt_of_lt_of_le h₁ h₂
no goals
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : Nat.minFac (mersenne (p' + 2)) ^ 2 ≤ mersenne (p' + 2)
h : 2 ^ (p' + 2) < mersenne (p' + 2)
⊢ False
exact not_lt_of_ge (Nat.sub_le _ _) h