[GOAL]
k n : ℕ
hk0 : k ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
rcases(one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)
[GOAL]
case inl
n : ℕ
hk0 : 1 ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
[PROOFSTEP]
rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩
[GOAL]
case inl.intro.intro
n : ℕ
hk0 : 1 ≠ 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
[PROOFSTEP]
exact ⟨p, hp, hnp, modEq_one⟩
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
let b := k * (n !)
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
have hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs :=
  by
  rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
  have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
  calc
    1 ≤ b - 1 := le_tsub_of_add_le_left hb
    _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs := sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
[PROOFSTEP]
rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
[GOAL]
case intro
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 1 < Int.natAbs (eval (↑b) (cyclotomic (k + 1) ℤ))
[PROOFSTEP]
have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
[GOAL]
case intro
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
hb : 2 ≤ b
⊢ 1 < Int.natAbs (eval (↑b) (cyclotomic (k + 1) ℤ))
[PROOFSTEP]
calc
  1 ≤ b - 1 := le_tsub_of_add_le_left hb
  _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs := sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
let p := minFac (eval (↑b) (cyclotomic k ℤ)).natAbs
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) :=
  by
  have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
  rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, ← Int.cast_ofNat, this, eval₂_hom,
    Int.coe_castRingHom, ZMod.int_cast_zmod_eq_zero_iff_dvd _ _]
  apply Int.dvd_natAbs.1
  exact_mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
⊢ IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
[PROOFSTEP]
have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
⊢ ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
[PROOFSTEP]
simp
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
this : ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
⊢ IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
[PROOFSTEP]
rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, ← Int.cast_ofNat, this, eval₂_hom,
  Int.coe_castRingHom, ZMod.int_cast_zmod_eq_zero_iff_dvd _ _]
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
this : ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ eval (↑b) (cyclotomic k ℤ)
[PROOFSTEP]
apply Int.dvd_natAbs.1
[GOAL]
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
this : ↑↑b = ↑(Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ ↑(Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
[PROOFSTEP]
exact_mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
have hpb : ¬p ∣ b := hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm
[GOAL]
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
refine' ⟨p, hprime.1, not_le.1 fun habs => _, _⟩
[GOAL]
case inr.refine'_1
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
habs : p ≤ n
⊢ False
[PROOFSTEP]
exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
have hdiv : orderOf (b : ZMod p) ∣ p - 1 := ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
haveI : NeZero (k : ZMod p) := NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this : NeZero ↑k
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
rw [← this] at hdiv 
[GOAL]
case inr.refine'_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < Int.natAbs (eval (↑b) (cyclotomic k ℤ))
p : ℕ := minFac (Int.natAbs (eval (↑b) (cyclotomic k ℤ)))
hprime : Fact (Prime p)
hroot : IsRoot (cyclotomic k (ZMod p)) (↑(castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : k ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]
[PROOFSTEP]
exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm
[GOAL]
k : ℕ
hk0 : k ≠ 0
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]
[PROOFSTEP]
refine' frequently_atTop.2 fun n => _
[GOAL]
k : ℕ
hk0 : k ≠ 0
n : ℕ
⊢ ∃ b, b ≥ n ∧ Prime b ∧ b ≡ 1 [MOD k]
[PROOFSTEP]
obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0
[GOAL]
case intro
k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b, b ≥ n ∧ Prime b ∧ b ≡ 1 [MOD k]
[PROOFSTEP]
exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩
