![]() |
Metamath
Proof Explorer Theorem List (p. 474 of 479) | < 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: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nn0mullong 47301* | Standard algorithm (also known as "long multiplication" or "grade-school multiplication") to calculate the product of two nonnegative integers π and π by multiplying the multiplicand π by each digit of the multiplier π and then add up all the properly shifted results. Here, the binary representation of the multiplier π is used, i.e., the above mentioned "digits" are 0 or 1. This is a similar result as provided by smumul 16433. (Contributed by AV, 7-Jun-2020.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ Β· π΅) = Ξ£π β (0..^(#bβπ΄))(((π(digitβ2)π΄) Β· (2βπ)) Β· π΅)) | ||
According to Wikipedia ("Arity", https://en.wikipedia.org/wiki/Arity, 19-May-2024): "In logic, mathematics, and computer science, arity is the number of arguments or operands taken by a function, operation or relation." N-ary functions are often also called multivariate functions, without indicating the actual number of argumens. See also Wikipedia ("Multivariate functions", 19-May-2024, https://en.wikipedia.org/wiki/Function_(mathematics)#Multivariate_functions ): "A multivariate function, multivariable function, or function of several variables is a function that depends on several arguments. ... Formally, a function of n variables is a function whose domain is a set of n-tuples. For example, multiplication of integers is a function of two variables, or bivariate function, whose domain is the set of all ordered pairs (2-tuples) of integers, and whose codomain is the set of integers. The same is true for every binary operation. Commonly, an n-tuple is denoted enclosed between parentheses, such as in ( 1 , 2 , ... , n ). When using functional notation, one usually omits the parentheses surrounding tuples, writing f ( x1 , ... , xn ) instead of f ( ( x1 , ... , xn ) ). Given n sets X1 , ... , Xn , the set of all n-tuples ( x1 , ... , xn ) such that x1 is element of X1 , ... , xn is element of Xn is called the Cartesian product of X1 , ... , Xn , and denoted X1 X ... X Xn . Therefore, a multivariate function is a function that has a Cartesian product or a proper subset of a Cartesian product as a domain: π:πβΆπ where where the domain π has the form π β ((...((πβ1) Γ (πβ2)) Γ ...) Γ (πβπ))." In the following, n-ary functions are defined as mappings (see df-map 8821) from a finite sequence of arguments, which themselves are defined as mappings from the half-open range of nonnegative integers to the domain of each argument. Furthermore, the definition is restricted to endofunctions, meaning that the domain(s) of the argument(s) is identical with its codomain. This means that the domains of all arguments are identical (in contrast to the definition in Wikipedia, see above: here, we have X1 = X2 = ... = Xn = X). For small n, n-ary functions correspond to "usual" functions with a different number of arguments: - n = 0 (nullary functions): These correspond actually to constants, see 0aryfvalelfv 47311 and mapsn 8881: (π βm {β }) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 47321 and efmndbas 18751: (π βm π) - n = 2 (binary functions): These correspond to usual operations on two elements of the same set, also called "binary operation" (according to Wikipedia ("Binary operation", 19-May-2024, https://en.wikipedia.org/wiki/Binary_operation 18751): "In mathematics, a binary operation or dyadic operation is a rule for combining two elements (called operands) to produce another element. More formally, a binary operation is an operation of arity two. More specifically, a binary operation on a set is a binary operation whose two domains and the codomain are the same set." Sometimes also called "closed internal binary operation"), see 2aryenef 47332 and compare with df-clintop 46600: (π βm (π Γ π)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (πββπ) (see df-finxp 36260) could have been used to represent multiple arguments. However, this concept is not fully developed yet (it is within a mathbox), and it is currently based on ordinal numbers, e.g., (πββ2o), instead of integers, e.g., (πββ2), which is not very practical. The definition df-ixp of infinite Cartesian product could also have been used to represent multiple arguments, but this would have been more cumbersome without any additional advantage. naryfvalixp 47305 shows that both definitions are equivalent. | ||
Syntax | cnaryf 47302 | Extend the definition of a class to include the n-ary functions. |
class -aryF | ||
Definition | df-naryf 47303* | Define the n-ary (endo)functions. (Contributed by AV, 11-May-2024.) (Revised by TA and SN, 7-Jun-2024.) |
β’ -aryF = (π β β0, π₯ β V β¦ (π₯ βm (π₯ βm (0..^π)))) | ||
Theorem | naryfval 47304 | The set of the n-ary (endo)functions on a class π. (Contributed by AV, 13-May-2024.) |
β’ πΌ = (0..^π) β β’ (π β β0 β (π-aryF π) = (π βm (π βm πΌ))) | ||
Theorem | naryfvalixp 47305* | The set of the n-ary (endo)functions on a class π expressed with the notation of infinite Cartesian products. (Contributed by AV, 19-May-2024.) |
β’ πΌ = (0..^π) β β’ (π β β0 β (π-aryF π) = (π βm Xπ₯ β πΌ π)) | ||
Theorem | naryfvalel 47306 | An n-ary (endo)function on a set π. (Contributed by AV, 14-May-2024.) |
β’ πΌ = (0..^π) β β’ ((π β β0 β§ π β π) β (πΉ β (π-aryF π) β πΉ:(π βm πΌ)βΆπ)) | ||
Theorem | naryrcl 47307 | Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.) |
β’ πΌ = (0..^π) β β’ (πΉ β (π-aryF π) β (π β β0 β§ π β V)) | ||
Theorem | naryfvalelfv 47308 | The value of an n-ary (endo)function on a set π is an element of π. (Contributed by AV, 14-May-2024.) |
β’ πΌ = (0..^π) β β’ ((πΉ β (π-aryF π) β§ π΄:πΌβΆπ) β (πΉβπ΄) β π) | ||
Theorem | naryfvalelwrdf 47309* | An n-ary (endo)function on a set π expressed as a function over the set of words on π of length π. (Contributed by AV, 4-Jun-2024.) |
β’ ((π β β0 β§ π β π) β (πΉ β (π-aryF π) β πΉ:{π€ β Word π β£ (β―βπ€) = π}βΆπ)) | ||
Theorem | 0aryfvalel 47310* | A nullary (endo)function on a set π is a singleton of an ordered pair with the empty set as first component. A nullary function represents a constant: (πΉββ ) = πΆ with πΆ β π, see also 0aryfvalelfv 47311. Instead of (πΉββ ), nullary functions are usually written as πΉ() in literature. (Contributed by AV, 15-May-2024.) |
β’ (π β π β (πΉ β (0-aryF π) β βπ₯ β π πΉ = {β¨β , π₯β©})) | ||
Theorem | 0aryfvalelfv 47311* | The value of a nullary (endo)function on a set π. (Contributed by AV, 19-May-2024.) |
β’ (πΉ β (0-aryF π) β βπ₯ β π (πΉββ ) = π₯) | ||
Theorem | 1aryfvalel 47312 | A unary (endo)function on a set π. (Contributed by AV, 15-May-2024.) |
β’ (π β π β (πΉ β (1-aryF π) β πΉ:(π βm {0})βΆπ)) | ||
Theorem | fv1arycl 47313 | Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.) |
β’ ((πΊ β (1-aryF π) β§ π΄ β π) β (πΊβ{β¨0, π΄β©}) β π) | ||
Theorem | 1arympt1 47314* | A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
β’ πΉ = (π₯ β (π βm {0}) β¦ (π΄β(π₯β0))) β β’ ((π β π β§ π΄:πβΆπ) β πΉ β (1-aryF π)) | ||
Theorem | 1arympt1fv 47315* | The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
β’ πΉ = (π₯ β (π βm {0}) β¦ (π΄β(π₯β0))) β β’ ((π β π β§ π΅ β π) β (πΉβ{β¨0, π΅β©}) = (π΄βπ΅)) | ||
Theorem | 1arymaptfv 47316* | The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.) |
β’ π» = (β β (1-aryF π) β¦ (π₯ β π β¦ (ββ{β¨0, π₯β©}))) β β’ (πΉ β (1-aryF π) β (π»βπΉ) = (π₯ β π β¦ (πΉβ{β¨0, π₯β©}))) | ||
Theorem | 1arymaptf 47317* | The mapping of unary (endo)functions is a function into the set of endofunctions. (Contributed by AV, 18-May-2024.) |
β’ π» = (β β (1-aryF π) β¦ (π₯ β π β¦ (ββ{β¨0, π₯β©}))) β β’ (π β π β π»:(1-aryF π)βΆ(π βm π)) | ||
Theorem | 1arymaptf1 47318* | The mapping of unary (endo)functions is a one-to-one function into the set of endofunctions. (Contributed by AV, 19-May-2024.) |
β’ π» = (β β (1-aryF π) β¦ (π₯ β π β¦ (ββ{β¨0, π₯β©}))) β β’ (π β π β π»:(1-aryF π)β1-1β(π βm π)) | ||
Theorem | 1arymaptfo 47319* | The mapping of unary (endo)functions is a function onto the set of endofunctions. (Contributed by AV, 18-May-2024.) |
β’ π» = (β β (1-aryF π) β¦ (π₯ β π β¦ (ββ{β¨0, π₯β©}))) β β’ (π β π β π»:(1-aryF π)βontoβ(π βm π)) | ||
Theorem | 1arymaptf1o 47320* | The mapping of unary (endo)functions is a one-to-one function onto the set of endofunctions. (Contributed by AV, 19-May-2024.) |
β’ π» = (β β (1-aryF π) β¦ (π₯ β π β¦ (ββ{β¨0, π₯β©}))) β β’ (π β π β π»:(1-aryF π)β1-1-ontoβ(π βm π)) | ||
Theorem | 1aryenef 47321 | The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.) |
β’ (1-aryF π) β (π βm π) | ||
Theorem | 1aryenefmnd 47322 | The set of unary (endo)functions and the base set of the monoid of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.) |
β’ (1-aryF π) β (Baseβ(EndoFMndβπ)) | ||
Theorem | 2aryfvalel 47323 | A binary (endo)function on a set π. (Contributed by AV, 20-May-2024.) |
β’ (π β π β (πΉ β (2-aryF π) β πΉ:(π βm {0, 1})βΆπ)) | ||
Theorem | fv2arycl 47324 | Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.) |
β’ ((πΊ β (2-aryF π) β§ π΄ β π β§ π΅ β π) β (πΊβ{β¨0, π΄β©, β¨1, π΅β©}) β π) | ||
Theorem | 2arympt 47325* | A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.) |
β’ πΉ = (π₯ β (π βm {0, 1}) β¦ ((π₯β0)π(π₯β1))) β β’ ((π β π β§ π:(π Γ π)βΆπ) β πΉ β (2-aryF π)) | ||
Theorem | 2arymptfv 47326* | The value of a binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.) |
β’ πΉ = (π₯ β (π βm {0, 1}) β¦ ((π₯β0)π(π₯β1))) β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (πΉβ{β¨0, π΄β©, β¨1, π΅β©}) = (π΄ππ΅)) | ||
Theorem | 2arymaptfv 47327* | The value of the mapping of binary (endo)functions. (Contributed by AV, 21-May-2024.) |
β’ π» = (β β (2-aryF π) β¦ (π₯ β π, π¦ β π β¦ (ββ{β¨0, π₯β©, β¨1, π¦β©}))) β β’ (πΉ β (2-aryF π) β (π»βπΉ) = (π₯ β π, π¦ β π β¦ (πΉβ{β¨0, π₯β©, β¨1, π¦β©}))) | ||
Theorem | 2arymaptf 47328* | The mapping of binary (endo)functions is a function into the set of binary operations. (Contributed by AV, 21-May-2024.) |
β’ π» = (β β (2-aryF π) β¦ (π₯ β π, π¦ β π β¦ (ββ{β¨0, π₯β©, β¨1, π¦β©}))) β β’ (π β π β π»:(2-aryF π)βΆ(π βm (π Γ π))) | ||
Theorem | 2arymaptf1 47329* | The mapping of binary (endo)functions is a one-to-one function into the set of binary operations. (Contributed by AV, 22-May-2024.) |
β’ π» = (β β (2-aryF π) β¦ (π₯ β π, π¦ β π β¦ (ββ{β¨0, π₯β©, β¨1, π¦β©}))) β β’ (π β π β π»:(2-aryF π)β1-1β(π βm (π Γ π))) | ||
Theorem | 2arymaptfo 47330* | The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-May-2024.) |
β’ π» = (β β (2-aryF π) β¦ (π₯ β π, π¦ β π β¦ (ββ{β¨0, π₯β©, β¨1, π¦β©}))) β β’ (π β π β π»:(2-aryF π)βontoβ(π βm (π Γ π))) | ||
Theorem | 2arymaptf1o 47331* | The mapping of binary (endo)functions is a one-to-one function onto the set of binary operations. (Contributed by AV, 23-May-2024.) |
β’ π» = (β β (2-aryF π) β¦ (π₯ β π, π¦ β π β¦ (ββ{β¨0, π₯β©, β¨1, π¦β©}))) β β’ (π β π β π»:(2-aryF π)β1-1-ontoβ(π βm (π Γ π))) | ||
Theorem | 2aryenef 47332 | The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.) |
β’ (2-aryF π) β (π βm (π Γ π)) | ||
According to Wikipedia ("Ackermann function", 8-May-2024, https://en.wikipedia.org/wiki/Ackermann_function): "In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. ... One common version is the two-argument Ackermann-PΓ©ter function developed by RΓ³zsa PΓ©ter and Raphael Robinson. Its value grows very rapidly; for example, A(4,2) results in 2^65536-3 [see ackval42 47372)], an integer of 19,729 decimal digits." In the following, the Ackermann function is defined as iterated 1-ary function (also mentioned in Wikipedia), see df-ack 47336, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 47335. As an illustration, we have ((IterCompβπΉ)β3) = (πΉ β (πΉ β πΉ))) (see itcoval3 47341). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 47336: ((Ackβ(π + 1))βπ) = (((IterCompβ(Ackβπ))β(π + 1))β1)). That Definition df-ack 47336 is equivalent to PΓ©ter's definition is proven by the following three theorems: ackval0val 47362: ((Ackβ0)βπ) = (π + 1); ackvalsuc0val 47363: ((Ackβ(π + 1))β0) = ((Ackβπ)β1); ackvalsucsucval 47364: ((Ackβ(π + 1))β(π + 1)) = ((Ackβπ)β((Ackβ(π + 1))βπ)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 47365: π΄(0, 0) = 1, π΄(0, 1) = 2, π΄(0, 2) = 3; ackval1012 47366: π΄(1, 0) = 2, π΄(1, 1) = 3, π΄(1, 3) = 4; ackval2012 47367: π΄(2, 0) = 3, π΄(2, 1) = 5, π΄(2, 3) = 7; ackval3012 47368: π΄(3, 0) = 5, π΄(3, 1) = ;13, π΄(3, 3) = ;29. | ||
Syntax | citco 47333 | Extend the definition of a class to include iterated functions. |
class IterComp | ||
Syntax | cack 47334 | Extend the definition of a class to include the Ackermann function operator. |
class Ack | ||
Definition | df-itco 47335* | Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.) |
β’ IterComp = (π β V β¦ seq0((π β V, π β V β¦ (π β π)), (π β β0 β¦ if(π = 0, ( I βΎ dom π), π)))) | ||
Definition | df-ack 47336* | Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.) |
β’ Ack = seq0((π β V, π β V β¦ (π β β0 β¦ (((IterCompβπ)β(π + 1))β1))), (π β β0 β¦ if(π = 0, (π β β0 β¦ (π + 1)), π))) | ||
Theorem | itcoval 47337* | The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024.) |
β’ (πΉ β π β (IterCompβπΉ) = seq0((π β V, π β V β¦ (πΉ β π)), (π β β0 β¦ if(π = 0, ( I βΎ dom πΉ), πΉ)))) | ||
Theorem | itcoval0 47338 | A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.) |
β’ (πΉ β π β ((IterCompβπΉ)β0) = ( I βΎ dom πΉ)) | ||
Theorem | itcoval1 47339 | A function iterated once. (Contributed by AV, 2-May-2024.) |
β’ ((Rel πΉ β§ πΉ β π) β ((IterCompβπΉ)β1) = πΉ) | ||
Theorem | itcoval2 47340 | A function iterated twice. (Contributed by AV, 2-May-2024.) |
β’ ((Rel πΉ β§ πΉ β π) β ((IterCompβπΉ)β2) = (πΉ β πΉ)) | ||
Theorem | itcoval3 47341 | A function iterated three times. (Contributed by AV, 2-May-2024.) |
β’ ((Rel πΉ β§ πΉ β π) β ((IterCompβπΉ)β3) = (πΉ β (πΉ β πΉ))) | ||
Theorem | itcoval0mpt 47342* | A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β π΄ β¦ π΅) β β’ ((π΄ β π β§ βπ β π΄ π΅ β π) β ((IterCompβπΉ)β0) = (π β π΄ β¦ π)) | ||
Theorem | itcovalsuc 47343* | The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.) |
β’ ((πΉ β π β§ π β β0 β§ ((IterCompβπΉ)βπ) = πΊ) β ((IterCompβπΉ)β(π + 1)) = (πΊ(π β V, π β V β¦ (πΉ β π))πΉ)) | ||
Theorem | itcovalsucov 47344 | The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.) |
β’ ((πΉ β π β§ π β β0 β§ ((IterCompβπΉ)βπ) = πΊ) β ((IterCompβπΉ)β(π + 1)) = (πΉ β πΊ)) | ||
Theorem | itcovalendof 47345 | The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΄) & β’ (π β π β β0) β β’ (π β ((IterCompβπΉ)βπ):π΄βΆπ΄) | ||
Theorem | itcovalpclem1 47346* | Lemma 1 for itcovalpc 47348: induction basis. (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β β0 β¦ (π + πΆ)) β β’ (πΆ β β0 β ((IterCompβπΉ)β0) = (π β β0 β¦ (π + (πΆ Β· 0)))) | ||
Theorem | itcovalpclem2 47347* | Lemma 2 for itcovalpc 47348: induction step. (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β β0 β¦ (π + πΆ)) β β’ ((π¦ β β0 β§ πΆ β β0) β (((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦))) β ((IterCompβπΉ)β(π¦ + 1)) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1)))))) | ||
Theorem | itcovalpc 47348* | The value of the function that returns the n-th iterate of the "plus a constant" function with regard to composition. (Contributed by AV, 4-May-2024.) |
β’ πΉ = (π β β0 β¦ (π + πΆ)) β β’ ((πΌ β β0 β§ πΆ β β0) β ((IterCompβπΉ)βπΌ) = (π β β0 β¦ (π + (πΆ Β· πΌ)))) | ||
Theorem | itcovalt2lem2lem1 47349 | Lemma 1 for itcovalt2lem2 47352. (Contributed by AV, 6-May-2024.) |
β’ (((π β β β§ πΆ β β0) β§ π β β0) β (((π + πΆ) Β· π) β πΆ) β β0) | ||
Theorem | itcovalt2lem2lem2 47350 | Lemma 2 for itcovalt2lem2 47352. (Contributed by AV, 7-May-2024.) |
β’ (((π β β0 β§ πΆ β β0) β§ π β β0) β ((2 Β· (((π + πΆ) Β· (2βπ)) β πΆ)) + πΆ) = (((π + πΆ) Β· (2β(π + 1))) β πΆ)) | ||
Theorem | itcovalt2lem1 47351* | Lemma 1 for itcovalt2 47353: induction basis. (Contributed by AV, 5-May-2024.) |
β’ πΉ = (π β β0 β¦ ((2 Β· π) + πΆ)) β β’ (πΆ β β0 β ((IterCompβπΉ)β0) = (π β β0 β¦ (((π + πΆ) Β· (2β0)) β πΆ))) | ||
Theorem | itcovalt2lem2 47352* | Lemma 2 for itcovalt2 47353: induction step. (Contributed by AV, 7-May-2024.) |
β’ πΉ = (π β β0 β¦ ((2 Β· π) + πΆ)) β β’ ((π¦ β β0 β§ πΆ β β0) β (((IterCompβπΉ)βπ¦) = (π β β0 β¦ (((π + πΆ) Β· (2βπ¦)) β πΆ)) β ((IterCompβπΉ)β(π¦ + 1)) = (π β β0 β¦ (((π + πΆ) Β· (2β(π¦ + 1))) β πΆ)))) | ||
Theorem | itcovalt2 47353* | The value of the function that returns the n-th iterate of the "times 2 plus a constant" function with regard to composition. (Contributed by AV, 7-May-2024.) |
β’ πΉ = (π β β0 β¦ ((2 Β· π) + πΆ)) β β’ ((πΌ β β0 β§ πΆ β β0) β ((IterCompβπΉ)βπΌ) = (π β β0 β¦ (((π + πΆ) Β· (2βπΌ)) β πΆ))) | ||
Theorem | ackvalsuc1mpt 47354* | The Ackermann function at a successor of the first argument as a mapping of the second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.) |
β’ (π β β0 β (Ackβ(π + 1)) = (π β β0 β¦ (((IterCompβ(Ackβπ))β(π + 1))β1))) | ||
Theorem | ackvalsuc1 47355 | The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.) |
β’ ((π β β0 β§ π β β0) β ((Ackβ(π + 1))βπ) = (((IterCompβ(Ackβπ))β(π + 1))β1)) | ||
Theorem | ackval0 47356 | The Ackermann function at 0. (Contributed by AV, 2-May-2024.) |
β’ (Ackβ0) = (π β β0 β¦ (π + 1)) | ||
Theorem | ackval1 47357 | The Ackermann function at 1. (Contributed by AV, 4-May-2024.) |
β’ (Ackβ1) = (π β β0 β¦ (π + 2)) | ||
Theorem | ackval2 47358 | The Ackermann function at 2. (Contributed by AV, 4-May-2024.) |
β’ (Ackβ2) = (π β β0 β¦ ((2 Β· π) + 3)) | ||
Theorem | ackval3 47359 | The Ackermann function at 3. (Contributed by AV, 7-May-2024.) |
β’ (Ackβ3) = (π β β0 β¦ ((2β(π + 3)) β 3)) | ||
Theorem | ackendofnn0 47360 | The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024.) |
β’ (π β β0 β (Ackβπ):β0βΆβ0) | ||
Theorem | ackfnnn0 47361 | The Ackermann function at any nonnegative integer is a function on the nonnegative integers. (Contributed by AV, 4-May-2024.) (Proof shortened by AV, 8-May-2024.) |
β’ (π β β0 β (Ackβπ) Fn β0) | ||
Theorem | ackval0val 47362 | The Ackermann function at 0 (for the first argument). This is the first equation of PΓ©ter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.) |
β’ (π β β0 β ((Ackβ0)βπ) = (π + 1)) | ||
Theorem | ackvalsuc0val 47363 | The Ackermann function at a successor (of the first argument). This is the second equation of PΓ©ter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.) |
β’ (π β β0 β ((Ackβ(π + 1))β0) = ((Ackβπ)β1)) | ||
Theorem | ackvalsucsucval 47364 | The Ackermann function at the successors. This is the third equation of PΓ©ter's definition of the Ackermann function. (Contributed by AV, 8-May-2024.) |
β’ ((π β β0 β§ π β β0) β ((Ackβ(π + 1))β(π + 1)) = ((Ackβπ)β((Ackβ(π + 1))βπ))) | ||
Theorem | ackval0012 47365 | The Ackermann function at (0,0), (0,1), (0,2). (Contributed by AV, 2-May-2024.) |
β’ β¨((Ackβ0)β0), ((Ackβ0)β1), ((Ackβ0)β2)β© = β¨1, 2, 3β© | ||
Theorem | ackval1012 47366 | The Ackermann function at (1,0), (1,1), (1,2). (Contributed by AV, 4-May-2024.) |
β’ β¨((Ackβ1)β0), ((Ackβ1)β1), ((Ackβ1)β2)β© = β¨2, 3, 4β© | ||
Theorem | ackval2012 47367 | The Ackermann function at (2,0), (2,1), (2,2). (Contributed by AV, 4-May-2024.) |
β’ β¨((Ackβ2)β0), ((Ackβ2)β1), ((Ackβ2)β2)β© = β¨3, 5, 7β© | ||
Theorem | ackval3012 47368 | The Ackermann function at (3,0), (3,1), (3,2). (Contributed by AV, 7-May-2024.) |
β’ β¨((Ackβ3)β0), ((Ackβ3)β1), ((Ackβ3)β2)β© = β¨5, ;13, ;29β© | ||
Theorem | ackval40 47369 | The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β0) = ;13 | ||
Theorem | ackval41a 47370 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β1) = ((2β;16) β 3) | ||
Theorem | ackval41 47371 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β1) = ;;;;65533 | ||
Theorem | ackval42 47372 | The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β2) = ((2β;;;;65536) β 3) | ||
Theorem | ackval42a 47373 | The Ackermann function at (4,2), expressed with powers of 2. (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ4)β2) = ((2β(2β(2β(2β2)))) β 3) | ||
Theorem | ackval50 47374 | The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.) |
β’ ((Ackβ5)β0) = ;;;;65533 | ||
Theorem | fv1prop 47375 | The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023.) |
β’ (π΄ β π β ({β¨1, π΄β©, β¨2, π΅β©}β1) = π΄) | ||
Theorem | fv2prop 47376 | The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023.) |
β’ (π΅ β π β ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅) | ||
Theorem | submuladdmuld 47377 | Transformation of a sum of a product of a difference and a product with the subtrahend of the difference. (Contributed by AV, 2-Feb-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β (((π΄ β π΅) Β· πΆ) + (π΅ Β· π·)) = ((π΄ Β· πΆ) + (π΅ Β· (π· β πΆ)))) | ||
Theorem | affinecomb1 47378* | Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β πΊ β β) & β’ π = ((πΊ β πΉ) / (πΆ β π΅)) β β’ (π β (βπ‘ β β (π΄ = (((1 β π‘) Β· π΅) + (π‘ Β· πΆ)) β§ πΈ = (((1 β π‘) Β· πΉ) + (π‘ Β· πΊ))) β πΈ = ((π Β· (π΄ β π΅)) + πΉ))) | ||
Theorem | affinecomb2 47379* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β πΊ β β) β β’ (π β (βπ‘ β β (π΄ = (((1 β π‘) Β· π΅) + (π‘ Β· πΆ)) β§ πΈ = (((1 β π‘) Β· πΉ) + (π‘ Β· πΊ))) β ((πΆ β π΅) Β· πΈ) = (((πΊ β πΉ) Β· π΄) + ((πΉ Β· πΆ) β (π΅ Β· πΊ))))) | ||
Theorem | affineid 47380 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β (((1 β π) Β· π΄) + (π Β· π΄)) = π΄) | ||
Theorem | 1subrec1sub 47381 | Subtract the reciprocal of 1 minus a number from 1 results in the number divided by the number minus 1. (Contributed by AV, 15-Feb-2023.) |
β’ ((π΄ β β β§ π΄ β 1) β (1 β (1 / (1 β π΄))) = (π΄ / (π΄ β 1))) | ||
Theorem | resum2sqcl 47382 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) β β’ ((π΄ β β β§ π΅ β β) β π β β) | ||
Theorem | resum2sqgt0 47383 | The sum of the square of a nonzero real number and the square of another real number is greater than zero. (Contributed by AV, 7-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) β β’ (((π΄ β β β§ π΄ β 0) β§ π΅ β β) β 0 < π) | ||
Theorem | resum2sqrp 47384 | The sum of the square of a nonzero real number and the square of another real number is a positive real number. (Contributed by AV, 2-May-2023.) |
β’ π = ((π΄β2) + (π΅β2)) β β’ (((π΄ β β β§ π΄ β 0) β§ π΅ β β) β π β β+) | ||
Theorem | resum2sqorgt0 47385 | The sum of the square of two real numbers is greater than zero if at least one of the real numbers is nonzero. (Contributed by AV, 26-Feb-2023.) |
β’ π = ((π΄β2) + (π΅β2)) β β’ ((π΄ β β β§ π΅ β β β§ (π΄ β 0 β¨ π΅ β 0)) β 0 < π) | ||
Theorem | reorelicc 47386 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πΆ < π΄ β¨ πΆ β (π΄[,]π΅) β¨ π΅ < πΆ)) | ||
Theorem | rrx2pxel 47387 | The x-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) β β’ (π β π β (πβ1) β β) | ||
Theorem | rrx2pyel 47388 | The y-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) β β’ (π β π β (πβ2) β β) | ||
Theorem | prelrrx2 47389 | An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2. (Contributed by AV, 4-Feb-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) β β’ ((π΄ β β β§ π΅ β β) β {β¨1, π΄β©, β¨2, π΅β©} β π) | ||
Theorem | prelrrx2b 47390 | An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) β β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β ((π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) β π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}})) | ||
Theorem | rrx2pnecoorneor 47391 | If two different points π and π in a real Euclidean space of dimension 2 are different, then they are different at least at one coordinate. (Contributed by AV, 26-Feb-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) β β’ ((π β π β§ π β π β§ π β π) β ((πβ1) β (πβ1) β¨ (πβ2) β (πβ2))) | ||
Theorem | rrx2pnedifcoorneor 47392 | If two different points π and π in a real Euclidean space of dimension 2 are different, then at least one difference of two corresponding coordinates is not 0. (Contributed by AV, 26-Feb-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) & β’ π΄ = ((πβ1) β (πβ1)) & β’ π΅ = ((πβ2) β (πβ2)) β β’ ((π β π β§ π β π β§ π β π) β (π΄ β 0 β¨ π΅ β 0)) | ||
Theorem | rrx2pnedifcoorneorr 47393 | If two different points π and π in a real Euclidean space of dimension 2 are different, then at least one difference of two corresponding coordinates is not 0. (Contributed by AV, 26-Feb-2023.) |
β’ πΌ = {1, 2} & β’ π = (β βm πΌ) & β’ π΄ = ((πβ1) β (πβ1)) & β’ π΅ = ((πβ2) β (πβ2)) β β’ ((π β π β§ π β π β§ π β π) β (π΄ β 0 β¨ π΅ β 0)) | ||
Theorem | rrx2xpref1o 47394* | There is a bijection between the set of ordered pairs of real numbers (the cartesian product of the real numbers) and the set of points in the two dimensional Euclidean plane (represented as mappings from {1, 2} to the real numbers). (Contributed by AV, 12-Mar-2023.) |
β’ π = (β βm {1, 2}) & β’ πΉ = (π₯ β β, π¦ β β β¦ {β¨1, π₯β©, β¨2, π¦β©}) β β’ πΉ:(β Γ β)β1-1-ontoβπ | ||
Theorem | rrx2xpreen 47395 | The set of points in the two dimensional Euclidean plane and the set of ordered pairs of real numbers (the cartesian product of the real numbers) are equinumerous. (Contributed by AV, 12-Mar-2023.) |
β’ π = (β βm {1, 2}) β β’ π β (β Γ β) | ||
Theorem | rrx2plord 47396* | The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point iff its first coordinate is less than the first coordinate of the other point, or the first coordinates of both points are equal and the second coordinate of the first point is less than the second coordinate of the other point: β¨π, πβ© β€ β¨π₯, π¦β© iff (π < π₯ β¨ (π = π₯ β§ π β€ π¦)). (Contributed by AV, 12-Mar-2023.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π ) β§ ((π₯β1) < (π¦β1) β¨ ((π₯β1) = (π¦β1) β§ (π₯β2) < (π¦β2))))} β β’ ((π β π β§ π β π ) β (πππ β ((πβ1) < (πβ1) β¨ ((πβ1) = (πβ1) β§ (πβ2) < (πβ2))))) | ||
Theorem | rrx2plord1 47397* | The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point if its first coordinate is less than the first coordinate of the other point. (Contributed by AV, 12-Mar-2023.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π ) β§ ((π₯β1) < (π¦β1) β¨ ((π₯β1) = (π¦β1) β§ (π₯β2) < (π¦β2))))} β β’ ((π β π β§ π β π β§ (πβ1) < (πβ1)) β πππ) | ||
Theorem | rrx2plord2 47398* | The lexicographical ordering for points in the two dimensional Euclidean plane: if the first coordinates of two points are equal, a point is less than another point iff the second coordinate of the point is less than the second coordinate of the other point. (Contributed by AV, 12-Mar-2023.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π ) β§ ((π₯β1) < (π¦β1) β¨ ((π₯β1) = (π¦β1) β§ (π₯β2) < (π¦β2))))} & β’ π = (β βm {1, 2}) β β’ ((π β π β§ π β π β§ (πβ1) = (πβ1)) β (πππ β (πβ2) < (πβ2))) | ||
Theorem | rrx2plordisom 47399* | The set of points in the two dimensional Euclidean plane with the lexicographical ordering is isomorphic to the cartesian product of the real numbers with the lexicographical ordering implied by the ordering of the real numbers. (Contributed by AV, 12-Mar-2023.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π ) β§ ((π₯β1) < (π¦β1) β¨ ((π₯β1) = (π¦β1) β§ (π₯β2) < (π¦β2))))} & β’ π = (β βm {1, 2}) & β’ πΉ = (π₯ β β, π¦ β β β¦ {β¨1, π₯β©, β¨2, π¦β©}) & β’ π = {β¨π₯, π¦β© β£ ((π₯ β (β Γ β) β§ π¦ β (β Γ β)) β§ ((1st βπ₯) < (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯) < (2nd βπ¦))))} β β’ πΉ Isom π, π ((β Γ β), π ) | ||
Theorem | rrx2plordso 47400* | The lexicographical ordering for points in the two dimensional Euclidean plane is a strict total ordering. (Contributed by AV, 12-Mar-2023.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π ) β§ ((π₯β1) < (π¦β1) β¨ ((π₯β1) = (π¦β1) β§ (π₯β2) < (π¦β2))))} & β’ π = (β βm {1, 2}) β β’ π Or π |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |