Home | Metamath
Proof Explorer Theorem List (p. 405 of 470) | < 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
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3lexlogpow2ineq1 40401 | 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 40402 | 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 40403 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
⊢ ((2 logb 3)↑5) ≤ ;15 | ||
Theorem | intlewftc 40404* | Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹)) & ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺)) & ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 ∈ 𝐿1) & ⊢ (𝜑 → 𝐸 ∈ 𝐿1) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)) & ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄) & ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) | ||
Theorem | aks4d1lem1 40405 | Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵)) | ||
Theorem | aks4d1p1p1 40406* | Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘)) | ||
Theorem | dvrelog2 40407* | The derivative of the logarithm, ftc2 25330 version. (Contributed by metakunt, 11-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | dvrelog3 40408* | The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | dvrelog2b 40409* | Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | 0nonelalab 40410 | Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → 0 ≠ 𝐶) | ||
Theorem | dvrelogpow2b 40411* | Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑𝑁)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐶 · (((log‘𝑥)↑(𝑁 − 1)) / 𝑥))) & ⊢ 𝐶 = (𝑁 / ((log‘2)↑𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | aks4d1p1p3 40412 | 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 40413* | 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 40414* | 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 40415* | Collapsed dvle 25293. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐺) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐸)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐹)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐺)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐻)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐹 ≤ 𝐻) & ⊢ (𝑥 = 𝐴 → 𝐸 = 𝑃) & ⊢ (𝑥 = 𝐴 → 𝐺 = 𝑄) & ⊢ (𝑥 = 𝐵 → 𝐸 = 𝑅) & ⊢ (𝑥 = 𝐵 → 𝐺 = 𝑆) & ⊢ (𝜑 → 𝑃 ≤ 𝑄) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝑅 ≤ 𝑆) | ||
Theorem | aks4d1p1p6 40416* | 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 40417 | 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 40418* | 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 40419* | 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 40420 | 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 40421* | 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 40422* | 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 40423* | 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 40424* | 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 40425* | 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 40426* | 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 40427 | 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 40428 | 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 40429 | 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 40430* | 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 40431* | 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 40432* | 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 40433 | 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 40434* | 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 40435* | 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 40436 | The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.) |
⊢ (5C2) = ;10 | ||
Theorem | facp2 40437 | The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.) |
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 2)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 2)))) | ||
Theorem | 2np3bcnp1 40438 | Part of induction step for 2ap1caineq 40439. (Contributed by metakunt, 8-Jun-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2))))) | ||
Theorem | 2ap1caineq 40439 | Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁)) | ||
Theorem | sticksstones1 40440* | 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 40441* | 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 40442* | 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 40443* | Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
Theorem | sticksstones5 40444* | 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 40445* | 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 40446* | 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 40447* | 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 40448* | 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 40449* | 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 40450* | 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 40451* | 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 40452* | 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 40453* | 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 40454* | 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 40455* | 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 40456* | Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1))) | ||
Theorem | sticksstones17 40457* | 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 40458* | 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 40459* | 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 40460* | 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 40461* | Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) | ||
Theorem | sticksstones22 40462* | Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))) | ||
Theorem | metakunt1 40463* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) ⇒ ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | ||
Theorem | metakunt2 40464* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) ⇒ ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | ||
Theorem | metakunt3 40465* | Value of A. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) | ||
Theorem | metakunt4 40466* | Value of A. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) | ||
Theorem | metakunt5 40467* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
Theorem | metakunt6 40468* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
Theorem | metakunt7 40469* | 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 40470* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
Theorem | metakunt9 40471* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
Theorem | metakunt10 40472* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
Theorem | metakunt11 40473* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
Theorem | metakunt12 40474* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ ¬ (𝑋 = 𝑀 ∨ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
Theorem | metakunt13 40475* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
Theorem | metakunt14 40476* | 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 40477* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1))) | ||
Theorem | metakunt16 40478* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) | ||
Theorem | metakunt17 40479 | The union of three disjoint bijections is a bijection. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋) & ⊢ (𝜑 → 𝐻:𝐵–1-1-onto→𝑌) & ⊢ (𝜑 → 𝐼:𝐶–1-1-onto→𝑍) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅) & ⊢ (𝜑 → (𝑋 ∩ 𝑌) = ∅) & ⊢ (𝜑 → (𝑋 ∩ 𝑍) = ∅) & ⊢ (𝜑 → (𝑌 ∩ 𝑍) = ∅) & ⊢ (𝜑 → 𝐹 = ((𝐺 ∪ 𝐻) ∪ 𝐼)) & ⊢ (𝜑 → 𝐷 = ((𝐴 ∪ 𝐵) ∪ 𝐶)) & ⊢ (𝜑 → 𝑊 = ((𝑋 ∪ 𝑌) ∪ 𝑍)) ⇒ ⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝑊) | ||
Theorem | metakunt18 40480 | Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | ||
Theorem | metakunt19 40481* | Domains on restrictions of functions. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) & ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) ⇒ ⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {⟨𝑀, 𝑀⟩} Fn {𝑀})) | ||
Theorem | metakunt20 40482* | Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) & ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝑋 = 𝑀) ⇒ ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋)) | ||
Theorem | metakunt21 40483* | Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) & ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ (𝜑 → ¬ 𝑋 = 𝑀) & ⊢ (𝜑 → 𝑋 < 𝐼) ⇒ ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋)) | ||
Theorem | metakunt22 40484* | Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) & ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ (𝜑 → ¬ 𝑋 = 𝑀) & ⊢ (𝜑 → ¬ 𝑋 < 𝐼) ⇒ ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋)) | ||
Theorem | metakunt23 40485* | B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) & ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋)) | ||
Theorem | metakunt24 40486 | Technical condition such that metakunt17 40479 holds. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) | ||
Theorem | metakunt25 40487* | B is a permutation. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) ⇒ ⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) | ||
Theorem | metakunt26 40488* | Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ (𝜑 → 𝑋 = 𝐼) ⇒ ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑋) | ||
Theorem | metakunt27 40489* | Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ (𝜑 → ¬ 𝑋 = 𝐼) & ⊢ (𝜑 → 𝑋 < 𝐼) ⇒ ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼))) | ||
Theorem | metakunt28 40490* | Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ (𝜑 → ¬ 𝑋 = 𝐼) & ⊢ (𝜑 → ¬ 𝑋 < 𝐼) ⇒ ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 − 𝐼)) | ||
Theorem | metakunt29 40491* | Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ (𝜑 → ¬ 𝑋 = 𝐼) & ⊢ (𝜑 → 𝑋 < 𝐼) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ⇒ ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | ||
Theorem | metakunt30 40492* | Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ (𝜑 → ¬ 𝑋 = 𝐼) & ⊢ (𝜑 → ¬ 𝑋 < 𝐼) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) ⇒ ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 − 𝐼) + 𝐻)) | ||
Theorem | metakunt31 40493* | Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) & ⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) & ⊢ 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) ⇒ ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑅) | ||
Theorem | metakunt32 40494* | Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) & ⊢ 𝐷 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0))))) & ⊢ 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) & ⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) & ⊢ 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = 𝑅) | ||
Theorem | metakunt33 40495* | Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ 𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0))))) ⇒ ⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)) = 𝐷) | ||
Theorem | metakunt34 40496* | 𝐷 is a permutation. (Contributed by metakunt, 18-Jul-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0))))) ⇒ ⊢ (𝜑 → 𝐷:(1...𝑀)–1-1-onto→(1...𝑀)) | ||
Theorem | andiff 40497 | Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024.) |
⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜓 → (𝜃 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | ||
Theorem | fac2xp3 40498 | Factorial of 2x+3, sublemma for sublemma for AKS. (Contributed by metakunt, 19-Apr-2024.) |
⊢ (𝑥 ∈ ℕ0 → (!‘((2 · 𝑥) + 3)) = ((!‘((2 · 𝑥) + 1)) · (((2 · 𝑥) + 2) · ((2 · 𝑥) + 3)))) | ||
Theorem | prodsplit 40499* | Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 𝐾))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 𝐾))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...(𝑁 + 𝐾))𝐴)) | ||
Theorem | 2xp3dxp2ge1d 40500 | 2x+3 is greater than or equal to x+2 for x >= -1, a deduction version (Contributed by metakunt, 21-Apr-2024.) |
⊢ (𝜑 → 𝑋 ∈ (-1[,)+∞)) ⇒ ⊢ (𝜑 → 1 ≤ (((2 · 𝑋) + 3) / (𝑋 + 2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |