G. Austria 2015 Problem 4

Show that every positive integer ending in $133$ in decimal representation has a prime factor larger than $7$.

<small>Note: the template was updated after the contest.</small>

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.29.0.

import Mathlib.Data.Nat.Prime.Defs

theorem solution (n : ℕ) (hn : 0 < n) (h133 : n % 1000 = 133) : ∃ p > 7, p.Prime ∧ p ∣ n := sorry

Submit Solution

Login to submit a solution.

Recent Submissions