English
If n passes Fermat's probable prime test to base b and n,b ≥ 1, then gcd(n,b)=1.
Русский
Если n удовлетворяет тесту на вероятность простоты по основанию b и n,b ≥ 1, то gcd(n,b)=1.
LaTeX
$$Nat.Coprime\\(n,b\\) for ProbablePrime n b with n,b ≥ 1$$
Lean4
/-- If `n` passes the Fermat primality test to base `b`, then `n` is coprime with `b`, assuming that
`n` and `b` are both positive.
-/
theorem coprime_of_probablePrime {n b : ℕ} (h : ProbablePrime n b) (h₁ : 1 ≤ n) (h₂ : 1 ≤ b) : Nat.Coprime n b :=
by
by_cases h₃ : 2 ≤ n
· -- To prove that `n` is coprime with `b`, we need to show that for all prime factors of `n`,
-- we can derive a contradiction if `n` divides `b`.
apply Nat.coprime_of_dvd
rintro k hk ⟨m, rfl⟩
⟨j, rfl⟩
-- Because prime numbers do not divide 1, it suffices to show that `k ∣ 1` to prove a
-- contradiction
apply Nat.Prime.not_dvd_one hk
replace h := dvd_of_mul_right_dvd h
rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]
-- Since `k` divides `b`, `k` also divides any power of `b` except `b ^ 0`. Therefore, it
-- suffices to show that `n - 1` isn't zero. However, we know that `n - 1` isn't zero because we
-- assumed `2 ≤ n` when doing `by_cases`.
refine dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)
cutsat
-- If `n = 1`, then it follows trivially that `n` is coprime with `b`.
· rw [show n = 1 by cutsat]
simp
