theorem
proved
balanced_prime_onehundredfiftyseven
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2108.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2105theorem balanced_prime_fiftythree : Prime 53 ∧ Prime 47 ∧ Prime 59 ∧ (47 + 59) / 2 = 53 := by native_decide
2106
2107/-- 157 is a balanced prime: (151 + 163)/2 = 157. -/
2108theorem balanced_prime_onehundredfiftyseven : Prime 157 ∧ Prime 151 ∧ Prime 163 ∧ (151 + 163) / 2 = 157 := by native_decide
2109
2110/-- 173 is a balanced prime: (167 + 179)/2 = 173. -/
2111theorem balanced_prime_onehundredseventythree : Prime 173 ∧ Prime 167 ∧ Prime 179 ∧ (167 + 179) / 2 = 173 := by native_decide
2112
2113/-- 211 is a balanced prime: (199 + 223)/2 = 211. -/
2114theorem balanced_prime_twohundredeleven : Prime 211 ∧ Prime 199 ∧ Prime 223 ∧ (199 + 223) / 2 = 211 := by native_decide
2115
2116/-- 257 is a balanced prime: (251 + 263)/2 = 257 (Fermat prime F_3). -/
2117theorem balanced_prime_twohundredfiftyseven : Prime 257 ∧ Prime 251 ∧ Prime 263 ∧ (251 + 263) / 2 = 257 := by native_decide
2118
2119/-! ### Practical numbers (every m ≤ n is a sum of distinct divisors of n) -/
2120
2121/-- σ_1(1) = 1 ≥ 1, so 1 is practical. -/
2122theorem practical_one : sigma 1 1 ≥ 1 := by native_decide
2123
2124/-- σ_1(2) = 3 ≥ 2, so 2 is practical. -/
2125theorem practical_two : sigma 1 2 ≥ 2 := by native_decide
2126
2127/-- σ_1(4) = 7 ≥ 4, so 4 is practical. -/
2128theorem practical_four : sigma 1 4 ≥ 4 := by native_decide
2129
2130/-- σ_1(6) = 12 ≥ 6, so 6 is practical. -/
2131theorem practical_six : sigma 1 6 ≥ 6 := by native_decide
2132
2133/-- σ_1(8) = 15 ≥ 8, so 8 is practical. -/
2134theorem practical_eight : sigma 1 8 ≥ 8 := by native_decide
2135
2136/-- σ_1(12) = 28 ≥ 12, so 12 is practical. -/
2137theorem practical_twelve : sigma 1 12 ≥ 12 := by native_decide
2138