P. 418 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41701-41800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imadomfi 41701	An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025.)
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐹) → (𝐹 “ 𝐴) ≼ 𝐴)
21.28.3  Some gcd and lcm results
Theorem	12gcd5e1 41702	The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;12 gcd 5) = 1
Theorem	60gcd6e6 41703	The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 gcd 6) = 6
Theorem	60gcd7e1 41704	The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 gcd 7) = 1
Theorem	420gcd8e4 41705	The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;;420 gcd 8) = 4
Theorem	lcmeprodgcdi 41706	Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐺 ∈ ℕ    &   ⊢ 𝐻 ∈ ℕ    &   ⊢ (𝑀 gcd 𝑁) = 𝐺    &   ⊢ (𝐺 · 𝐻) = 𝐴    &   ⊢ (𝑀 · 𝑁) = 𝐴    ⇒   ⊢ (𝑀 lcm 𝑁) = 𝐻
Theorem	12lcm5e60 41707	The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;12 lcm 5) = ;60
Theorem	60lcm6e60 41708	The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 lcm 6) = ;60
Theorem	60lcm7e420 41709	The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 lcm 7) = ;;420
Theorem	420lcm8e840 41710	The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;;420 lcm 8) = ;;840
Theorem	lcmfunnnd 41711	Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (lcm‘(1...𝑁)) = ((lcm‘(1...(𝑁 − 1))) lcm 𝑁))
Theorem	lcm1un 41712	Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...1)) = 1
Theorem	lcm2un 41713	Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...2)) = 2
Theorem	lcm3un 41714	Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...3)) = 6
Theorem	lcm4un 41715	Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...4)) = ;12
Theorem	lcm5un 41716	Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...5)) = ;60
Theorem	lcm6un 41717	Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...6)) = ;60
Theorem	lcm7un 41718	Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...7)) = ;;420
Theorem	lcm8un 41719	Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...8)) = ;;840
21.28.4  Least common multiple inequality theorem
Theorem	3factsumint1 41720*	Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
⊢ 𝐴 = (𝐿[,]𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥)
Theorem	3factsumint2 41721*	Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥)
Theorem	3factsumint3 41722*	Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
⊢ 𝐴 = (𝐿[,]𝑈)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥))
Theorem	3factsumint4 41723*	Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥)
Theorem	3factsumint 41724*	Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.)
⊢ 𝐴 = (𝐿[,]𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥))
Theorem	resopunitintvd 41725	Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝐴) ∈ ((0(,)1)–cn→ℂ))
Theorem	resclunitintvd 41726	Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ ((0[,]1)–cn→ℂ))
Theorem	resdvopclptsd 41727*	Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ 𝐴)) = (𝑥 ∈ (0(,)1) ↦ 𝐵))
Theorem	lcmineqlem1 41728*	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)((𝑥↑(𝑀 − 1)) · Σ𝑘 ∈ (0...(𝑁 − 𝑀))(((-1↑𝑘) · ((𝑁 − 𝑀)C𝑘)) · (𝑥↑𝑘))) d𝑥)
Theorem	lcmineqlem2 41729*	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𝑥))
Theorem	lcmineqlem3 41730*	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 / (𝑀 + 𝑘))))
Theorem	lcmineqlem4 41731	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 41733. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    &   ⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀)))    ⇒   ⊢ (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ)
Theorem	lcmineqlem5 41732	Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶)))
Theorem	lcmineqlem6 41733*	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...𝑁)) · 𝐹) ∈ ℤ)
Theorem	lcmineqlem7 41734	Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.)
⊢ (ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1)
Theorem	lcmineqlem8 41735*	Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))))
Theorem	lcmineqlem9 41736*	(1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ))
Theorem	lcmineqlem10 41737*	Induction step of lcmineqlem13 41740 (deduction form). (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥))
Theorem	lcmineqlem11 41738	Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀)))))
Theorem	lcmineqlem12 41739*	Base case for induction. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1))))
Theorem	lcmineqlem13 41740*	Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.)
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀))))
Theorem	lcmineqlem14 41741	Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷)    &   ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸)    &   ⊢ (𝜑 → 𝐷 ∥ 𝐸)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸)
Theorem	lcmineqlem15 41742*	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...𝑁)) · 𝐹) ∈ ℕ)
Theorem	lcmineqlem16 41743	Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁)))
Theorem	lcmineqlem17 41744	Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
Theorem	lcmineqlem18 41745	Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
Theorem	lcmineqlem19 41746	Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem20 41747	Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem21 41748	The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 4 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem22 41749	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)))))
Theorem	lcmineqlem23 41750	Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 9 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
Theorem	lcmineqlem 41751	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.28.5  Logarithm inequalities
Theorem	3exp7 41752	3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.)
⊢ (3↑7) = ;;;2187
Theorem	3lexlogpow5ineq1 41753	First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.)
⊢ 9 < ((;11 / 7)↑5)
Theorem	3lexlogpow5ineq2 41754	Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 3 ≤ 𝑋)    ⇒   ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5))
Theorem	3lexlogpow5ineq4 41755	Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 3 ≤ 𝑋)    ⇒   ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5))
Theorem	3lexlogpow5ineq3 41756	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))
Theorem	3lexlogpow2ineq1 41757	Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
⊢ ((3 / 2) < (2 logb 3) ∧ (2 logb 3) < (5 / 3))
Theorem	3lexlogpow2ineq2 41758	Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
⊢ (2 < ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < 3)
Theorem	3lexlogpow5ineq5 41759	Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
⊢ ((2 logb 3)↑5) ≤ ;15
21.28.6  Miscellaneous results for AKS formalisation
Theorem	intlewftc 41760*	Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃))    &   ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄)    &   ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴))    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵))
Theorem	aks4d1lem1 41761	Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵))
Theorem	aks4d1p1p1 41762*	Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘))
Theorem	dvrelog2 41763*	The derivative of the logarithm, ftc2 26070 version. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	dvrelog3 41764*	The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	dvrelog2b 41765*	Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	0nonelalab 41766	Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 0 ≠ 𝐶)
Theorem	dvrelogpow2b 41767*	Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑𝑁))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐶 · (((log‘𝑥)↑(𝑁 − 1)) / 𝑥)))    &   ⊢ 𝐶 = (𝑁 / ((log‘2)↑𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	aks4d1p1p3 41768	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))))
Theorem	aks4d1p1p2 41769*	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))))
Theorem	aks4d1p1p4 41770*	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↑𝐵))
Theorem	dvle2 41771*	Collapsed dvle 26031. (Contributed by metakunt, 19-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐺) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐸)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐹))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐺)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐻))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐹 ≤ 𝐻)    &   ⊢ (𝑥 = 𝐴 → 𝐸 = 𝑃)    &   ⊢ (𝑥 = 𝐴 → 𝐺 = 𝑄)    &   ⊢ (𝑥 = 𝐵 → 𝐸 = 𝑅)    &   ⊢ (𝑥 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑄)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝑅 ≤ 𝑆)
Theorem	aks4d1p1p6 41772*	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)) / 𝑥)))))
Theorem	aks4d1p1p7 41773	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) / 𝐴)))
Theorem	aks4d1p1p5 41774*	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↑𝐵))
Theorem	aks4d1p1 41775*	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↑𝐵))
Theorem	aks4d1p2 41776	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...𝐵)))
Theorem	aks4d1p3 41777*	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...𝐵) ¬ 𝑟 ∥ 𝐴)
Theorem	aks4d1p4 41778*	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...𝐵) ∧ ¬ 𝑅 ∥ 𝐴))
Theorem	aks4d1p5 41779*	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)
Theorem	aks4d1p6 41780*	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 𝐵)))
Theorem	aks4d1p7d1 41781*	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 𝐵))))
Theorem	aks4d1p7 41782*	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...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < )    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁))
Theorem	aks4d1p8d1 41783	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 𝑁)))
Theorem	aks4d1p8d2 41784	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 𝑅)) < 𝑅)
Theorem	aks4d1p8d3 41785	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)
Theorem	aks4d1p8 41786*	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)
Theorem	aks4d1p9 41787*	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ℤ‘𝑅)‘𝑁))
Theorem	aks4d1 41788*	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ℤ‘𝑟)‘𝑁)))
Theorem	fldhmf1 41789	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→𝐵)
Syntax	cprimroots 41790	Define the class of primitive roots. (Contributed by metakunt, 25-Apr-2025.)
class PrimRoots
Definition	df-primroots 41791*	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‘𝑟) → 𝑘 ∥ 𝑙))})
Theorem	isprimroot 41792*	The value of a primitive root. (Contributed by metakunt, 25-Apr-2025.)
⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ ↑ = (.g‘𝑅)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
Theorem	mndmolinv 41793*	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‘𝑀))
Theorem	linvh 41794*	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‘𝑅))
Theorem	primrootsunit1 41795*	Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.)
⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}    ⇒   ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
Theorem	primrootsunit 41796*	Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.)
⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}    ⇒   ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
Theorem	primrootscoprmpow 41797*	Coprime powers of primitive roots are primitive roots. (Contributed by metakunt, 25-Apr-2025.)
⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → (𝐸 gcd 𝐾) = 1)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾))    &   ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}    ⇒   ⊢ (𝜑 → (𝐸(.g‘𝑅)𝑀) ∈ (𝑅 PrimRoots 𝐾))
Theorem	posbezout 41798*	Bezout's identity restricted on positive integers in all but one variable. (Contributed by metakunt, 26-Apr-2025.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
Theorem	primrootscoprf 41799*	Coprime powers of primitive roots are primitive roots, as a function. (Contributed by metakunt, 26-Apr-2025.)
⊢ 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐸(.g‘𝑅)𝑚))    &   ⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → (𝐸 gcd 𝐾) = 1)    ⇒   ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
Theorem	primrootscoprbij 41800*	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 𝐾))