Prove2Me

lean_workbook_plus_60497

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Dado que (n,p)=1(n,p)=1, donde n,p∈Z+n, p \in Z^{+} y pp primo, demostrar que existe un número primo P1P_{1} y un entero positivo kk tal que nk+p=P1nk+p = P_{1}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60497 (n p : ℕ) (hp : p.Prime) (h : Nat.Coprime n p) : ∃ P k : ℕ, P.Prime ∧ n * k + p = P   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph