P. 479 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47801-47900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nn0sumshdiglemB 47801*	Lemma for nn0sumshdig 47804 (induction step, odd multiplier). (Contributed by AV, 7-Jun-2020.)
⊢ (((𝑎 ∈ ℕ ∧ ((𝑎 − 1) / 2) ∈ ℕ0) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Theorem	nn0sumshdiglem1 47802*	Lemma 1 for nn0sumshdig 47804 (induction step). (Contributed by AV, 7-Jun-2020.)
⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Theorem	nn0sumshdiglem2 47803*	Lemma 2 for nn0sumshdig 47804. (Contributed by AV, 7-Jun-2020.)
⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
Theorem	nn0sumshdig 47804*	A nonnegative integer can be represented as sum of its shifted bits. (Contributed by AV, 7-Jun-2020.)
⊢ (𝐴 ∈ ℕ0 → 𝐴 = Σ𝑘 ∈ (0..^(#b‘𝐴))((𝑘(digit‘2)𝐴) · (2↑𝑘)))
21.45.21.12  Algorithms for the multiplication of nonnegative integers
Theorem	nn0mulfsum 47805*	Trivial algorithm to calculate the product of two nonnegative integers 𝑎 and 𝑏 by adding 𝑏 to itself 𝑎 times. (Contributed by AV, 17-May-2020.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (1...𝐴)𝐵)
Theorem	nn0mullong 47806*	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 16462. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (0..^(#b‘𝐴))(((𝑘(digit‘2)𝐴) · (2↑𝑘)) · 𝐵))
21.45.21.13  N-ary functions 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 8840) 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 47816 and mapsn 8900: (𝑋 ↑m {∅}) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 47826 and efmndbas 18822: (𝑋 ↑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 18822): "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 47837 and compare with df-clintop 47370: (𝑋 ↑m (𝑋 × 𝑋)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (𝑈↑↑𝑁) (see df-finxp 36916) 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 47810 shows that both definitions are equivalent.
Syntax	cnaryf 47807	Extend the definition of a class to include the n-ary functions.
class -aryF
Definition	df-naryf 47808*	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 47809	The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m (𝑋 ↑m 𝐼)))
Theorem	naryfvalixp 47810*	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 47811	An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m 𝐼)⟶𝑋))
Theorem	naryrcl 47812	Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V))
Theorem	naryfvalelfv 47813	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 47814*	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 47815*	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 47816. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐹 = {⟨∅, 𝑥⟩}))
Theorem	0aryfvalelfv 47816*	The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.)
⊢ (𝐹 ∈ (0-aryF 𝑋) → ∃𝑥 ∈ 𝑋 (𝐹‘∅) = 𝑥)
Theorem	1aryfvalel 47817	A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0})⟶𝑋))
Theorem	fv1arycl 47818	Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.)
⊢ ((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐺‘{⟨0, 𝐴⟩}) ∈ 𝑋)
Theorem	1arympt1 47819*	A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴:𝑋⟶𝑋) → 𝐹 ∈ (1-aryF 𝑋))
Theorem	1arympt1fv 47820*	The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{⟨0, 𝐵⟩}) = (𝐴‘𝐵))
Theorem	1arymaptfv 47821*	The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.)
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{⟨0, 𝑥⟩})))    ⇒   ⊢ (𝐹 ∈ (1-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐹‘{⟨0, 𝑥⟩})))
Theorem	1arymaptf 47822*	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 47823*	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 47824*	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 47825*	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 47826	The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.)
⊢ (1-aryF 𝑋) ≈ (𝑋 ↑m 𝑋)
Theorem	1aryenefmnd 47827	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 47828	A binary (endo)function on a set 𝑋. (Contributed by AV, 20-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (2-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0, 1})⟶𝑋))
Theorem	fv2arycl 47829	Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.)
⊢ ((𝐺 ∈ (2-aryF 𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐺‘{⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) ∈ 𝑋)
Theorem	2arympt 47830*	A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑂:(𝑋 × 𝑋)⟶𝑋) → 𝐹 ∈ (2-aryF 𝑋))
Theorem	2arymptfv 47831*	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 47832*	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 47833*	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 47834*	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 47835*	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 47836*	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 47837	The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.)
⊢ (2-aryF 𝑋) ≈ (𝑋 ↑m (𝑋 × 𝑋))
21.45.21.14  The Ackermann function 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 47877)], 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 47841, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 47840. As an illustration, we have ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) (see itcoval3 47846). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 47841: ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)). That Definition df-ack 47841 is equivalent to Péter's definition is proven by the following three theorems: ackval0val 47867: ((Ack‘0)‘𝑀) = (𝑀 + 1); ackvalsuc0val 47868: ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1); ackvalsucsucval 47869: ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 47870: 𝐴(0, 0) = 1, 𝐴(0, 1) = 2, 𝐴(0, 2) = 3; ackval1012 47871: 𝐴(1, 0) = 2, 𝐴(1, 1) = 3, 𝐴(1, 3) = 4; ackval2012 47872: 𝐴(2, 0) = 3, 𝐴(2, 1) = 5, 𝐴(2, 3) = 7; ackval3012 47873: 𝐴(3, 0) = 5, 𝐴(3, 1) = ;13, 𝐴(3, 3) = ;29.
Syntax	citco 47838	Extend the definition of a class to include iterated functions.
class IterComp
Syntax	cack 47839	Extend the definition of a class to include the Ackermann function operator.
class Ack
Definition	df-itco 47840*	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 47841*	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 47842*	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 47843	A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.)
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹))
Theorem	itcoval1 47844	A function iterated once. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹)
Theorem	itcoval2 47845	A function iterated twice. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹))
Theorem	itcoval3 47846	A function iterated three times. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹)))
Theorem	itcoval0mpt 47847*	A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛))
Theorem	itcovalsuc 47848*	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 47849	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 47850	The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴)
Theorem	itcovalpclem1 47851*	Lemma 1 for itcovalpc 47853: induction basis. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0))))
Theorem	itcovalpclem2 47852*	Lemma 2 for itcovalpc 47853: induction step. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))))
Theorem	itcovalpc 47853*	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 47854	Lemma 1 for itcovalt2lem2 47857. (Contributed by AV, 6-May-2024.)
⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0)
Theorem	itcovalt2lem2lem2 47855	Lemma 2 for itcovalt2lem2 47857. (Contributed by AV, 7-May-2024.)
⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶))
Theorem	itcovalt2lem1 47856*	Lemma 1 for itcovalt2 47858: induction basis. (Contributed by AV, 5-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶)))
Theorem	itcovalt2lem2 47857*	Lemma 2 for itcovalt2 47858: induction step. (Contributed by AV, 7-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))
Theorem	itcovalt2 47858*	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 47859*	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 47860	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 47861	The Ackermann function at 0. (Contributed by AV, 2-May-2024.)
⊢ (Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
Theorem	ackval1 47862	The Ackermann function at 1. (Contributed by AV, 4-May-2024.)
⊢ (Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2))
Theorem	ackval2 47863	The Ackermann function at 2. (Contributed by AV, 4-May-2024.)
⊢ (Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3))
Theorem	ackval3 47864	The Ackermann function at 3. (Contributed by AV, 7-May-2024.)
⊢ (Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3))
Theorem	ackendofnn0 47865	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 47866	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 47867	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 47868	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 47869	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 47870	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 47871	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 47872	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 47873	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 47874	The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘0) = ;13
Theorem	ackval41a 47875	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3)
Theorem	ackval41 47876	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ;;;;65533
Theorem	ackval42 47877	The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3)
Theorem	ackval42a 47878	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 47879	The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘5)‘0) = ;;;;65533
21.45.22  Elementary geometry (extension)
21.45.22.1  Auxiliary theorems
Theorem	fv1prop 47880	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 47881	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 47882	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 47883*	Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    &   ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹)))
Theorem	affinecomb2 47884*	Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))))
Theorem	affineid 47885	Identity of an affine combination. (Contributed by AV, 2-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴)
Theorem	1subrec1sub 47886	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 47887	The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.)
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
Theorem	resum2sqgt0 47888	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 47889	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 47890	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 47891	Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶))
21.45.22.2  Real euclidean space of dimension 2
Theorem	rrx2pxel 47892	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 47893	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 47894	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 47895	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 47896	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 47897	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 47898	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 47899*	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 47900	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})    ⇒   ⊢ 𝑅 ≈ (ℝ × ℝ)