HomeHome Metamath Proof Explorer
Theorem List (p. 416 of 483)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-30741)
  Hilbert Space Explorer  Hilbert Space Explorer
(30742-32264)
  Users' Mathboxes  Users' Mathboxes
(32265-48238)
 

Theorem List for Metamath Proof Explorer - 41501-41600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlcmineqlem2 41501* Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = Σ𝑘 ∈ (0...(𝑁𝑀))(((-1↑𝑘) · ((𝑁𝑀)C𝑘)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · (𝑥𝑘)) d𝑥))
 
Theoremlcmineqlem3 41502* Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 30-Apr-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = Σ𝑘 ∈ (0...(𝑁𝑀))(((-1↑𝑘) · ((𝑁𝑀)C𝑘)) · (1 / (𝑀 + 𝑘))))
 
Theoremlcmineqlem4 41503 Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 41505. (Contributed by metakunt, 10-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)    &   (𝜑𝐾 ∈ (0...(𝑁𝑀)))       (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ)
 
Theoremlcmineqlem5 41504 Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐶 ≠ 0)       (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶)))
 
Theoremlcmineqlem6 41505* Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 10-May-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℤ)
 
Theoremlcmineqlem7 41506 Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.)
(ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1)
 
Theoremlcmineqlem8 41507* Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 < 𝑁)       (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁𝑀) · ((1 − 𝑥)↑((𝑁𝑀) − 1)))))
 
Theoremlcmineqlem9 41508* (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁𝑀))) ∈ (ℂ–cn→ℂ))
 
Theoremlcmineqlem10 41509* Induction step of lcmineqlem13 41512 (deduction form). (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 < 𝑁)       (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥))
 
Theoremlcmineqlem11 41510 Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 < 𝑁)       (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁𝑀)) · (1 / (𝑀 · (𝑁C𝑀)))))
 
Theoremlcmineqlem12 41511* Base case for induction. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1))))
 
Theoremlcmineqlem13 41512* Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = (1 / (𝑀 · (𝑁C𝑀))))
 
Theoremlcmineqlem14 41513 Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝐷 ∈ ℕ)    &   (𝜑𝐸 ∈ ℕ)    &   (𝜑 → (𝐴 · 𝐶) ∥ 𝐷)    &   (𝜑 → (𝐵 · 𝐶) ∥ 𝐸)    &   (𝜑𝐷𝐸)    &   (𝜑 → (𝐴 gcd 𝐵) = 1)       (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸)
 
Theoremlcmineqlem15 41514* F times the least common multiple of 1 to n is a natural number. (Contributed by metakunt, 10-May-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℕ)
 
Theoremlcmineqlem16 41515 Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁)))
 
Theoremlcmineqlem17 41516 Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.)
(𝜑𝑁 ∈ ℕ0)       (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
 
Theoremlcmineqlem18 41517 Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
 
Theoremlcmineqlem19 41518 Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))))
 
Theoremlcmineqlem20 41519 Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
 
Theoremlcmineqlem21 41520 The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 4 ≤ 𝑁)       (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
 
Theoremlcmineqlem22 41521 The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 4 ≤ 𝑁)       (𝜑 → ((2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2)))))
 
Theoremlcmineqlem23 41522 Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 9 ≤ 𝑁)       (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
 
Theoremlcmineqlem 41523 The least common multiple inequality lemma, a central result for future use. Theorem 3.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 16-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 7 ≤ 𝑁)       (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
 
21.27.5  Logarithm inequalities
 
Theorem3exp7 41524 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.)
(3↑7) = 2187
 
Theorem3lexlogpow5ineq1 41525 First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.)
9 < ((11 / 7)↑5)
 
Theorem3lexlogpow5ineq2 41526 Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
(𝜑𝑋 ∈ ℝ)    &   (𝜑 → 3 ≤ 𝑋)       (𝜑 → ((11 / 7)↑5) ≤ ((2 logb 𝑋)↑5))
 
Theorem3lexlogpow5ineq4 41527 Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.)
(𝜑𝑋 ∈ ℝ)    &   (𝜑 → 3 ≤ 𝑋)       (𝜑 → 9 < ((2 logb 𝑋)↑5))
 
Theorem3lexlogpow5ineq3 41528 Combined inequality chain for a specific power of the binary logarithm, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
(𝜑𝑋 ∈ ℝ)    &   (𝜑 → 3 ≤ 𝑋)       (𝜑 → 7 < ((2 logb 𝑋)↑5))
 
Theorem3lexlogpow2ineq1 41529 Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
((3 / 2) < (2 logb 3) ∧ (2 logb 3) < (5 / 3))
 
Theorem3lexlogpow2ineq2 41530 Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
(2 < ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < 3)
 
Theorem3lexlogpow5ineq5 41531 Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
((2 logb 3)↑5) ≤ 15
 
21.27.6  Miscellaneous results for AKS formalisation
 
Theoremintlewftc 41532* Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)    &   (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   (𝜑𝐷 = (ℝ D 𝐹))    &   (𝜑𝐸 = (ℝ D 𝐺))    &   (𝜑𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   (𝜑𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   (𝜑𝐷 ∈ 𝐿1)    &   (𝜑𝐸 ∈ 𝐿1)    &   (𝜑𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃))    &   (𝜑𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄))    &   ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑃𝑄)    &   (𝜑 → (𝐹𝐴) ≤ (𝐺𝐴))       (𝜑 → (𝐹𝐵) ≤ (𝐺𝐵))
 
Theoremaks4d1lem1 41533 Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵))
 
Theoremaks4d1p1p1 41534* Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴𝑐𝑘) = (𝐴𝑐Σ𝑘 ∈ (1...𝑁)𝑘))
 
Theoremdvrelog2 41535* The derivative of the logarithm, ftc2 25992 version. (Contributed by metakunt, 11-Aug-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)    &   (𝜑𝐴𝐵)    &   𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))    &   𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))       (𝜑 → (ℝ D 𝐹) = 𝐺)
 
Theoremdvrelog3 41536* The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴𝐵)    &   𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥))    &   𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))       (𝜑 → (ℝ D 𝐹) = 𝐺)
 
Theoremdvrelog2b 41537* Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴𝐵)    &   𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥))    &   𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))       (𝜑 → (ℝ D 𝐹) = 𝐺)
 
Theorem0nonelalab 41538 Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)    &   (𝜑𝐴𝐵)    &   (𝜑𝐶 ∈ (𝐴(,)𝐵))       (𝜑 → 0 ≠ 𝐶)
 
Theoremdvrelogpow2b 41539* Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)    &   (𝜑𝐴𝐵)    &   𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑𝑁))    &   𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐶 · (((log‘𝑥)↑(𝑁 − 1)) / 𝑥)))    &   𝐶 = (𝑁 / ((log‘2)↑𝑁))    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (ℝ D 𝐹) = 𝐺)
 
Theoremaks4d1p1p3 41540 Bound of a ceiling of the binary logarithm to the fifth power. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝑁 ∈ ℕ)    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   (𝜑 → 3 ≤ 𝑁)       (𝜑 → (𝑁𝑐(⌊‘(2 logb 𝐵))) < (𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))))
 
Theoremaks4d1p1p2 41541* Rewrite 𝐴 in more suitable form. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝑁 ∈ ℕ)    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   (𝜑 → 3 ≤ 𝑁)       (𝜑𝐴 < (𝑁𝑐(((2 logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2))))
 
Theoremaks4d1p1p4 41542* Technical step for inequality. The hard work is in to prove the final hypothesis. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝑁 ∈ ℕ)    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   (𝜑 → 3 ≤ 𝑁)    &   𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1))    &   𝐷 = ((2 logb 𝑁)↑2)    &   𝐸 = ((2 logb 𝑁)↑4)    &   (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸)       (𝜑𝐴 < (2↑𝐵))
 
Theoremdvle2 41543* Collapsed dvle 25953. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐺) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐸)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐹))    &   (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐺)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐻))    &   ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝐹𝐻)    &   (𝑥 = 𝐴𝐸 = 𝑃)    &   (𝑥 = 𝐴𝐺 = 𝑄)    &   (𝑥 = 𝐵𝐸 = 𝑅)    &   (𝑥 = 𝐵𝐺 = 𝑆)    &   (𝜑𝑃𝑄)    &   (𝜑𝐴𝐵)       (𝜑𝑅𝑆)
 
Theoremaks4d1p1p6 41544* Inequality lift to differentiable functions for a term in AKS inequality lemma. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 3 ≤ 𝐴)    &   (𝜑𝐴𝐵)       (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))))
 
Theoremaks4d1p1p7 41545 Bound of intermediary of inequality step. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑 → 4 ≤ 𝐴)       (𝜑 → ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
 
Theoremaks4d1p1p5 41546* Show inequality for existence of a non-divisor. (Contributed by metakunt, 19-Aug-2024.)
(𝜑𝑁 ∈ ℕ)    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   (𝜑 → 4 ≤ 𝑁)    &   𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1))    &   𝐷 = ((2 logb 𝑁)↑2)    &   𝐸 = ((2 logb 𝑁)↑4)       (𝜑𝐴 < (2↑𝐵))
 
Theoremaks4d1p1 41547* Show inequality for existence of a non-divisor. (Contributed by metakunt, 21-Aug-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑𝐴 < (2↑𝐵))
 
Theoremaks4d1p2 41548 Technical lemma for existence of non-divisor. (Contributed by metakunt, 27-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → (2↑𝐵) ≤ (lcm‘(1...𝐵)))
 
Theoremaks4d1p3 41549* There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 27-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴)
 
Theoremaks4d1p4 41550* There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 28-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅𝐴))
 
Theoremaks4d1p5 41551* Show that 𝑁 and 𝑅 are coprime for AKS existence theorem. Precondition will be eliminated in further theorem. (Contributed by metakunt, 30-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )    &   (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴)       (𝜑 → (𝑁 gcd 𝑅) = 1)
 
Theoremaks4d1p6 41552* The maximal prime power exponent is smaller than the binary logarithm floor of 𝐵. (Contributed by metakunt, 30-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑅)    &   𝐾 = (𝑃 pCnt 𝑅)       (𝜑𝐾 ≤ (⌊‘(2 logb 𝐵)))
 
Theoremaks4d1p7d1 41553* Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )    &   (𝜑 → ∀𝑝 ∈ ℙ (𝑝𝑅𝑝𝑁))       (𝜑𝑅 ∥ (𝑁↑(⌊‘(2 logb 𝐵))))
 
Theoremaks4d1p7 41554* Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → ∃𝑝 ∈ ℙ (𝑝𝑅 ∧ ¬ 𝑝𝑁))
 
Theoremaks4d1p8d1 41555 If a prime divides one number 𝑀, but not another number 𝑁, then it divides the quotient of 𝑀 and the gcd of 𝑀 and 𝑁. (Contributed by Thierry Arnoux, 10-Nov-2024.)
(𝜑𝑃 ∈ ℙ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑀)    &   (𝜑 → ¬ 𝑃𝑁)       (𝜑𝑃 ∥ (𝑀 / (𝑀 gcd 𝑁)))
 
Theoremaks4d1p8d2 41556 Any prime power dividing a positive integer is less than that integer if that integer has another prime factor. (Contributed by metakunt, 13-Nov-2024.)
(𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑄 ∈ ℙ)    &   (𝜑𝑃𝑅)    &   (𝜑𝑄𝑅)    &   (𝜑 → ¬ 𝑃𝑁)    &   (𝜑𝑄𝑁)       (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) < 𝑅)
 
Theoremaks4d1p8d3 41557 The remainder of a division with its maximal prime power is coprime with that prime power. (Contributed by metakunt, 13-Nov-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)       (𝜑 → ((𝑁 / (𝑃↑(𝑃 pCnt 𝑁))) gcd (𝑃↑(𝑃 pCnt 𝑁))) = 1)
 
Theoremaks4d1p8 41558* Show that 𝑁 and 𝑅 are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024.) (Proof sketch by Thierry Arnoux.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → (𝑁 gcd 𝑅) = 1)
 
Theoremaks4d1p9 41559* Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → ((2 logb 𝑁)↑2) < ((od𝑅)‘𝑁))
 
Theoremaks4d1 41560* Lemma 4.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf, existence of a polynomially bounded number by the digit size of 𝑁 that asserts the polynomial subspace that we need to search to guarantee that 𝑁 is prime. Eventually we want to show that the polynomial searching space is bounded by degree 𝐵. (Contributed by metakunt, 14-Nov-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → ∃𝑟 ∈ (1...𝐵)((𝑁 gcd 𝑟) = 1 ∧ ((2 logb 𝑁)↑2) < ((od𝑟)‘𝑁)))
 
Theoremfldhmf1 41561 A field homomorphism is injective. This follows immediately from the definition of the ring homomorphism that sends the multiplicative identity to the multiplicative identity. (Contributed by metakunt, 7-Jan-2025.)
(𝜑𝐾 ∈ Field)    &   (𝜑𝐿 ∈ Field)    &   (𝜑𝐹 ∈ (𝐾 RingHom 𝐿))    &   𝐴 = (Base‘𝐾)    &   𝐵 = (Base‘𝐿)       (𝜑𝐹:𝐴1-1𝐵)
 
Syntaxcprimroots 41562 Define the class of primitive roots. (Contributed by metakunt, 25-Apr-2025.)
class PrimRoots
 
Definitiondf-primroots 41563* A 𝑟-th primitive root is a root of unity such that the exponent divides 𝑟. (Contributed by metakunt, 25-Apr-2025.)
PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0(Base‘𝑟) / 𝑏{𝑎𝑏 ∣ ((𝑘(.g𝑟)𝑎) = (0g𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑟)𝑎) = (0g𝑟) → 𝑘𝑙))})
 
Theoremisprimroot 41564* The value of a primitive root. (Contributed by metakunt, 25-Apr-2025.)
(𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ0)    &    = (.g𝑅)       (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙))))
 
Theoremmndmolinv 41565* An element of a monoid that has a right inverse has at most one left inverse. (Contributed by metakunt, 25-Apr-2025.)
𝐵 = (Base‘𝑀)    &   (𝜑𝑀 ∈ Mnd)    &   (𝜑𝐴𝐵)    &   (𝜑 → ∃𝑥𝐵 (𝐴(+g𝑀)𝑥) = (0g𝑀))       (𝜑 → ∃*𝑥𝐵 (𝑥(+g𝑀)𝐴) = (0g𝑀))
 
Theoremlinvh 41566* If an element has a unique left inverse, then the value satisfies the left inverse value equation. (Contributed by metakunt, 25-Apr-2025.)
(𝜑𝑋 ∈ (Base‘𝑅))    &   (𝜑 → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑋) = (0g𝑅))       (𝜑 → (((invg𝑅)‘𝑋)(+g𝑅)𝑋) = (0g𝑅))
 
Theoremprimrootsunit1 41567* Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.)
(𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}       (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅s 𝑈) PrimRoots 𝐾) ∧ (𝑅s 𝑈) ∈ Abel))
 
Theoremprimrootsunit 41568* Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.)
(𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}       (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅s 𝑈) PrimRoots 𝐾) ∧ (𝑅s 𝑈) ∈ Abel))
 
Theoremressmulgnnd 41569 Values for the group multiple function in a restricted structure, a deduction version. (Contributed by metakunt, 14-May-2025.)
𝐻 = (𝐺s 𝐴)    &   (𝜑𝐴 ⊆ (Base‘𝐺))    &   (𝜑𝑋𝐴)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (𝑁(.g𝐻)𝑋) = (𝑁(.g𝐺)𝑋))
 
Theoremprimrootscoprmpow 41570* Coprime powers of primitive roots are primitive roots. (Contributed by metakunt, 25-Apr-2025.)
(𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝐸 ∈ ℕ)    &   (𝜑 → (𝐸 gcd 𝐾) = 1)    &   (𝜑𝑀 ∈ (𝑅 PrimRoots 𝐾))    &   𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}       (𝜑 → (𝐸(.g𝑅)𝑀) ∈ (𝑅 PrimRoots 𝐾))
 
Theoremposbezout 41571* Bezout's identity restricted on positive integers in all but one variable. (Contributed by metakunt, 26-Apr-2025.)
((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
 
Theoremprimrootscoprf 41572* Coprime powers of primitive roots are primitive roots, as a function. (Contributed by metakunt, 26-Apr-2025.)
𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐸(.g𝑅)𝑚))    &   (𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝐸 ∈ ℕ)    &   (𝜑 → (𝐸 gcd 𝐾) = 1)       (𝜑𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
 
Theoremprimrootscoprbij 41573* A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025.)
𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g𝑅)𝑚))    &   (𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐽 ∈ ℕ)    &   (𝜑𝑍 ∈ ℤ)    &   (𝜑 → 1 = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))    &   𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}       (𝜑𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))
 
Theoremprimrootscoprbij2 41574* A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025.)
𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g𝑅)𝑚))    &   (𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑 → (𝐼 gcd 𝐾) = 1)       (𝜑𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))
 
Theoremremexz 41575* Division with rest. (Contributed by metakunt, 15-May-2025.)
(𝜑𝑁 ∈ ℤ)    &   (𝜑𝐴 ∈ ℕ)       (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (0...(𝐴 − 1))𝑁 = ((𝑥 · 𝐴) + 𝑦))
 
Theoremprimrootlekpowne0 41576 There is no smaller power of a primitive root that sends it to the neutral element. (Contributed by metakunt, 15-May-2025.)
(𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝑀 ∈ (𝑅 PrimRoots 𝐾))    &   (𝜑𝑁 ∈ (1...(𝐾 − 1)))       (𝜑 → (𝑁(.g𝑅)𝑀) ≠ (0g𝑅))
 
Theoremprimrootspoweq0 41577* The power of a 𝑅-th primitive root is zero if and only if it divides 𝑅. (Contributed by metakunt, 15-May-2025.)
(𝜑𝑅 ∈ CMnd)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝑀 ∈ (𝑅 PrimRoots 𝐾))    &   𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → ((𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ↔ 𝐾𝑁))
 
Theoremaks6d1c1p1 41578* Definition of the introspective relation. (Contributed by metakunt, 25-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒𝐷𝑦)))}    &   (𝜑𝐹𝐵)    &   (𝜑𝐸 ∈ ℕ)       (𝜑 → (𝐸 𝐹 ↔ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝐸 ((𝑂𝐹)‘𝑦)) = ((𝑂𝐹)‘(𝐸𝐷𝑦))))
 
Theoremaks6d1c1p1rcl 41579* Reverse closure of the introspective relation. (Contributed by metakunt, 25-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒𝐷𝑦)))}    &   (𝜑𝐸 𝐹)       (𝜑 → (𝐸 ∈ ℕ ∧ 𝐹𝐵))
 
Theoremaks6d1c1p2 41580* 𝑃 and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝐷 = (.g𝑊)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝑃𝑁)    &   𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))    &   (𝜑𝐴 ∈ ℤ)       (𝜑𝑃 𝐹)
 
Theoremaks6d1c1p3 41581* In a field with a Frobenius isomorphism (read: algebraic closure or finite field), 𝑁 and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝐷 = (.g𝑊)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝑃𝑁)    &   𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))    &   (𝜑𝐴 ∈ ℤ)    &   (𝜑𝑁 𝐹)    &   (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 𝑥)) ∈ (𝐾 RingIso 𝐾))       (𝜑 → (𝑁 / 𝑃) 𝐹)
 
Theoremaks6d1c1p4 41582* The product of polynomials is introspective. (Contributed by metakunt, 25-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝐷 = (.g𝑊)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝑃𝑁)    &   (𝜑𝐸 𝐹)    &   (𝜑𝐸 𝐺)       (𝜑𝐸 (𝐹(+g𝑊)𝐺))
 
Theoremaks6d1c1p5 41583* The product of exponents is introspective. (Contributed by metakunt, 26-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝐸 gcd 𝑅) = 1)    &   (𝜑𝑃𝑁)    &   (𝜑𝐷 𝐹)    &   (𝜑𝐸 𝐹)       (𝜑 → (𝐷 · 𝐸) 𝐹)
 
Theoremaks6d1c1p7 41584* 𝑋 is introspective to all positive integers. (Contributed by metakunt, 30-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐿 ∈ ℕ)       (𝜑𝐿 𝑋)
 
Theoremaks6d1c1p6 41585* If a polynomials 𝐹 is introspective to 𝐸, then so are its powers. (Contributed by metakunt, 30-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝐷 = (.g𝑊)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐸 𝐹)    &   (𝜑𝐿 ∈ ℕ0)       (𝜑𝐸 (𝐿𝐷𝐹))
 
Theoremaks6d1c1p8 41586* If a number 𝐸 is introspective to 𝐹, then so are its powers. (Contributed by metakunt, 30-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝐷 = (.g𝑊)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐸 𝐹)    &   (𝜑𝐿 ∈ ℕ0)    &   (𝜑 → (𝐸 gcd 𝑅) = 1)       (𝜑 → (𝐸𝐿) 𝐹)
 
Theoremaks6d1c1 41587* Claim 1 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 30-Apr-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ((𝑂𝑓)‘𝑦)) = ((𝑂𝑓)‘(𝑒 𝑦)))}    &   𝑆 = (Poly1𝐾)    &   𝐵 = (Base‘𝑆)    &   𝑋 = (var1𝐾)    &   𝑊 = (mulGrp‘𝑆)    &   𝑉 = (mulGrp‘𝐾)    &    = (.g𝑉)    &   𝐶 = (algSc‘𝑆)    &   𝐷 = (.g𝑊)    &   𝑃 = (chr‘𝐾)    &   𝑂 = (eval1𝐾)    &    + = (+g𝑆)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐹:(0...𝐴)⟶ℕ0)    &   𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))    &   (𝜑𝐴 ∈ ℕ0)    &   (𝜑𝑈 ∈ ℕ0)    &   (𝜑𝐿 ∈ ℕ0)    &   𝐸 = ((𝑃𝑈) · ((𝑁 / 𝑃)↑𝐿))    &   (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))    &   (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 𝑥)) ∈ (𝐾 RingIso 𝐾))       (𝜑𝐸 (𝐺𝐹))
 
Theoremevl1gprodd 41588* Polynomial evaluation builder for a finite group product of polynomials. (Contributed by metakunt, 29-Apr-2025.)
𝑂 = (eval1𝑅)    &   𝑃 = (Poly1𝑅)    &   𝑄 = (mulGrp‘𝑃)    &   𝐵 = (Base‘𝑅)    &   𝑈 = (Base‘𝑃)    &   𝑆 = (mulGrp‘𝑅)    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝑌𝐵)    &   (𝜑 → ∀𝑥𝑁 𝑀𝑈)    &   (𝜑𝑁 ∈ Fin)       (𝜑 → ((𝑂‘(𝑄 Σg (𝑥𝑁𝑀)))‘𝑌) = (𝑆 Σg (𝑥𝑁 ↦ ((𝑂𝑀)‘𝑌))))
 
Theoremaks6d1c2p1 41589* In the AKS-theorem the subset defined by 𝐸 takes values in the positive integers. (Contributed by metakunt, 7-Jan-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))       (𝜑𝐸:(ℕ0 × ℕ0)⟶ℕ)
 
Theoremaks6d1c2p2 41590* Injective condition for countability argument assuming that 𝑁 is not a prime power. (Contributed by metakunt, 7-Jan-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   (𝜑𝑄 ∈ ℙ)    &   (𝜑𝑄𝑁)    &   (𝜑𝑃𝑄)       (𝜑𝐸:(ℕ0 × ℕ0)–1-1→ℕ)
 
Theoremhashscontpowcl 41591 Closure of E for https://www3.nd.edu/%7eandyp/notes/AKS.pdf Theorem 6.1. (Contributed by metakunt, 28-Apr-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   𝐿 = (ℤRHom‘𝑌)    &   𝑌 = (ℤ/nℤ‘𝑅)       (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
 
Theoremhashscontpow1 41592 Helper lemma for to prove inequality in Zr. (Contributed by metakunt, 28-Apr-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐴 ∈ (1...((od𝑅)‘𝑁)))    &   (𝜑𝐵 ∈ (1...((od𝑅)‘𝑁)))    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   𝐿 = (ℤRHom‘𝑌)    &   𝑌 = (ℤ/nℤ‘𝑅)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐿‘(𝑁𝐴)) ≠ (𝐿‘(𝑁𝐵)))
 
Theoremhashscontpow 41593* If a set contains all 𝑁-th powers, then the size of the image under the ZR homomorphism is greater than the 𝑅-th order of 𝑁. (Contributed by metakunt, 28-Apr-2025.)
(𝜑𝐸 ⊆ ℤ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑 → ∀𝑘 ∈ ℕ0 (𝑁𝑘) ∈ 𝐸)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   𝐿 = (ℤRHom‘𝑌)    &   𝑌 = (ℤ/nℤ‘𝑅)       (𝜑 → ((od𝑅)‘𝑁) ≤ (♯‘(𝐿𝐸)))
 
Theoremaks6d1c3 41594* Claim 3 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 28-Apr-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   𝐿 = (ℤRHom‘𝑌)    &   𝑌 = (ℤ/nℤ‘𝑅)    &   (𝜑 → ((2 logb 𝑁)↑2) < ((od𝑅)‘𝑁))       (𝜑 → ((2 logb 𝑁)↑2) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
 
Theoremaks6d1c4 41595* Claim 4 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 12-May-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))       (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (ϕ‘𝑅))
 
Theoremaks6d1c1rh 41596* Claim 1 of AKS primality proof with collapsed definitions since their ease of use is no longer needed. (Contributed by metakunt, 1-May-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}    &   𝑃 = (chr‘𝐾)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐹:(0...𝐴)⟶ℕ0)    &   𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))    &   (𝜑𝐴 ∈ ℕ0)    &   (𝜑𝑈 ∈ ℕ0)    &   (𝜑𝐿 ∈ ℕ0)    &   𝐸 = ((𝑃𝑈) · ((𝑁 / 𝑃)↑𝐿))    &   (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))    &   (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))       (𝜑𝐸 (𝐺𝐹))
 
Theoremaks6d1c2lem3 41597* Lemma for aks6d1c2 41601 to simplify context. (Contributed by metakunt, 1-May-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}    &   𝑃 = (chr‘𝐾)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐹:(0...𝐴)⟶ℕ0)    &   𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))    &   (𝜑𝐴 ∈ ℕ0)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))    &   (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))    &   (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))    &   (𝜑𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))    &   𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀))    &   𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))    &   𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵)))    &   (𝜑𝐼𝐶)    &   (𝜑𝐽𝐶)    &   (𝜑𝐼 < 𝐽)    &    = (.g‘(mulGrp‘(Poly1𝐾)))    &   𝑋 = (var1𝐾)    &   𝑆 = ((𝐽 𝑋)(-g‘(Poly1𝐾))(𝐼 𝑋))    &   (𝜑𝑈 ∈ ℕ)    &   (𝜑𝐽 = (𝐼 + (𝑈 · 𝑅)))    &   (𝜑𝑠 ∈ (ℕ0m (0...𝐴)))    &   (𝜑𝑟 ∈ (0...𝐵))    &   (𝜑𝑜 ∈ (0...𝐵))    &   (𝜑𝐽 = (𝑟𝐸𝑜))    &   (𝜑𝑝 ∈ (0...𝐵))    &   (𝜑𝑞 ∈ (0...𝐵))    &   (𝜑𝐼 = (𝑝𝐸𝑞))    &   (𝜑𝐼 ∈ ℕ0)       (𝜑 → (𝐽(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘(𝐺𝑠))‘𝑀)) = (𝐼(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘(𝐺𝑠))‘𝑀)))
 
Theoremaks6d1c2lem4 41598* Claim 2 of Theorem 6.1 AKS, Preparation for injectivity proof. (Contributed by metakunt, 1-May-2025.)
= {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}    &   𝑃 = (chr‘𝐾)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑁)    &   (𝜑 → (𝑁 gcd 𝑅) = 1)    &   (𝜑𝐹:(0...𝐴)⟶ℕ0)    &   𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))    &   (𝜑𝐴 ∈ ℕ0)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))    &   (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))    &   (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))    &   (𝜑𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))    &   𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀))    &   𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))    &   𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵)))    &   (𝜑𝐼𝐶)    &   (𝜑𝐽𝐶)    &   (𝜑𝐼 < 𝐽)    &    = (.g‘(mulGrp‘(Poly1𝐾)))    &   𝑋 = (var1𝐾)    &   𝑆 = ((𝐽 𝑋)(-g‘(Poly1𝐾))(𝐼 𝑋))    &   (𝜑𝑈 ∈ ℕ)    &   (𝜑𝐽 = (𝐼 + (𝑈 · 𝑅)))       (𝜑 → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
 
Theoremhashnexinj 41599* If the number of elements of the domain are greater than the number of elements in a codomain, then there are two different values that map to the same. (Contributed by metakunt, 2-May-2025.)
(𝜑𝐴 ∈ Fin)    &   (𝜑𝐵 ∈ Fin)    &   (𝜑 → (♯‘𝐵) < (♯‘𝐴))    &   (𝜑𝐹:𝐴𝐵)       (𝜑 → ∃𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑦))
 
Theoremhashnexinjle 41600* If the number of elements of the domain are greater than the number of elements in a codomain, then there are two different values that map to the same. Also we introduce a one sided inequality to simplify a duplicateable proof. (Contributed by metakunt, 2-May-2025.)
(𝜑𝐴 ∈ Fin)    &   (𝜑𝐵 ∈ Fin)    &   (𝜑 → (♯‘𝐵) < (♯‘𝐴))    &   (𝜑𝐹:𝐴𝐵)    &   (𝜑𝐴 ⊆ ℝ)       (𝜑 → ∃𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31500 316 31501-31600 317 31601-31700 318 31701-31800 319 31801-31900 320 31901-32000 321 32001-32100 322 32101-32200 323 32201-32300 324 32301-32400 325 32401-32500 326 32501-32600 327 32601-32700 328 32701-32800 329 32801-32900 330 32901-33000 331 33001-33100 332 33101-33200 333 33201-33300 334 33301-33400 335 33401-33500 336 33501-33600 337 33601-33700 338 33701-33800 339 33801-33900 340 33901-34000 341 34001-34100 342 34101-34200 343 34201-34300 344 34301-34400 345 34401-34500 346 34501-34600 347 34601-34700 348 34701-34800 349 34801-34900 350 34901-35000 351 35001-35100 352 35101-35200 353 35201-35300 354 35301-35400 355 35401-35500 356 35501-35600 357 35601-35700 358 35701-35800 359 35801-35900 360 35901-36000 361 36001-36100 362 36101-36200 363 36201-36300 364 36301-36400 365 36401-36500 366 36501-36600 367 36601-36700 368 36701-36800 369 36801-36900 370 36901-37000 371 37001-37100 372 37101-37200 373 37201-37300 374 37301-37400 375 37401-37500 376 37501-37600 377 37601-37700 378 37701-37800 379 37801-37900 380 37901-38000 381 38001-38100 382 38101-38200 383 38201-38300 384 38301-38400 385 38401-38500 386 38501-38600 387 38601-38700 388 38701-38800 389 38801-38900 390 38901-39000 391 39001-39100 392 39101-39200 393 39201-39300 394 39301-39400 395 39401-39500 396 39501-39600 397 39601-39700 398 39701-39800 399 39801-39900 400 39901-40000 401 40001-40100 402 40101-40200 403 40201-40300 404 40301-40400 405 40401-40500 406 40501-40600 407 40601-40700 408 40701-40800 409 40801-40900 410 40901-41000 411 41001-41100 412 41101-41200 413 41201-41300 414 41301-41400 415 41401-41500 416 41501-41600 417 41601-41700 418 41701-41800 419 41801-41900 420 41901-42000 421 42001-42100 422 42101-42200 423 42201-42300 424 42301-42400 425 42401-42500 426 42501-42600 427 42601-42700 428 42701-42800 429 42801-42900 430 42901-43000 431 43001-43100 432 43101-43200 433 43201-43300 434 43301-43400 435 43401-43500 436 43501-43600 437 43601-43700 438 43701-43800 439 43801-43900 440 43901-44000 441 44001-44100 442 44101-44200 443 44201-44300 444 44301-44400 445 44401-44500 446 44501-44600 447 44601-44700 448 44701-44800 449 44801-44900 450 44901-45000 451 45001-45100 452 45101-45200 453 45201-45300 454 45301-45400 455 45401-45500 456 45501-45600 457 45601-45700 458 45701-45800 459 45801-45900 460 45901-46000 461 46001-46100 462 46101-46200 463 46201-46300 464 46301-46400 465 46401-46500 466 46501-46600 467 46601-46700 468 46701-46800 469 46801-46900 470 46901-47000 471 47001-47100 472 47101-47200 473 47201-47300 474 47301-47400 475 47401-47500 476 47501-47600 477 47601-47700 478 47701-47800 479 47801-47900 480 47901-48000 481 48001-48100 482 48101-48200 483 48201-48238
  Copyright terms: Public domain < Previous  Next >