theorem
proved
mod6_five_prime
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 1894.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1891theorem mod6_onehundredthree_prime : Prime 103 ∧ 103 % 6 = 1 := by native_decide
1892
1893/-- 5 ≡ 5 (mod 6). -/
1894theorem mod6_five_prime : Prime 5 ∧ 5 % 6 = 5 := by native_decide
1895
1896/-- 11 ≡ 5 (mod 6) (RS-relevant). -/
1897theorem mod6_eleven_prime : Prime 11 ∧ 11 % 6 = 5 := by native_decide
1898
1899/-- 17 ≡ 5 (mod 6) (RS-relevant). -/
1900theorem mod6_seventeen_prime : Prime 17 ∧ 17 % 6 = 5 := by native_decide
1901
1902/-- 23 ≡ 5 (mod 6). -/
1903theorem mod6_twentythree_prime : Prime 23 ∧ 23 % 6 = 5 := by native_decide
1904
1905/-- 29 ≡ 5 (mod 6). -/
1906theorem mod6_twentynine_prime : Prime 29 ∧ 29 % 6 = 5 := by native_decide
1907
1908/-- 41 ≡ 5 (mod 6). -/
1909theorem mod6_fortyone_prime : Prime 41 ∧ 41 % 6 = 5 := by native_decide
1910
1911/-- 47 ≡ 5 (mod 6). -/
1912theorem mod6_fortyseven_prime : Prime 47 ∧ 47 % 6 = 5 := by native_decide
1913
1914/-- 53 ≡ 5 (mod 6). -/
1915theorem mod6_fiftythree_prime : Prime 53 ∧ 53 % 6 = 5 := by native_decide
1916
1917/-- 59 ≡ 5 (mod 6). -/
1918theorem mod6_fiftynine_prime : Prime 59 ∧ 59 % 6 = 5 := by native_decide
1919
1920/-- 71 ≡ 5 (mod 6). -/
1921theorem mod6_seventyone_prime : Prime 71 ∧ 71 % 6 = 5 := by native_decide
1922
1923/-- 83 ≡ 5 (mod 6). -/
1924theorem mod6_eightythree_prime : Prime 83 ∧ 83 % 6 = 5 := by native_decide