theorem
proved
six_almost_prime_fivehundredsixty
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 2735.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2732theorem six_almost_prime_fivehundredfortyfour : isSixAlmostPrime 544 = true := by native_decide
2733
2734/-- 560 = 2⁴ × 5 × 7 is 6-almost prime. -/
2735theorem six_almost_prime_fivehundredsixty : isSixAlmostPrime 560 = true := by native_decide
2736
2737-- Note: 576 = 2⁶ × 3², Ω = 6 + 2 = 8, so not 6-almost prime.
2738
2739/-- 624 = 2⁴ × 3 × 13 is 6-almost prime. -/
2740theorem six_almost_prime_sixhundredtwentyfour : isSixAlmostPrime 624 = true := by native_decide
2741
2742/-- 729 = 3⁶ is 6-almost prime. -/
2743theorem six_almost_prime_sevenhundredtwentynine : isSixAlmostPrime 729 = true := by native_decide
2744
2745/-! ### Weak primes (p < (p_prev + p_next)/2) -/
2746
2747-- Note: 3 < (2 + 5)/2 = 3.5, but in ℕ, (2+5)/2 = 3, so 3 < 3 is false. 3 is balanced.
2748
2749/-- 7 is a weak prime: 7 < (5 + 11)/2 = 8. -/
2750theorem weak_prime_seven : Prime 7 ∧ Prime 5 ∧ Prime 11 ∧ 7 < (5 + 11) / 2 := by native_decide
2751
2752/-- 13 is a weak prime: 13 < (11 + 17)/2 = 14. -/
2753theorem weak_prime_thirteen : Prime 13 ∧ Prime 11 ∧ Prime 17 ∧ 13 < (11 + 17) / 2 := by native_decide
2754
2755/-- 19 is a weak prime: 19 < (17 + 23)/2 = 20. -/
2756theorem weak_prime_nineteen : Prime 19 ∧ Prime 17 ∧ Prime 23 ∧ 19 < (17 + 23) / 2 := by native_decide
2757
2758/-- 23 is a weak prime: 23 < (19 + 29)/2 = 24. -/
2759theorem weak_prime_twentythree : Prime 23 ∧ Prime 19 ∧ Prime 29 ∧ 23 < (19 + 29) / 2 := by native_decide
2760
2761/-- 31 is a weak prime: 31 < (29 + 37)/2 = 33. -/
2762theorem weak_prime_thirtyone : Prime 31 ∧ Prime 29 ∧ Prime 37 ∧ 31 < (29 + 37) / 2 := by native_decide
2763
2764/-- 43 is a weak prime: 43 < (41 + 47)/2 = 44. -/
2765theorem weak_prime_fortythree : Prime 43 ∧ Prime 41 ∧ Prime 47 ∧ 43 < (41 + 47) / 2 := by native_decide