[GOAL]
p : ℕ
h : 0 < p
⊢ 0 < mersenne p
[PROOFSTEP]
dsimp [mersenne]
[GOAL]
p : ℕ
h : 0 < p
⊢ 0 < 2 ^ p - 1
[PROOFSTEP]
calc
  0 < 2 ^ 1 - 1 := by norm_num
  _ ≤ 2 ^ p - 1 := Nat.sub_le_sub_right (Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) h) 1
[GOAL]
p : ℕ
h : 0 < p
⊢ 0 < 2 ^ 1 - 1
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
hp : 1 < p
⊢ 1 + 1 = 2 ^ 1
[PROOFSTEP]
rw [one_add_one_eq_two, pow_one]
[GOAL]
k : ℕ
⊢ mersenne k + 1 = 2 ^ k
[PROOFSTEP]
rw [mersenne, tsub_add_cancel_of_le]
[GOAL]
k : ℕ
⊢ 1 ≤ 2 ^ k
[PROOFSTEP]
exact one_le_pow_of_one_le (by norm_num) k
[GOAL]
k : ℕ
⊢ 1 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
hp : 0 < p
⊢ 1 < 2 ^ p
[PROOFSTEP]
exact_mod_cast Nat.one_lt_two_pow p hp
[GOAL]
p : ℕ
w : 0 < p
i : ℕ
⊢ 0 ≤ sMod p i
[PROOFSTEP]
cases i
[GOAL]
case zero
p : ℕ
w : 0 < p
⊢ 0 ≤ sMod p zero
[PROOFSTEP]
dsimp [sMod]
[GOAL]
case succ
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 0 ≤ sMod p (succ n✝)
[PROOFSTEP]
dsimp [sMod]
[GOAL]
case zero
p : ℕ
w : 0 < p
⊢ 0 ≤ 4 % (2 ^ p - 1)
[PROOFSTEP]
exact sup_eq_right.mp rfl
[GOAL]
case succ
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)
[PROOFSTEP]
apply Int.emod_nonneg
[GOAL]
case succ.a
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 2 ^ p - 1 ≠ 0
[PROOFSTEP]
exact mersenne_int_ne_zero p w
[GOAL]
p i : ℕ
⊢ sMod p i % (2 ^ p - 1) = sMod p i
[PROOFSTEP]
cases i
[GOAL]
case zero
p : ℕ
⊢ sMod p zero % (2 ^ p - 1) = sMod p zero
[PROOFSTEP]
simp [sMod]
[GOAL]
case succ
p n✝ : ℕ
⊢ sMod p (succ n✝) % (2 ^ p - 1) = sMod p (succ n✝)
[PROOFSTEP]
simp [sMod]
[GOAL]
p : ℕ
w : 0 < p
i : ℕ
⊢ sMod p i < 2 ^ p - 1
[PROOFSTEP]
rw [← sMod_mod]
[GOAL]
p : ℕ
w : 0 < p
i : ℕ
⊢ sMod p i % (2 ^ p - 1) < 2 ^ p - 1
[PROOFSTEP]
refine (Int.emod_lt _ (mersenne_int_ne_zero p w)).trans_eq ?_
[GOAL]
p : ℕ
w : 0 < p
i : ℕ
⊢ |2 ^ p - 1| = 2 ^ p - 1
[PROOFSTEP]
exact abs_of_nonneg (mersenne_int_pos w).le
[GOAL]
p' i : ℕ
⊢ sZMod (p' + 2) i = ↑(s i)
[PROOFSTEP]
induction' i with i ih
[GOAL]
case zero
p' : ℕ
⊢ sZMod (p' + 2) zero = ↑(s zero)
[PROOFSTEP]
dsimp [s, sZMod]
[GOAL]
case zero
p' : ℕ
⊢ 4 = ↑4
[PROOFSTEP]
norm_num
[GOAL]
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ sZMod (p' + 2) (succ i) = ↑(s (succ i))
[PROOFSTEP]
push_cast [s, sZMod, ih]
[GOAL]
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
[PROOFSTEP]
rfl
[GOAL]
b p : ℕ
w : 0 < b
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1
[PROOFSTEP]
have : 1 ≤ b ^ p := Nat.one_le_pow p b w
[GOAL]
b p : ℕ
w : 0 < b
this : 1 ≤ b ^ p
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
p i : ℕ
⊢ sZMod p i = ↑(sMod p i)
[PROOFSTEP]
induction i
[GOAL]
case zero
p : ℕ
⊢ sZMod p zero = ↑(sMod p zero)
[PROOFSTEP]
push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]
[GOAL]
case succ
p n✝ : ℕ
n_ih✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ sZMod p (succ n✝) = ↑(sMod p (succ n✝))
[PROOFSTEP]
push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]
[GOAL]
case zero
p : ℕ
⊢ 4 = 4
[PROOFSTEP]
rfl
[GOAL]
case succ
p n✝ : ℕ
n_ih✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ ↑(sMod p n✝) ^ 2 - 2 = ↑(sMod p n✝) ^ 2 - 2
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
w : 1 < p
⊢ lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0
[PROOFSTEP]
dsimp [lucasLehmerResidue]
[GOAL]
p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
[PROOFSTEP]
rw [sZMod_eq_sMod p]
[GOAL]
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0
[PROOFSTEP]
simp [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h 
[GOAL]
case mp
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) = 0
[PROOFSTEP]
apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h
[GOAL]
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ 0 ≤ sMod p (p - 2)
[PROOFSTEP]
clear h
[GOAL]
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) < 2 ^ p - 1
[PROOFSTEP]
clear h
[GOAL]
p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)
[PROOFSTEP]
apply sMod_nonneg _ (Nat.lt_of_succ_lt w)
[GOAL]
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1
[PROOFSTEP]
exact sMod_lt _ (Nat.lt_of_succ_lt w) (p - 2)
[GOAL]
case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑(sMod p (p - 2)) = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑0 = 0
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
x y : X q
h₁ : x.fst = y.fst
h₂ : x.snd = y.snd
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk
q : ℕ+
y : X q
fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝, snd✝).fst = y.fst
h₂ : (fst✝, snd✝).snd = y.snd
⊢ (fst✝, snd✝) = y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
q : ℕ+
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
h₂ : (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
[PROOFSTEP]
congr
[GOAL]
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x y z : X q
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x y z : X q
⊢ (x * y * z).fst = (x * (y * z)).fst
[PROOFSTEP]
dsimp
[GOAL]
case h₂
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x y z : X q
⊢ (x * y * z).snd = (x * (y * z)).snd
[PROOFSTEP]
dsimp
[GOAL]
case h₁
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x y z : X q
⊢ (x.fst * y.fst + 3 * x.snd * y.snd) * z.fst + 3 * (x.fst * y.snd + x.snd * y.fst) * z.snd =
    x.fst * (y.fst * z.fst + 3 * y.snd * z.snd) + 3 * x.snd * (y.fst * z.snd + y.snd * z.fst)
[PROOFSTEP]
ring
[GOAL]
case h₂
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x y z : X q
⊢ (x.fst * y.fst + 3 * x.snd * y.snd) * z.snd + (x.fst * y.snd + x.snd * y.fst) * z.fst =
    x.fst * (y.fst * z.snd + y.snd * z.fst) + x.snd * (y.fst * z.fst + 3 * y.snd * z.snd)
[PROOFSTEP]
ring
[GOAL]
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x : X q
⊢ 1 * x = x
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x : X q
⊢ (1 * x).fst = x.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x : X q
⊢ (1 * x).snd = x.snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x : X q
⊢ x * 1 = x
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x : X q
⊢ (x * 1).fst = x.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝¹ : Mul (X q) := inferInstanceAs (Mul (X q))
src✝ : One (X q) := inferInstanceAs (One (X q))
x : X q
⊢ (x * 1).snd = x.snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
⊢ (NatCast.natCast 0).fst = 0.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
⊢ (NatCast.natCast 0).snd = 0.snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
x✝ : ℕ
⊢ (NatCast.natCast (x✝ + 1)).fst = (NatCast.natCast x✝ + 1).fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
x✝ : ℕ
⊢ (NatCast.natCast (x✝ + 1)).snd = (NatCast.natCast x✝ + 1).snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
n : ℕ
⊢ IntCast.intCast ↑n = ↑n
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
n : ℕ
⊢ (IntCast.intCast ↑n).fst = (↑n).fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
n : ℕ
⊢ (IntCast.intCast ↑n).snd = (↑n).snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
n : ℕ
⊢ (IntCast.intCast (Int.negSucc n)).fst = (-↑(n + 1)).fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝² : Monoid (X q) := inferInstanceAs (Monoid (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : NatCast (X q) := inferInstanceAs (NatCast (X q))
n : ℕ
⊢ (IntCast.intCast (Int.negSucc n)).snd = (-↑(n + 1)).snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
x y z : X q
⊢ x * (y + z) = x * y + x * z
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
x y z : X q
⊢ (x * (y + z)).fst = (x * y + x * z).fst
[PROOFSTEP]
dsimp
[GOAL]
case h₂
q : ℕ+
x y z : X q
⊢ (x * (y + z)).snd = (x * y + x * z).snd
[PROOFSTEP]
dsimp
[GOAL]
case h₁
q : ℕ+
x y z : X q
⊢ x.fst * (y.fst + z.fst) + 3 * x.snd * (y.snd + z.snd) =
    x.fst * y.fst + 3 * x.snd * y.snd + (x.fst * z.fst + 3 * x.snd * z.snd)
[PROOFSTEP]
ring
[GOAL]
case h₂
q : ℕ+
x y z : X q
⊢ x.fst * (y.snd + z.snd) + x.snd * (y.fst + z.fst) = x.fst * y.snd + x.snd * y.fst + (x.fst * z.snd + x.snd * z.fst)
[PROOFSTEP]
ring
[GOAL]
q : ℕ+
x y z : X q
⊢ (x + y) * z = x * z + y * z
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
x y z : X q
⊢ ((x + y) * z).fst = (x * z + y * z).fst
[PROOFSTEP]
dsimp
[GOAL]
case h₂
q : ℕ+
x y z : X q
⊢ ((x + y) * z).snd = (x * z + y * z).snd
[PROOFSTEP]
dsimp
[GOAL]
case h₁
q : ℕ+
x y z : X q
⊢ (x.fst + y.fst) * z.fst + 3 * (x.snd + y.snd) * z.snd =
    x.fst * z.fst + 3 * x.snd * z.snd + (y.fst * z.fst + 3 * y.snd * z.snd)
[PROOFSTEP]
ring
[GOAL]
case h₂
q : ℕ+
x y z : X q
⊢ (x.fst + y.fst) * z.snd + (x.snd + y.snd) * z.fst = x.fst * z.snd + x.snd * z.fst + (y.fst * z.snd + y.snd * z.fst)
[PROOFSTEP]
ring
[GOAL]
q : ℕ+
src✝² : AddGroupWithOne (X q) := inferInstanceAs (AddGroupWithOne (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : Monoid (X q) := inferInstanceAs (Monoid (X q))
x✝ : X q
⊢ 0 * x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝² : AddGroupWithOne (X q) := inferInstanceAs (AddGroupWithOne (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : Monoid (X q) := inferInstanceAs (Monoid (X q))
x✝ : X q
⊢ (0 * x✝).fst = 0.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝² : AddGroupWithOne (X q) := inferInstanceAs (AddGroupWithOne (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : Monoid (X q) := inferInstanceAs (Monoid (X q))
x✝ : X q
⊢ (0 * x✝).snd = 0.snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝² : AddGroupWithOne (X q) := inferInstanceAs (AddGroupWithOne (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : Monoid (X q) := inferInstanceAs (Monoid (X q))
x✝ : X q
⊢ x✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝² : AddGroupWithOne (X q) := inferInstanceAs (AddGroupWithOne (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : Monoid (X q) := inferInstanceAs (Monoid (X q))
x✝ : X q
⊢ (x✝ * 0).fst = 0.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
src✝² : AddGroupWithOne (X q) := inferInstanceAs (AddGroupWithOne (X q))
src✝¹ : AddCommGroup (X q) := inferInstanceAs (AddCommGroup (X q))
src✝ : Monoid (X q) := inferInstanceAs (Monoid (X q))
x✝ : X q
⊢ (x✝ * 0).snd = 0.snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
src✝ : Ring (X q) := inferInstanceAs (Ring (X q))
x✝¹ x✝ : X q
⊢ x✝¹ * x✝ = x✝ * x✝¹
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
src✝ : Ring (X q) := inferInstanceAs (Ring (X q))
x✝¹ x✝ : X q
⊢ (x✝¹ * x✝).fst = (x✝ * x✝¹).fst
[PROOFSTEP]
dsimp
[GOAL]
case h₂
q : ℕ+
src✝ : Ring (X q) := inferInstanceAs (Ring (X q))
x✝¹ x✝ : X q
⊢ (x✝¹ * x✝).snd = (x✝ * x✝¹).snd
[PROOFSTEP]
dsimp
[GOAL]
case h₁
q : ℕ+
src✝ : Ring (X q) := inferInstanceAs (Ring (X q))
x✝¹ x✝ : X q
⊢ x✝¹.fst * x✝.fst + 3 * x✝¹.snd * x✝.snd = x✝.fst * x✝¹.fst + 3 * x✝.snd * x✝¹.snd
[PROOFSTEP]
ring
[GOAL]
case h₂
q : ℕ+
src✝ : Ring (X q) := inferInstanceAs (Ring (X q))
x✝¹ x✝ : X q
⊢ x✝¹.fst * x✝.snd + x✝¹.snd * x✝.fst = x✝.fst * x✝¹.snd + x✝.snd * x✝¹.fst
[PROOFSTEP]
ring
[GOAL]
q : ℕ+
n m : ℤ
⊢ ↑(n * m) = ↑n * ↑m
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
n m : ℤ
⊢ (↑(n * m)).fst = (↑n * ↑m).fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
n m : ℤ
⊢ (↑(n * m)).snd = (↑n * ↑m).snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
n : ℕ
⊢ ↑↑n = ↑n
[PROOFSTEP]
ext
[GOAL]
case h₁
q : ℕ+
n : ℕ
⊢ (↑↑n).fst = (↑n).fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q : ℕ+
n : ℕ
⊢ (↑↑n).snd = (↑n).snd
[PROOFSTEP]
simp
[GOAL]
q : ℕ+
⊢ Fintype.card (X q) = ↑q ^ 2
[PROOFSTEP]
dsimp [X]
[GOAL]
q : ℕ+
⊢ Fintype.card (ZMod ↑q × ZMod ↑q) = ↑q ^ 2
[PROOFSTEP]
rw [Fintype.card_prod, ZMod.card q, sq]
[GOAL]
q : ℕ+
w : 1 < q
⊢ Fintype.card (X q)ˣ < ↑q ^ 2
[PROOFSTEP]
have : Fact (1 < (q : ℕ)) := ⟨w⟩
[GOAL]
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ Fintype.card (X q)ˣ < ↑q ^ 2
[PROOFSTEP]
convert card_units_lt (X q)
[GOAL]
case h.e'_4
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ ↑q ^ 2 = Fintype.card (X q)
[PROOFSTEP]
rw [card_eq]
[GOAL]
q✝ q : ℕ+
⊢ ω * ωb = 1
[PROOFSTEP]
dsimp [ω, ωb]
[GOAL]
q✝ q : ℕ+
⊢ (2, 1) * (2, -1) = 1
[PROOFSTEP]
ext
[GOAL]
case h₁
q✝ q : ℕ+
⊢ ((2, 1) * (2, -1)).fst = 1.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
q✝ q : ℕ+
⊢ ((2, 1) * (2, -1)).snd = 1.snd
[PROOFSTEP]
simp
[GOAL]
case h₁
q✝ q : ℕ+
⊢ 2 * 2 + -3 = 1
[PROOFSTEP]
ring
[GOAL]
q✝ q : ℕ+
⊢ ωb * ω = 1
[PROOFSTEP]
rw [mul_comm, ω_mul_ωb]
[GOAL]
q : ℕ+
i : ℕ
⊢ ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
[PROOFSTEP]
induction' i with i ih
[GOAL]
case zero
q : ℕ+
⊢ ↑(s zero) = ω ^ 2 ^ zero + ωb ^ 2 ^ zero
[PROOFSTEP]
dsimp [s, ω, ωb]
[GOAL]
case zero
q : ℕ+
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1
[PROOFSTEP]
ext
[GOAL]
case zero.h₁
q : ℕ+
⊢ (↑4).fst = ((2, 1) ^ 1 + (2, -1) ^ 1).fst
[PROOFSTEP]
norm_num
[GOAL]
case zero.h₂
q : ℕ+
⊢ (↑4).snd = ((2, 1) ^ 1 + (2, -1) ^ 1).snd
[PROOFSTEP]
norm_num
[GOAL]
case succ
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s (succ i)) = ω ^ 2 ^ succ i + ωb ^ 2 ^ succ i
[PROOFSTEP]
calc
  (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
  _ = (s i : X q) ^ 2 - 2 := by push_cast ; rfl
  _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
  _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
  _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel]
  _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ']
[GOAL]
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i ^ 2 - 2) = ↑(s i) ^ 2 - 2
[PROOFSTEP]
push_cast
[GOAL]
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
[PROOFSTEP]
rfl
[GOAL]
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2
[PROOFSTEP]
rw [ih]
[GOAL]
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2
[PROOFSTEP]
ring
[GOAL]
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2
[PROOFSTEP]
rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel]
[GOAL]
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)
[PROOFSTEP]
rw [← pow_mul, ← pow_mul, _root_.pow_succ']
[GOAL]
p' : ℕ
⊢ 2 < q (p' + 2)
[PROOFSTEP]
refine (minFac_prime (one_lt_mersenne ?_).ne').two_le.lt_of_ne' ?_
[GOAL]
case refine_1
p' : ℕ
⊢ 1 < p' + 2
[PROOFSTEP]
exact le_add_left _ _
[GOAL]
case refine_2
p' : ℕ
⊢ minFac (mersenne (p' + 2)) ≠ 2
[PROOFSTEP]
rw [Ne.def, minFac_eq_two_iff, mersenne, Nat.pow_succ']
[GOAL]
case refine_2
p' : ℕ
⊢ ¬2 ∣ 2 * 2 ^ (p' + 1) - 1
[PROOFSTEP]
exact Nat.two_not_dvd_two_mul_sub_one (Nat.one_le_two_pow _)
[GOAL]
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
dsimp [lucasLehmerResidue] at h 
[GOAL]
p' : ℕ
h : sZMod (p' + 2) (p' + 2 - 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
rw [sZMod_eq_s p'] at h 
[GOAL]
p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
simp [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h 
[GOAL]
p' : ℕ
h : 2 ^ (p' + 2) - 1 ∣ s p'
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
cases' h with k h
[GOAL]
case intro
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
use k
[GOAL]
case h
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h
[GOAL]
case h
p' : ℕ
k : ℤ
h : (fun n => ↑n) (s p') = (fun n => ↑n) ((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
dsimp at h 
[GOAL]
case h
p' : ℕ
k : ℤ
h : ↑(s p') = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
rw [closed_form] at h 
[GOAL]
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' + ωb ^ 2 ^ p' = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
replace h := congr_arg (fun x => ω ^ 2 ^ p' * x) h
[GOAL]
case h
p' : ℕ
k : ℤ
h : (fun x => ω ^ 2 ^ p' * x) (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = (fun x => ω ^ 2 ^ p' * x) ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
dsimp at h 
[GOAL]
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
have t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1) := by ring
[GOAL]
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
⊢ 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
[PROOFSTEP]
ring
[GOAL]
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h 
[GOAL]
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
rw [mul_comm, coe_mul] at h 
[GOAL]
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑(2 ^ (p' + 2) - 1) * ↑k * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
rw [mul_comm _ (k : X (q (p' + 2)))] at h 
[GOAL]
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
replace h := eq_sub_of_add_eq h
[GOAL]
case h
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide)
[GOAL]
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case h
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
this : 1 ≤ 2 ^ (p' + 2)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
[PROOFSTEP]
exact_mod_cast h
[GOAL]
p : ℕ
⊢ ↑(mersenne p) = 0
[PROOFSTEP]
ext
[GOAL]
case h₁
p : ℕ
⊢ (↑(mersenne p)).fst = 0.fst
[PROOFSTEP]
simp [mersenne, q, ZMod.nat_cast_zmod_eq_zero_iff_dvd, -pow_pos]
[GOAL]
case h₂
p : ℕ
⊢ (↑(mersenne p)).snd = 0.snd
[PROOFSTEP]
simp [mersenne, q, ZMod.nat_cast_zmod_eq_zero_iff_dvd, -pow_pos]
[GOAL]
case h₁
p : ℕ
⊢ minFac (2 ^ p - 1) ∣ 2 ^ p - 1
[PROOFSTEP]
apply Nat.minFac_dvd
[GOAL]
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 1) = -1
[PROOFSTEP]
cases' ω_pow_formula p' h with k w
[GOAL]
case intro
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1
[PROOFSTEP]
rw [mersenne_coe_X] at w 
[GOAL]
case intro
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1
[PROOFSTEP]
simpa using w
[GOAL]
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 2) = (ω ^ 2 ^ (p' + 1)) ^ 2
[PROOFSTEP]
rw [← pow_mul, ← Nat.pow_succ]
[GOAL]
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (ω ^ 2 ^ (p' + 1)) ^ 2 = (-1) ^ 2
[PROOFSTEP]
rw [ω_pow_eq_neg_one p' h]
[GOAL]
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (-1) ^ 2 = 1
[PROOFSTEP]
simp
[GOAL]
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) = 2 ^ (p' + 2)
[PROOFSTEP]
apply Nat.eq_prime_pow_of_dvd_least_prime_pow
[GOAL]
case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2
[PROOFSTEP]
exact Nat.prime_two
[GOAL]
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
[PROOFSTEP]
intro o
[GOAL]
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
⊢ False
[PROOFSTEP]
have ω_pow := orderOf_dvd_iff_pow_eq_one.1 o
[GOAL]
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ωUnit (p' + 2) ^ 2 ^ (p' + 1) = 1
⊢ False
[PROOFSTEP]
replace ω_pow := congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) ω_pow
[GOAL]
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ↑(Units.coeHom (X (q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = ↑(Units.coeHom (X (q (p' + 2)))) 1
⊢ False
[PROOFSTEP]
simp at ω_pow 
[GOAL]
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
⊢ False
[PROOFSTEP]
have h : (1 : ZMod (q (p' + 2))) = -1 := congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
[GOAL]
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
⊢ False
[PROOFSTEP]
haveI : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
[GOAL]
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
this : Fact (2 < ↑(q (p' + 2)))
⊢ False
[PROOFSTEP]
apply ZMod.neg_one_ne_one h.symm
[GOAL]
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)
[PROOFSTEP]
apply orderOf_dvd_iff_pow_eq_one.2
[GOAL]
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1) = 1
[PROOFSTEP]
apply Units.ext
[GOAL]
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1)) = ↑1
[PROOFSTEP]
push_cast
[GOAL]
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2)) ^ 2 ^ (p' + 1 + 1) = 1
[PROOFSTEP]
exact ω_pow_eq_one p' h
[GOAL]
p : ℕ
w : 1 < p
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
[PROOFSTEP]
let p' := p - 2
[GOAL]
p : ℕ
w : 1 < p
p' : ℕ := p - 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
[PROOFSTEP]
have z : p = p' + 2 := (tsub_eq_iff_eq_add_of_le w.nat_succ_le).mp rfl
[GOAL]
p : ℕ
w : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
[PROOFSTEP]
have w : 1 < p' + 2 := Nat.lt_of_sub_eq_succ rfl
[GOAL]
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)
[PROOFSTEP]
contrapose
[GOAL]
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ ¬Nat.Prime (mersenne p) → ¬LucasLehmerTest p
[PROOFSTEP]
intro a t
[GOAL]
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne p)
t : LucasLehmerTest p
⊢ False
[PROOFSTEP]
rw [z] at a 
[GOAL]
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
[PROOFSTEP]
rw [z] at t 
[GOAL]
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
[PROOFSTEP]
have h₁ := order_ineq p' t
[GOAL]
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
[PROOFSTEP]
have h₂ := Nat.minFac_sq_le_self (mersenne_pos (Nat.lt_of_succ_lt w)) a
[GOAL]
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
[PROOFSTEP]
have h := lt_of_lt_of_le h₁ h₂
[GOAL]
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
[PROOFSTEP]
exact not_lt_of_ge (Nat.sub_le _ _) h
[GOAL]
p k : ℕ
hp : 2 ≤ p
⊢ ↑(sMod' (2 ^ p - 1) k) = sMod p k
[PROOFSTEP]
have h1 :=
  calc
    4 = 2 ^ 2 := by norm_num
    _ ≤ 2 ^ p := Nat.pow_le_pow_of_le_right (by norm_num) hp
[GOAL]
p k : ℕ
hp : 2 ≤ p
⊢ 4 = 2 ^ 2
[PROOFSTEP]
norm_num
[GOAL]
p k : ℕ
hp : 2 ≤ p
⊢ 2 > 0
[PROOFSTEP]
norm_num
[GOAL]
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
⊢ ↑(sMod' (2 ^ p - 1) k) = sMod p k
[PROOFSTEP]
have h2 : 1 ≤ 2 ^ p := by linarith
[GOAL]
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
⊢ 1 ≤ 2 ^ p
[PROOFSTEP]
linarith
[GOAL]
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sMod' (2 ^ p - 1) k) = sMod p k
[PROOFSTEP]
induction k with
| zero =>
  rw [sMod', sMod, Int.ofNat_emod]
  simp [h2]
| succ k ih =>
  rw [sMod', sMod, ← ih]
  have h3 : 2 ≤ 2 ^ p - 1 := by
    zify [h2]
    calc
      (2 : Int) ≤ 4 - 1 := by norm_num
      _ ≤ 2 ^ p - 1 := by zify at h1 ; exact Int.sub_le_sub_right h1 _
  zify [h2, h3]
  rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc, Int.add_emod_self, ← sub_eq_add_neg]
[GOAL]
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sMod' (2 ^ p - 1) k) = sMod p k
[PROOFSTEP]
induction k with
| zero =>
  rw [sMod', sMod, Int.ofNat_emod]
  simp [h2]
| succ k ih =>
  rw [sMod', sMod, ← ih]
  have h3 : 2 ≤ 2 ^ p - 1 := by
    zify [h2]
    calc
      (2 : Int) ≤ 4 - 1 := by norm_num
      _ ≤ 2 ^ p - 1 := by zify at h1 ; exact Int.sub_le_sub_right h1 _
  zify [h2, h3]
  rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc, Int.add_emod_self, ← sub_eq_add_neg]
[GOAL]
case zero
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sMod' (2 ^ p - 1) Nat.zero) = sMod p Nat.zero
[PROOFSTEP]

| zero =>
  rw [sMod', sMod, Int.ofNat_emod]
  simp [h2]
[GOAL]
case zero
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sMod' (2 ^ p - 1) Nat.zero) = sMod p Nat.zero
[PROOFSTEP]
rw [sMod', sMod, Int.ofNat_emod]
[GOAL]
case zero
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑4 % ↑(2 ^ p - 1) = 4 % (2 ^ p - 1)
[PROOFSTEP]
simp [h2]
[GOAL]
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ ↑(sMod' (2 ^ p - 1) (Nat.succ k)) = sMod p (Nat.succ k)
[PROOFSTEP]

| succ k ih =>
  rw [sMod', sMod, ← ih]
  have h3 : 2 ≤ 2 ^ p - 1 := by
    zify [h2]
    calc
      (2 : Int) ≤ 4 - 1 := by norm_num
      _ ≤ 2 ^ p - 1 := by zify at h1 ; exact Int.sub_le_sub_right h1 _
  zify [h2, h3]
  rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc, Int.add_emod_self, ← sub_eq_add_neg]
[GOAL]
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ ↑(sMod' (2 ^ p - 1) (Nat.succ k)) = sMod p (Nat.succ k)
[PROOFSTEP]
rw [sMod', sMod, ← ih]
[GOAL]
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ ↑((sMod' (2 ^ p - 1) k ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1)) = (↑(sMod' (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)
[PROOFSTEP]
have h3 : 2 ≤ 2 ^ p - 1 := by
  zify [h2]
  calc
    (2 : Int) ≤ 4 - 1 := by norm_num
    _ ≤ 2 ^ p - 1 := by zify at h1 ; exact Int.sub_le_sub_right h1 _
[GOAL]
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ 2 ≤ 2 ^ p - 1
[PROOFSTEP]
zify [h2]
[GOAL]
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ 2 ≤ 2 ^ p - 1
[PROOFSTEP]
calc
  (2 : Int) ≤ 4 - 1 := by norm_num
  _ ≤ 2 ^ p - 1 := by zify at h1 ; exact Int.sub_le_sub_right h1 _
[GOAL]
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ 2 ≤ 4 - 1
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
⊢ 4 - 1 ≤ 2 ^ p - 1
[PROOFSTEP]
zify at h1 
[GOAL]
p : ℕ
hp : 2 ≤ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
h1 : 4 ≤ 2 ^ p
⊢ 4 - 1 ≤ 2 ^ p - 1
[PROOFSTEP]
exact Int.sub_le_sub_right h1 _
[GOAL]
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
h3 : 2 ≤ 2 ^ p - 1
⊢ ↑((sMod' (2 ^ p - 1) k ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1)) = (↑(sMod' (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)
[PROOFSTEP]
zify [h2, h3]
[GOAL]
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sMod' (2 ^ p - 1) k) = sMod p k
h3 : 2 ≤ 2 ^ p - 1
⊢ (↑(sMod' (2 ^ p - 1) k) ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1) = (↑(sMod' (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)
[PROOFSTEP]
rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc, Int.add_emod_self, ← sub_eq_add_neg]
[GOAL]
p : ℕ
hp : Nat.blt 1 p = true
h : sMod' (2 ^ p - 1) (p - 2) = 0
⊢ LucasLehmerTest p
[PROOFSTEP]
rw [Nat.blt_eq] at hp 
[GOAL]
p : ℕ
hp : 1 < p
h : sMod' (2 ^ p - 1) (p - 2) = 0
⊢ LucasLehmerTest p
[PROOFSTEP]
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sMod'_eq_sMod p _ hp, h]
[GOAL]
p : ℕ
hp : 1 < p
h : sMod' (2 ^ p - 1) (p - 2) = 0
⊢ ↑0 = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sMod' (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p
[PROOFSTEP]
rw [Nat.blt_eq] at hp 
[GOAL]
p : ℕ
hp : 1 < p
h : Nat.ble 1 (sMod' (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p
[PROOFSTEP]
rw [Nat.ble_eq, Nat.succ_le, Nat.pos_iff_ne_zero] at h 
[GOAL]
p : ℕ
hp : 1 < p
h : sMod' (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬LucasLehmerTest p
[PROOFSTEP]
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sMod'_eq_sMod p _ hp]
[GOAL]
p : ℕ
hp : 1 < p
h : sMod' (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sMod' (2 ^ p - 1) (p - 2)) = 0
[PROOFSTEP]
simpa using h
[GOAL]
n k : ℕ
⊢ 1 * (k / 2 ^ n) + k % 2 ^ n = k / 2 ^ n + k % 2 ^ n
[PROOFSTEP]
rw [one_mul]
