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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lcmineqlem21 40401 | 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 40402 | 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 40403 | Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ 9 โค ๐) โ โข (๐ โ (2โ๐) โค (lcmโ(1...๐))) | ||
Theorem | lcmineqlem 40404 | 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...๐))) | ||
Theorem | 3exp7 40405 | 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.) |
โข (3โ7) = ;;;2187 | ||
Theorem | 3lexlogpow5ineq1 40406 | First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.) |
โข 9 < ((;11 / 7)โ5) | ||
Theorem | 3lexlogpow5ineq2 40407 | Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ 3 โค ๐) โ โข (๐ โ ((;11 / 7)โ5) โค ((2 logb ๐)โ5)) | ||
Theorem | 3lexlogpow5ineq4 40408 | Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ 3 โค ๐) โ โข (๐ โ 9 < ((2 logb ๐)โ5)) | ||
Theorem | 3lexlogpow5ineq3 40409 | 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 40410 | 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 40411 | 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 40412 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
โข ((2 logb 3)โ5) โค ;15 | ||
Theorem | intlewftc 40413* | Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐น โ ((๐ด[,]๐ต)โcnโโ)) & โข (๐ โ ๐บ โ ((๐ด[,]๐ต)โcnโโ)) & โข (๐ โ ๐ท = (โ D ๐น)) & โข (๐ โ ๐ธ = (โ D ๐บ)) & โข (๐ โ ๐ท โ ((๐ด(,)๐ต)โcnโโ)) & โข (๐ โ ๐ธ โ ((๐ด(,)๐ต)โcnโโ)) & โข (๐ โ ๐ท โ ๐ฟ1) & โข (๐ โ ๐ธ โ ๐ฟ1) & โข (๐ โ ๐ท = (๐ฅ โ (๐ด(,)๐ต) โฆ ๐)) & โข (๐ โ ๐ธ = (๐ฅ โ (๐ด(,)๐ต) โฆ ๐)) & โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ โค ๐) & โข (๐ โ (๐นโ๐ด) โค (๐บโ๐ด)) โ โข (๐ โ (๐นโ๐ต) โค (๐บโ๐ต)) | ||
Theorem | aks4d1lem1 40414 | Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.) |
โข (๐ โ ๐ โ (โคโฅโ3)) & โข ๐ต = (โโ((2 logb ๐)โ5)) โ โข (๐ โ (๐ต โ โ โง 9 < ๐ต)) | ||
Theorem | aks4d1p1p1 40415* | Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ โ โ) โ โข (๐ โ โ๐ โ (1...๐)(๐ดโ๐๐) = (๐ดโ๐ฮฃ๐ โ (1...๐)๐)) | ||
Theorem | dvrelog2 40416* | The derivative of the logarithm, ftc2 25330 version. (Contributed by metakunt, 11-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข ๐น = (๐ฅ โ (๐ด[,]๐ต) โฆ (logโ๐ฅ)) & โข ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / ๐ฅ)) โ โข (๐ โ (โ D ๐น) = ๐บ) | ||
Theorem | dvrelog3 40417* | The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข ๐น = (๐ฅ โ (๐ด(,)๐ต) โฆ (logโ๐ฅ)) & โข ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / ๐ฅ)) โ โข (๐ โ (โ D ๐น) = ๐บ) | ||
Theorem | dvrelog2b 40418* | Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข ๐น = (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ)) & โข ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2)))) โ โข (๐ โ (โ D ๐น) = ๐บ) | ||
Theorem | 0nonelalab 40419 | Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โ (๐ด(,)๐ต)) โ โข (๐ โ 0 โ ๐ถ) | ||
Theorem | dvrelogpow2b 40420* | Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข ๐น = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ๐)) & โข ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ))) & โข ๐ถ = (๐ / ((logโ2)โ๐)) & โข (๐ โ ๐ โ โ) โ โข (๐ โ (โ D ๐น) = ๐บ) | ||
Theorem | aks4d1p1p3 40421 | 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 40422* | 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 40423* | 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 40424* | Collapsed dvle 25293. (Contributed by metakunt, 19-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (๐ฅ โ (๐ด[,]๐ต) โฆ ๐ธ) โ ((๐ด[,]๐ต)โcnโโ)) & โข (๐ โ (๐ฅ โ (๐ด[,]๐ต) โฆ ๐บ) โ ((๐ด[,]๐ต)โcnโโ)) & โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ๐ธ)) = (๐ฅ โ (๐ด(,)๐ต) โฆ ๐น)) & โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ๐บ)) = (๐ฅ โ (๐ด(,)๐ต) โฆ ๐ป)) & โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐น โค ๐ป) & โข (๐ฅ = ๐ด โ ๐ธ = ๐) & โข (๐ฅ = ๐ด โ ๐บ = ๐) & โข (๐ฅ = ๐ต โ ๐ธ = ๐ ) & โข (๐ฅ = ๐ต โ ๐บ = ๐) & โข (๐ โ ๐ โค ๐) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ ๐ โค ๐) | ||
Theorem | aks4d1p1p6 40425* | 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 40426 | 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 40427* | 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 40428* | 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 40429 | 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 40430* | 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 40431* | 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 40432* | 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 40433* | 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 40434* | 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 40435* | 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 40436 | 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 40437 | 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 40438 | 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 40439* | 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 40440* | 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 40441* | 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 40442 | 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 40443* | 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 40444* | 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 40445 | The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.) |
โข (5C2) = ;10 | ||
Theorem | facp2 40446 | The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.) |
โข (๐ โ โ0 โ (!โ(๐ + 2)) = ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2)))) | ||
Theorem | 2np3bcnp1 40447 | Part of induction step for 2ap1caineq 40448. (Contributed by metakunt, 8-Jun-2024.) |
โข (๐ โ ๐ โ โ0) โ โข (๐ โ (((2 ยท (๐ + 1)) + 1)C(๐ + 1)) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) | ||
Theorem | 2ap1caineq 40448 | Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.) |
โข (๐ โ ๐ โ โค) & โข (๐ โ 2 โค ๐) โ โข (๐ โ (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐)) | ||
Theorem | sticksstones1 40449* | 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 40450* | 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 40451* | 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 40452* | Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.) |
โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐พ โ โ0) & โข ๐ต = {๐ โ ๐ซ (1...๐) โฃ (โฏโ๐) = ๐พ} & โข ๐ด = {๐ โฃ (๐:(1...๐พ)โถ(1...๐) โง โ๐ฅ โ (1...๐พ)โ๐ฆ โ (1...๐พ)(๐ฅ < ๐ฆ โ (๐โ๐ฅ) < (๐โ๐ฆ)))} โ โข (๐ โ ๐ด โ ๐ต) | ||
Theorem | sticksstones5 40453* | 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 40454* | 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 40455* | 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 40456* | 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 40457* | 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 40458* | 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 40459* | 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 40460* | 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 40461* | 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 40462* | 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 40463* | 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 40464* | 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 40465* | Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.) |
โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐พ โ โ) & โข ๐ด = {๐ โฃ (๐:(1...๐พ)โถโ0 โง ฮฃ๐ โ (1...๐พ)(๐โ๐) = ๐)} โ โข (๐ โ (โฏโ๐ด) = ((๐ + (๐พ โ 1))C(๐พ โ 1))) | ||
Theorem | sticksstones17 40466* | 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 40467* | 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 40468* | 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 40469* | 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 40470* | Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.) |
โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ โ ) & โข ๐ด = {๐ โฃ (๐:๐โถโ0 โง ฮฃ๐ โ ๐ (๐โ๐) = ๐)} โ โข (๐ โ (โฏโ๐ด) = ((๐ + ((โฏโ๐) โ 1))C((โฏโ๐) โ 1))) | ||
Theorem | sticksstones22 40471* | Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.) |
โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ โ ) & โข ๐ด = {๐ โฃ (๐:๐โถโ0 โง ฮฃ๐ โ ๐ (๐โ๐) โค ๐)} โ โข (๐ โ (โฏโ๐ด) = ((๐ + (โฏโ๐))C(โฏโ๐))) | ||
Theorem | metakunt1 40472* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) โ โข (๐ โ ๐ด:(1...๐)โถ(1...๐)) | ||
Theorem | metakunt2 40473* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐, ๐ผ, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ + 1)))) โ โข (๐ โ ๐ด:(1...๐)โถ(1...๐)) | ||
Theorem | metakunt3 40474* | Value of A. (Contributed by metakunt, 23-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข (๐ โ (๐ดโ๐) = if(๐ = ๐ผ, ๐, if(๐ < ๐ผ, ๐, (๐ โ 1)))) | ||
Theorem | metakunt4 40475* | Value of A. (Contributed by metakunt, 23-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐, ๐ผ, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข (๐ โ (๐ดโ๐) = if(๐ = ๐, ๐ผ, if(๐ < ๐ผ, ๐, (๐ + 1)))) | ||
Theorem | metakunt5 40476* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข ((๐ โง ๐ = ๐ผ) โ (๐ถโ(๐ดโ๐)) = ๐) | ||
Theorem | metakunt6 40477* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข ((๐ โง ๐ < ๐ผ) โ (๐ถโ(๐ดโ๐)) = ๐) | ||
Theorem | metakunt7 40478* | 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 40479* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข ((๐ โง ๐ผ < ๐) โ (๐ถโ(๐ดโ๐)) = ๐) | ||
Theorem | metakunt9 40480* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข (๐ โ (๐ถโ(๐ดโ๐)) = ๐) | ||
Theorem | metakunt10 40481* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข ((๐ โง ๐ = ๐) โ (๐ดโ(๐ถโ๐)) = ๐) | ||
Theorem | metakunt11 40482* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข ((๐ โง ๐ < ๐ผ) โ (๐ดโ(๐ถโ๐)) = ๐) | ||
Theorem | metakunt12 40483* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข ((๐ โง ยฌ (๐ = ๐ โจ ๐ < ๐ผ)) โ (๐ดโ(๐ถโ๐)) = ๐) | ||
Theorem | metakunt13 40484* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ด = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐ผ, ๐, if(๐ฅ < ๐ผ, ๐ฅ, (๐ฅ โ 1)))) & โข ๐ถ = (๐ฆ โ (1...๐) โฆ if(๐ฆ = ๐, ๐ผ, if(๐ฆ < ๐ผ, ๐ฆ, (๐ฆ + 1)))) & โข (๐ โ ๐ โ (1...๐)) โ โข (๐ โ (๐ดโ(๐ถโ๐)) = ๐) | ||
Theorem | metakunt14 40485* | 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 40486* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐น = (๐ฅ โ (1...(๐ผ โ 1)) โฆ (๐ฅ + (๐ โ ๐ผ))) โ โข (๐ โ ๐น:(1...(๐ผ โ 1))โ1-1-ontoโ(((๐ โ ๐ผ) + 1)...(๐ โ 1))) | ||
Theorem | metakunt16 40487* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐น = (๐ฅ โ (๐ผ...(๐ โ 1)) โฆ (๐ฅ + (1 โ ๐ผ))) โ โข (๐ โ ๐น:(๐ผ...(๐ โ 1))โ1-1-ontoโ(1...(๐ โ ๐ผ))) | ||
Theorem | metakunt17 40488 | 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 40489 | Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) โ โข (๐ โ ((((1...(๐ผ โ 1)) โฉ (๐ผ...(๐ โ 1))) = โ โง ((1...(๐ผ โ 1)) โฉ {๐}) = โ โง ((๐ผ...(๐ โ 1)) โฉ {๐}) = โ ) โง (((((๐ โ ๐ผ) + 1)...(๐ โ 1)) โฉ (1...(๐ โ ๐ผ))) = โ โง ((((๐ โ ๐ผ) + 1)...(๐ โ 1)) โฉ {๐}) = โ โง ((1...(๐ โ ๐ผ)) โฉ {๐}) = โ ))) | ||
Theorem | metakunt19 40490* | 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 40491* | 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 40492* | 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 40493* | 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 40494* | 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 40495 | Technical condition such that metakunt17 40488 holds. (Contributed by metakunt, 28-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) โ โข (๐ โ ((((1...(๐ผ โ 1)) โช (๐ผ...(๐ โ 1))) โฉ {๐}) = โ โง (1...๐) = (((1...(๐ผ โ 1)) โช (๐ผ...(๐ โ 1))) โช {๐}) โง (1...๐) = (((((๐ โ ๐ผ) + 1)...(๐ โ 1)) โช (1...(๐ โ ๐ผ))) โช {๐}))) | ||
Theorem | metakunt25 40496* | B is a permutation. (Contributed by metakunt, 28-May-2024.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ผ โ โ) & โข (๐ โ ๐ผ โค ๐) & โข ๐ต = (๐ฅ โ (1...๐) โฆ if(๐ฅ = ๐, ๐, if(๐ฅ < ๐ผ, (๐ฅ + (๐ โ ๐ผ)), (๐ฅ + (1 โ ๐ผ))))) โ โข (๐ โ ๐ต:(1...๐)โ1-1-ontoโ(1...๐)) | ||
Theorem | metakunt26 40497* | 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 40498* | 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 40499* | 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 40500* | 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) โ โข (๐ โ (๐ถโ(๐ตโ(๐ดโ๐))) = ((๐ + (๐ โ ๐ผ)) + ๐ป)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |