theorem
proved
weak_prime_nineteen
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 2756.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
2766
2767/-- 47 is a weak prime: 47 < (43 + 53)/2 = 48. -/
2768theorem weak_prime_fortyseven : Prime 47 ∧ Prime 43 ∧ Prime 53 ∧ 47 < (43 + 53) / 2 := by native_decide
2769
2770/-- 61 is a weak prime: 61 < (59 + 67)/2 = 63. -/
2771theorem weak_prime_sixtyone : Prime 61 ∧ Prime 59 ∧ Prime 67 ∧ 61 < (59 + 67) / 2 := by native_decide
2772
2773/-- 73 is a weak prime: 73 < (71 + 79)/2 = 75. -/
2774theorem weak_prime_seventythree : Prime 73 ∧ Prime 71 ∧ Prime 79 ∧ 73 < (71 + 79) / 2 := by native_decide
2775
2776/-- 83 is a weak prime: 83 < (79 + 89)/2 = 84. -/
2777theorem weak_prime_eightythree : Prime 83 ∧ Prime 79 ∧ Prime 89 ∧ 83 < (79 + 89) / 2 := by native_decide
2778
2779/-- 89 is a weak prime: 89 < (83 + 97)/2 = 90. -/
2780theorem weak_prime_eightynine : Prime 89 ∧ Prime 83 ∧ Prime 97 ∧ 89 < (83 + 97) / 2 := by native_decide
2781
2782/-- 103 is a weak prime: 103 < (101 + 107)/2 = 104 (RS-relevant). -/
2783theorem weak_prime_onehundredthree : Prime 103 ∧ Prime 101 ∧ Prime 107 ∧ 103 < (101 + 107) / 2 := by native_decide
2784
2785/-! ### Superprimes (prime-indexed primes: p_n where n is also prime) -/
2786