P. 410 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40901-41000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcmineqlem8 40901*	Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))))
Theorem	lcmineqlem9 40902*	(1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ))
Theorem	lcmineqlem10 40903*	Induction step of lcmineqlem13 40906 (deduction form). (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥))
Theorem	lcmineqlem11 40904	Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀)))))
Theorem	lcmineqlem12 40905*	Base case for induction. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1))))
Theorem	lcmineqlem13 40906*	Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.)
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀))))
Theorem	lcmineqlem14 40907	Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷)    &   ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸)    &   ⊢ (𝜑 → 𝐷 ∥ 𝐸)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸)
Theorem	lcmineqlem15 40908*	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 40909	Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁)))
Theorem	lcmineqlem17 40910	Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
Theorem	lcmineqlem18 40911	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 40912	Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem20 40913	Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
Theorem	lcmineqlem21 40914	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 40915	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 40916	Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 9 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
Theorem	lcmineqlem 40917	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.4  Logarithm inequalities
Theorem	3exp7 40918	3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.)
⊢ (3↑7) = ;;;2187
Theorem	3lexlogpow5ineq1 40919	First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.)
⊢ 9 < ((;11 / 7)↑5)
Theorem	3lexlogpow5ineq2 40920	Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 3 ≤ 𝑋)    ⇒   ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5))
Theorem	3lexlogpow5ineq4 40921	Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 3 ≤ 𝑋)    ⇒   ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5))
Theorem	3lexlogpow5ineq3 40922	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 40923	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 40924	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 40925	Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.)
⊢ ((2 logb 3)↑5) ≤ ;15
21.27.5  Miscellaneous results for AKS formalisation
Theorem	intlewftc 40926*	Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹))    &   ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺))    &   ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃))    &   ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄)    &   ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴))    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵))
Theorem	aks4d1lem1 40927	Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵))
Theorem	aks4d1p1p1 40928*	Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘))
Theorem	dvrelog2 40929*	The derivative of the logarithm, ftc2 25561 version. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	dvrelog3 40930*	The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	dvrelog2b 40931*	Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	0nonelalab 40932	Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 0 ≠ 𝐶)
Theorem	dvrelogpow2b 40933*	Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑𝑁))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐶 · (((log‘𝑥)↑(𝑁 − 1)) / 𝑥)))    &   ⊢ 𝐶 = (𝑁 / ((log‘2)↑𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)
Theorem	aks4d1p1p3 40934	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 40935*	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 40936*	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 40937*	Collapsed dvle 25524. (Contributed by metakunt, 19-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐺) ∈ ((𝐴[,]𝐵)–cn→ℝ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐸)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐹))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐺)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐻))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐹 ≤ 𝐻)    &   ⊢ (𝑥 = 𝐴 → 𝐸 = 𝑃)    &   ⊢ (𝑥 = 𝐴 → 𝐺 = 𝑄)    &   ⊢ (𝑥 = 𝐵 → 𝐸 = 𝑅)    &   ⊢ (𝑥 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑄)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝑅 ≤ 𝑆)
Theorem	aks4d1p1p6 40938*	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 40939	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 40940*	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 40941*	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 40942	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 40943*	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 40944*	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 40945*	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 40946*	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 40947*	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 40948*	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 40949	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 40950	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 40951	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 40952*	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 40953*	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 40954*	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 40955	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→𝐵)
Theorem	aks6d1c2p1 40956*	In the AKS-theorem the subset defined by 𝐸 takes values in the positive integers. (Contributed by metakunt, 7-Jan-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))    ⇒   ⊢ (𝜑 → 𝐸:(ℕ0 × ℕ0)⟶ℕ)
Theorem	aks6d1c2p2 40957*	Injective condition for countability argument assuming that 𝑁 is not a prime power. (Contributed by metakunt, 7-Jan-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   ⊢ (𝜑 → 𝑄 ∈ ℙ)    &   ⊢ (𝜑 → 𝑄 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝐸:(ℕ0 × ℕ0)–1-1→ℕ)
Theorem	5bc2eq10 40958	The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.)
⊢ (5C2) = ;10
Theorem	facp2 40959	The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.)
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 2)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 2))))
Theorem	2np3bcnp1 40960	Part of induction step for 2ap1caineq 40961. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2)))))
Theorem	2ap1caineq 40961	Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁))
21.27.6  Sticks and stones
Theorem	sticksstones1 40962*	Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )    ⇒   ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌)
Theorem	sticksstones2 40963*	The range function on strictly monotone functions with finite domain and codomain is an injective mapping onto 𝐾-elemental sets. (Contributed by metakunt, 27-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    &   ⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)
Theorem	sticksstones3 40964*	The range function on strictly monotone functions with finite domain and codomain is an surjective mapping onto 𝐾-elemental sets. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    &   ⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵)
Theorem	sticksstones4 40965*	Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐴 ≈ 𝐵)
Theorem	sticksstones5 40966*	Count the number of strictly monotonely increasing functions on finite domains and codomains. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = (𝑁C𝐾))
Theorem	sticksstones6 40967*	Function induces an order isomorphism for sticks and stones theorem. (Contributed by metakunt, 1-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺:(1...(𝐾 + 1))⟶ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝐾))    &   ⊢ (𝜑 → 𝑌 ∈ (1...𝐾))    &   ⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) < (𝐹‘𝑌))
Theorem	sticksstones7 40968*	Closure property of sticks and stones function. (Contributed by metakunt, 1-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺:(1...(𝐾 + 1))⟶ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝐾))    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)))    &   ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = 𝑁)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ∈ (1...(𝑁 + 𝐾)))
Theorem	sticksstones8 40969*	Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 1-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
Theorem	sticksstones9 40970*	Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 = 0)    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	sticksstones10 40971*	Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	sticksstones11 40972*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 = 0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones12a 40973*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 11-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑)
Theorem	sticksstones12 40974*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones13 40975*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones14 40976*	Sticks and stones with definitions as hypotheses. (Contributed by metakunt, 7-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + 𝐾)C𝐾))
Theorem	sticksstones15 40977*	Sticks and stones with almost collapsed definitions for positive integers. (Contributed by metakunt, 7-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + 𝐾)C𝐾))
Theorem	sticksstones16 40978*	Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
Theorem	sticksstones17 40979*	Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))))    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	sticksstones18 40980*	Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
Theorem	sticksstones19 40981*	Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))))    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones20 40982*	Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → (♯‘𝑆) = 𝐾)    ⇒   ⊢ (𝜑 → (♯‘𝐵) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
Theorem	sticksstones21 40983*	Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
Theorem	sticksstones22 40984*	Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
21.27.7  Permutation results
Theorem	metakunt1 40985*	A is an endomapping. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    ⇒   ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀))
Theorem	metakunt2 40986*	A is an endomapping. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))))    ⇒   ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀))
Theorem	metakunt3 40987*	Value of A. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))))
Theorem	metakunt4 40988*	Value of A. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))))
Theorem	metakunt5 40989*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt6 40990*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt7 40991*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) = (𝑋 − 1) ∧ ¬ (𝐴‘𝑋) = 𝑀 ∧ ¬ (𝐴‘𝑋) < 𝐼))
Theorem	metakunt8 40992*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt9 40993*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt10 40994*	C is the right inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt11 40995*	C is the right inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt12 40996*	C is the right inverse for A. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ ¬ (𝑋 = 𝑀 ∨ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt13 40997*	C is the right inverse for A. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt14 40998*	A is a primitive permutation that moves the I-th element to the end and C is its inverse that moves the last element back to the I-th position. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    ⇒   ⊢ (𝜑 → (𝐴:(1...𝑀)–1-1-onto→(1...𝑀) ∧ ◡𝐴 = 𝐶))
Theorem	metakunt15 40999*	Construction of another permutation. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    ⇒   ⊢ (𝜑 → 𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1)))
Theorem	metakunt16 41000*	Construction of another permutation. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    ⇒   ⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼)))