P. 427 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42601-42700   *Has distinct variable group(s)

Type	Label	Description
Statement
21.29.2  General helpful statements
Theorem	rhmzrhval 42601	Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ ℤ)    &   ⊢ 𝑀 = (ℤRHom‘𝑅)    &   ⊢ 𝑁 = (ℤRHom‘𝑆)    ⇒   ⊢ (𝜑 → (𝐹‘(𝑀‘𝑋)) = (𝑁‘𝑋))
Theorem	zndvdchrrhm 42602*	Construction of a ring homomorphism from ℤ/nℤ to 𝑅 when the characteristic of 𝑅 divides 𝑁. (Contributed by metakunt, 4-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (chr‘𝑅) ∈ ℤ)    &   ⊢ (𝜑 → (chr‘𝑅) ∥ 𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑍) ↦ ∪ ((ℤRHom‘𝑅) “ 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑍 RingHom 𝑅))
Theorem	relogbcld 42603	Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 𝐵 ≠ 1)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	relogbexpd 42604	Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≠ 1)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	relogbzexpd 42605	Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≠ 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶)))
Theorem	logblebd 42606	The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑌)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))
Theorem	uzindd 42607*	Induction on the upper integers that start at 𝑀. The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝑗 = 𝑀 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑗 = 𝑘 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑗 = 𝑁 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃 ∧ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘)) → 𝜏)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	fzadd2d 42608	Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑂 ∈ ℤ)    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃))    &   ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂))    &   ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃))    ⇒   ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅))
Theorem	fzne2d 42609	Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ≠ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 < 𝑁)
Theorem	eqfnfv2d2 42610*	Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	fzsplitnd 42611	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	fzsplitnr 42612	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	addassnni 42613	Associative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	addcomnni 42614	Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)
Theorem	mulassnni 42615	Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	mulcomnni 42616	Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	gcdcomnni 42617	Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)
Theorem	gcdnegnni 42618	Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)
Theorem	neggcdnni 42619	Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)
Theorem	bccl2d 42620	Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ)
Theorem	recbothd 42621	Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶)))
Theorem	gcdmultiplei 42622	The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀
Theorem	gcdaddmzz2nni 42623	Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))
Theorem	gcdaddmzz2nncomi 42624	Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))
Theorem	gcdnncli 42625	Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) ∈ ℕ
Theorem	muldvds1d 42626	If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ 𝑁)
Theorem	muldvds2d 42627	If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝑀 ∥ 𝑁)
Theorem	nndivdvdsd 42628	A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16309. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ))
Theorem	nnproddivdvdsd 42629	A product of natural numbers divides a natural number if and only if a factor divides the quotient, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 ↔ 𝐾 ∥ (𝑁 / 𝑀)))
Theorem	coprmdvds2d 42630	If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 gcd 𝑀) = 1)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    ⇒   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)
Theorem	imadomfi 42631	An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025.)
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐹) → (𝐹 “ 𝐴) ≼ 𝐴)
21.29.3  Some gcd and lcm results
Theorem	12gcd5e1 42632	The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;12 gcd 5) = 1
Theorem	60gcd6e6 42633	The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 gcd 6) = 6
Theorem	60gcd7e1 42634	The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 gcd 7) = 1
Theorem	420gcd8e4 42635	The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;;420 gcd 8) = 4
Theorem	lcmeprodgcdi 42636	Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐺 ∈ ℕ    &   ⊢ 𝐻 ∈ ℕ    &   ⊢ (𝑀 gcd 𝑁) = 𝐺    &   ⊢ (𝐺 · 𝐻) = 𝐴    &   ⊢ (𝑀 · 𝑁) = 𝐴    ⇒   ⊢ (𝑀 lcm 𝑁) = 𝐻
Theorem	12lcm5e60 42637	The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;12 lcm 5) = ;60
Theorem	60lcm6e60 42638	The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 lcm 6) = ;60
Theorem	60lcm7e420 42639	The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 lcm 7) = ;;420
Theorem	420lcm8e840 42640	The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;;420 lcm 8) = ;;840
Theorem	lcmfunnnd 42641	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 42642	Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...1)) = 1
Theorem	lcm2un 42643	Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...2)) = 2
Theorem	lcm3un 42644	Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...3)) = 6
Theorem	lcm4un 42645	Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...4)) = ;12
Theorem	lcm5un 42646	Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...5)) = ;60
Theorem	lcm6un 42647	Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...6)) = ;60
Theorem	lcm7un 42648	Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...7)) = ;;420
Theorem	lcm8un 42649	Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.)
⊢ (lcm‘(1...8)) = ;;840
21.29.4  Least common multiple inequality theorem
Theorem	3factsumint1 42650*	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 42651*	Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥)
Theorem	3factsumint3 42652*	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 42653*	Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥)
Theorem	3factsumint 42654*	Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.)
⊢ 𝐴 = (𝐿[,]𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥))
Theorem	resopunitintvd 42655	Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝐴) ∈ ((0(,)1)–cn→ℂ))
Theorem	resclunitintvd 42656	Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ ((0[,]1)–cn→ℂ))
Theorem	resdvopclptsd 42657*	Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ 𝐴)) = (𝑥 ∈ (0(,)1) ↦ 𝐵))
Theorem	lcmineqlem1 42658*	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 42659*	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 42660*	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 42661	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 42663. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    &   ⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀)))    ⇒   ⊢ (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ)
Theorem	lcmineqlem5 42662	Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶)))
Theorem	lcmineqlem6 42663*	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 42664	Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.)
⊢ (ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1)
Theorem	lcmineqlem8 42665*	Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))))
Theorem	lcmineqlem9 42666*	(1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ))
Theorem	lcmineqlem10 42667*	Induction step of lcmineqlem13 42670 (deduction form). (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥))
Theorem	lcmineqlem11 42668	Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀)))))
Theorem	lcmineqlem12 42669*	Base case for induction. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1))))
Theorem	lcmineqlem13 42670*	Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.)
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀))))
Theorem	lcmineqlem14 42671	Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷)    &   ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸)    &   ⊢ (𝜑 → 𝐷 ∥ 𝐸)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸)
Theorem	lcmineqlem15 42672*	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 42673	Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁)))
Theorem	lcmineqlem17 42674	Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
Theorem	lcmineqlem18 42675	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 42676	Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem20 42677	Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem21 42678	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 42679	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 42680	Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 9 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
Theorem	lcmineqlem 42681	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.29.5  Logarithm inequalities
Theorem	3exp7 42682	3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.)
⊢ (3↑7) = ;;;2187
Theorem	3lexlogpow5ineq1 42683	First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.)
⊢ 9 < ((;11 / 7)↑5)
Theorem	3lexlogpow5ineq2 42684	Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 3 ≤ 𝑋)    ⇒   ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5))
Theorem	3lexlogpow5ineq4 42685	Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 3 ≤ 𝑋)    ⇒   ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5))
Theorem	3lexlogpow5ineq3 42686	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 42687	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 42688	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 42689	Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
⊢ ((2 logb 3)↑5) ≤ ;15
21.29.6  Miscellaneous results for AKS formalisation
Theorem	intlewftc 42690*	Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃))    &   ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄)    &   ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴))    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵))
Theorem	aks4d1lem1 42691	Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵))
Theorem	aks4d1p1p1 42692*	Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘))
Theorem	dvrelog2 42693*	The derivative of the logarithm, ftc2 26164 version. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	dvrelog3 42694*	The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	dvrelog2b 42695*	Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	0nonelalab 42696	Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 0 ≠ 𝐶)
Theorem	dvrelogpow2b 42697*	Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑𝑁))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐶 · (((log‘𝑥)↑(𝑁 − 1)) / 𝑥)))    &   ⊢ 𝐶 = (𝑁 / ((log‘2)↑𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	aks4d1p1p3 42698	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 42699*	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 42700*	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↑𝐵))