P. 289 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28801-28900   *Has distinct variable group(s)

Type	Label	Description
Statement
15.6.5  Dyadic fractions
Syntax	c2s 28801	Declare the syntax for surreal two.
class 2s
Definition	df-2s 28802	Define surreal two. This is the simplest number greater than one. See 1p1e2s 28807 for its addition version. (Contributed by Scott Fenton, 27-May-2025.)
⊢ 2s = ({ 1s } |s ∅)
Syntax	cexps 28803	Declare the syntax for surreal exponentiation.
class ↑s
Definition	df-exps 28804*	Define surreal exponentiation. Compare df-exp 14208. (Contributed by Scott Fenton, 27-May-2025.)
⊢ ↑s = (𝑥 ∈ No, 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦))))))
Syntax	cz12s 28805	Define the syntax for the set of surreal dyadic fractions.
class ℤs[1/2]
Definition	df-z12s 28806*	Define the set of dyadic rationals. This is the set of rationals whose denominator is a power of two. Later we will prove that this is precisely the set of surreals with a finite birthday. (Contributed by Scott Fenton, 27-May-2025.)
⊢ ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}
Theorem	1p1e2s 28807	One plus one is two. Surreal version. (Contributed by Scott Fenton, 27-May-2025.)
⊢ ( 1s +s 1s ) = 2s
Theorem	no2times 28808	Version of 2times 12481 for surreal numbers. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ (𝐴 ∈ No → (2s ·s 𝐴) = (𝐴 +s 𝐴))
Theorem	2nns 28809	Surreal two is a surreal natural. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ 2s ∈ ℕs
Theorem	2no 28810	Surreal two is a surreal number. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ 2s ∈ No
Theorem	2ne0s 28811	Surreal two is nonzero. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ 2s ≠ 0s
Theorem	n0seo 28812*	A non-negative surreal integer is either even or odd. (Contributed by Scott Fenton, 19-Aug-2025.)
⊢ (𝑁 ∈ ℕ0s → (∃𝑥 ∈ ℕ0s 𝑁 = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑁 = ((2s ·s 𝑥) +s 1s )))
Theorem	zseo 28813*	A surreal integer is either even or odd. (Contributed by Scott Fenton, 19-Aug-2025.)
⊢ (𝑁 ∈ ℤs → (∃𝑥 ∈ ℤs 𝑁 = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs 𝑁 = ((2s ·s 𝑥) +s 1s )))
Theorem	twocut 28814	Two times the cut of zero and one is one. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ (2s ·s ({ 0s } |s { 1s })) = 1s
Theorem	nohalf 28815	An explicit expression for one half. This theorem avoids the axiom of infinity. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ ( 1s /su 2s) = ({ 0s } |s { 1s })
Theorem	expsval 28816	The value of surreal exponentiation. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ ℤs) → (𝐴↑s𝐵) = if(𝐵 = 0s , 1s , if( 0s <s 𝐵, (seqs 1s ( ·s , (ℕs × {𝐴}))‘𝐵), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝐴}))‘( -s‘𝐵))))))
Theorem	expnnsval 28817	Value of surreal exponentiation at a natural number. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕs) → (𝐴↑s𝑁) = (seqs 1s ( ·s , (ℕs × {𝐴}))‘𝑁))
Theorem	exps0 28818	Surreal exponentiation to zero. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ (𝐴 ∈ No → (𝐴↑s 0s ) = 1s )
Theorem	exps1 28819	Surreal exponentiation to one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ (𝐴 ∈ No → (𝐴↑s 1s ) = 𝐴)
Theorem	expsp1 28820	Value of a surreal number raised to a non-negative integer power plus one. (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s(𝑁 +s 1s )) = ((𝐴↑s𝑁) ·s 𝐴))
Theorem	expscllem 28821*	Lemma for proving non-negative surreal integer exponentiation closure. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ 𝐹 ⊆ No    &   ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ·s 𝑦) ∈ 𝐹)    &   ⊢ 1s ∈ 𝐹    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ 𝐹)
Theorem	expscl 28822	Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ No)
Theorem	n0expscl 28823	Closure law for non-negative surreal integer exponentiation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℕ0s)
Theorem	nnexpscl 28824	Closure law for positive surreal integer exponentiation. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℕs)
Theorem	zexpscl 28825	Closure law for surreal integer exponentiation. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ ((𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℤs)
Theorem	expadds 28826	Sum of exponents law for surreals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s(𝑀 +s 𝑁)) = ((𝐴↑s𝑀) ·s (𝐴↑s𝑁)))
Theorem	expsne0 28827	A non-negative surreal integer power is nonzero if its base is nonzero. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ≠ 0s )
Theorem	expsgt0 28828	A non-negative surreal integer power is positive if its base is positive. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ∧ 0s <s 𝐴) → 0s <s (𝐴↑s𝑁))
Theorem	pw2recs 28829*	Any power of two has a multiplicative inverse. Note that this theorem does not require the axiom of infinity. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ (𝑁 ∈ ℕ0s → ∃𝑥 ∈ No ((2s↑s𝑁) ·s 𝑥) = 1s )
Theorem	pw2divscld 28830	Division closure for powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 /su (2s↑s𝑁)) ∈ No)
Theorem	pw2divmulsd 28831	Relationship between surreal division and multiplication for powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((𝐴 /su (2s↑s𝑁)) = 𝐵 ↔ ((2s↑s𝑁) ·s 𝐵) = 𝐴))
Theorem	pw2divscan3d 28832	Cancellation law for surreal division by powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (((2s↑s𝑁) ·s 𝐴) /su (2s↑s𝑁)) = 𝐴)
Theorem	pw2divscan2d 28833	A cancellation law for surreal division by powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((2s↑s𝑁) ·s (𝐴 /su (2s↑s𝑁))) = 𝐴)
Theorem	pw2divsassd 28834	An associative law for division by powers of two. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su (2s↑s𝑁)) = (𝐴 ·s (𝐵 /su (2s↑s𝑁))))
Theorem	pw2divscan4d 28835	Cancellation law for divison by powers of two. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 /su (2s↑s𝑁)) = (((2s↑s𝑀) ·s 𝐴) /su (2s↑s(𝑁 +s 𝑀))))
Theorem	pw2gt0divsd 28836	Division of a positive surreal by a power of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 0s <s (𝐴 /su (2s↑s𝑁))))
Theorem	pw2ge0divsd 28837	Divison of a non-negative surreal by a power of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ( 0s ≤s 𝐴 ↔ 0s ≤s (𝐴 /su (2s↑s𝑁))))
Theorem	pw2divsrecd 28838	Relationship between surreal division and reciprocal for powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 /su (2s↑s𝑁)) = (𝐴 ·s ( 1s /su (2s↑s𝑁))))
Theorem	pw2divsdird 28839	Distribution of surreal division over addition for powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) /su (2s↑s𝑁)) = ((𝐴 /su (2s↑s𝑁)) +s (𝐵 /su (2s↑s𝑁))))
Theorem	pw2divsnegd 28840	Move negative sign inside of a power of two division. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ( -s‘(𝐴 /su (2s↑s𝑁))) = (( -s‘𝐴) /su (2s↑s𝑁)))
Theorem	pw2ltdivmulsd 28841	Surreal less-than relationship between division and multiplication for powers of two. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((𝐴 /su (2s↑s𝑁)) <s 𝐵 ↔ 𝐴 <s ((2s↑s𝑁) ·s 𝐵)))
Theorem	pw2ltmuldivs2d 28842	Surreal less-than relationship between division and multiplication for powers of two. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (((2s↑s𝑁) ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su (2s↑s𝑁))))
Theorem	pw2ltsdiv1d 28843	Surreal less-than relationship for division by a power of two. (Contributed by Scott Fenton, 18-Jan-2026.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 /su (2s↑s𝑁)) <s (𝐵 /su (2s↑s𝑁))))
Theorem	avglts1d 28844	Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 𝐴 <s ((𝐴 +s 𝐵) /su 2s)))
Theorem	avglts2d 28845	Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ((𝐴 +s 𝐵) /su 2s) <s 𝐵))
Theorem	pw2divs0d 28846	Division into zero is zero for a power of two. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ( 0s /su (2s↑s𝑁)) = 0s )
Theorem	pw2divsidd 28847	Identity law for division over powers of two. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((2s↑s𝑁) /su (2s↑s𝑁)) = 1s )
Theorem	pw2ltdivmuls2d 28848	Surreal less-than relationship between division and multiplication for powers of two. (Contributed by Scott Fenton, 23-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((𝐴 /su (2s↑s𝑁)) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s (2s↑s𝑁))))
Theorem	halfcut 28849	Relate the cut of twice of two numbers to the cut of the numbers. Lemma 4.2 of [Gonshor] p. 28. (Contributed by Scott Fenton, 7-Aug-2025.) Avoid the axiom of infinity. (Proof modified by Scott Fenton, 6-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → ({(2s ·s 𝐴)} |s {(2s ·s 𝐵)}) = (𝐴 +s 𝐵))    &   ⊢ 𝐶 = ({𝐴} |s {𝐵})    ⇒   ⊢ (𝜑 → 𝐶 = ((𝐴 +s 𝐵) /su 2s))
Theorem	addhalfcut 28850	The cut of a surreal non-negative integer and its successor is the original number plus one half. Part of theorem 4.2 of [Gonshor] p. 30. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ({𝐴} |s {(𝐴 +s 1s )}) = (𝐴 +s ( 1s /su 2s)))
Theorem	pw2cut 28851	Extend halfcut 28849 to arbitrary powers of two. Part of theorem 4.2 of [Gonshor] p. 28. (Contributed by Scott Fenton, 18-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → ({(2s ·s 𝐴)} |s {(2s ·s 𝐵)}) = (𝐴 +s 𝐵))    ⇒   ⊢ (𝜑 → ({(𝐴 /su (2s↑s𝑁))} |s {(𝐵 /su (2s↑s𝑁))}) = ((𝐴 +s 𝐵) /su (2s↑s(𝑁 +s 1s ))))
Theorem	pw2cutp1 28852	Simplify pw2cut 28851 in the case of successors of surreal integers. (Contributed by Scott Fenton, 11-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ({(𝐴 /su (2s↑s𝑁))} |s {((𝐴 +s 1s ) /su (2s↑s𝑁))}) = (((2s ·s 𝐴) +s 1s ) /su (2s↑s(𝑁 +s 1s ))))
Theorem	pw2cut2 28853	Cut expression for powers of two. Theorem 12 of [Conway] p. 12-13. (Contributed by Scott Fenton, 18-Jan-2026.)
⊢ ((𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s) → (𝐴 /su (2s↑s𝑁)) = ({((𝐴 −s 1s ) /su (2s↑s𝑁))} |s {((𝐴 +s 1s ) /su (2s↑s𝑁))}))
Theorem	bdaypw2n0bndlem 28854	Lemma for bdaypw2n0bnd 28855. Prove the case with a successor. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s (2s↑s(𝑁 +s 1s ))) → (bday‘(𝐴 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc (bday‘(𝑁 +s 1s )))
Theorem	bdaypw2n0bnd 28855	Upper bound for the birthday of a proper fraction of a power of two. This is actually a strict equality when 𝐴 is odd, but we do not need this for the rest of our development. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s (2s↑s𝑁)) → (bday‘(𝐴 /su (2s↑s𝑁))) ⊆ suc (bday‘𝑁))
Theorem	bdaypw2bnd 28856	Birthday bounding rule for non-negative dyadic rationals. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑌 <s (2s↑s𝑃))    &   ⊢ (𝜑 → (𝑋 +s 𝑃) <s 𝑁)    ⇒   ⊢ (𝜑 → (bday‘(𝑋 +s (𝑌 /su (2s↑s𝑃)))) ⊆ (bday‘𝑁))
Theorem	bdayfinbndcbv 28857*	Lemma for bdayfinbnd 28860. Change some bound variables. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → ∀𝑧 ∈ No (((bday‘𝑧) ⊆ (bday‘𝑁) ∧ 0s ≤s 𝑧) → (𝑧 = 𝑁 ∨ ∃𝑥 ∈ ℕ0s ∃𝑦 ∈ ℕ0s ∃𝑝 ∈ ℕ0s (𝑧 = (𝑥 +s (𝑦 /su (2s↑s𝑝))) ∧ 𝑦 <s (2s↑s𝑝) ∧ (𝑥 +s 𝑝) <s 𝑁))))    ⇒   ⊢ (𝜑 → ∀𝑤 ∈ No (((bday‘𝑤) ⊆ (bday‘𝑁) ∧ 0s ≤s 𝑤) → (𝑤 = 𝑁 ∨ ∃𝑎 ∈ ℕ0s ∃𝑏 ∈ ℕ0s ∃𝑞 ∈ ℕ0s (𝑤 = (𝑎 +s (𝑏 /su (2s↑s𝑞))) ∧ 𝑏 <s (2s↑s𝑞) ∧ (𝑎 +s 𝑞) <s 𝑁))))
Theorem	bdayfinbndlem1 28858*	Lemma for bdayfinbnd 28860. Show the first half of the inductive step. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → ∀𝑧 ∈ No (((bday‘𝑧) ⊆ (bday‘𝑁) ∧ 0s ≤s 𝑧) → (𝑧 = 𝑁 ∨ ∃𝑥 ∈ ℕ0s ∃𝑦 ∈ ℕ0s ∃𝑝 ∈ ℕ0s (𝑧 = (𝑥 +s (𝑦 /su (2s↑s𝑝))) ∧ 𝑦 <s (2s↑s𝑝) ∧ (𝑥 +s 𝑝) <s 𝑁))))    ⇒   ⊢ (𝜑 → ∀𝑤 ∈ No (((bday‘𝑤) ⊆ (bday‘(𝑁 +s 1s )) ∧ 0s ≤s 𝑤) → (𝑤 = (𝑁 +s 1s ) ∨ ∃𝑎 ∈ ℕ0s ∃𝑏 ∈ ℕ0s ∃𝑞 ∈ ℕ0s (𝑤 = (𝑎 +s (𝑏 /su (2s↑s𝑞))) ∧ 𝑏 <s (2s↑s𝑞) ∧ (𝑎 +s 𝑞) <s (𝑁 +s 1s )))))
Theorem	bdayfinbndlem2 28859*	Lemma for bdayfinbnd 28860. Conduct the induction. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ (𝑁 ∈ ℕ0s → ∀𝑧 ∈ No (((bday‘𝑧) ⊆ (bday‘𝑁) ∧ 0s ≤s 𝑧) → (𝑧 = 𝑁 ∨ ∃𝑥 ∈ ℕ0s ∃𝑦 ∈ ℕ0s ∃𝑝 ∈ ℕ0s (𝑧 = (𝑥 +s (𝑦 /su (2s↑s𝑝))) ∧ 𝑦 <s (2s↑s𝑝) ∧ (𝑥 +s 𝑝) <s 𝑁))))
Theorem	bdayfinbnd 28860*	Given a non-negative integer and a non-negative surreal of lesser or equal birthday, show that the surreal can be expressed as a dyadic fraction with an upper bound on the integer and exponent. This proof follows the proof from Mizar at https://mizar.uwb.edu.pl/version/current/html/surrealn.html. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑍 ∈ No)    &   ⊢ (𝜑 → (bday‘𝑍) ⊆ (bday‘𝑁))    &   ⊢ (𝜑 → 0s ≤s 𝑍)    ⇒   ⊢ (𝜑 → (𝑍 = 𝑁 ∨ ∃𝑥 ∈ ℕ0s ∃𝑦 ∈ ℕ0s ∃𝑝 ∈ ℕ0s (𝑍 = (𝑥 +s (𝑦 /su (2s↑s𝑝))) ∧ 𝑦 <s (2s↑s𝑝) ∧ (𝑥 +s 𝑝) <s 𝑁)))
Theorem	z12bdaylem1 28861	Lemma for z12bday 28876. Prove an inequality for birthday ordering. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0s)    &   ⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) <s (2s↑s𝑃))    ⇒   ⊢ (𝜑 → (𝑁 +s (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃))) ≠ (𝑁 +s 𝑃))
Theorem	z12bdaylem2 28862	Lemma for z12bday 28876. Show the first half of the equality. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0s)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0s)    &   ⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) <s (2s↑s𝑃))    ⇒   ⊢ (𝜑 → (bday‘(𝑁 +s (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ (bday‘((𝑁 +s 𝑃) +s 1s )))
Theorem	elz12s 28863*	Membership in the dyadic fractions. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝐴 ∈ ℤs[1/2] ↔ ∃𝑥 ∈ ℤs ∃𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su (2s↑s𝑦)))
Theorem	elz12si 28864	Inference form of membership in the dyadic fractions. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ ((𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s) → (𝐴 /su (2s↑s𝑁)) ∈ ℤs[1/2])
Theorem	z12sex 28865	The class of dyadic fractions is a set. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ℤs[1/2] ∈ V
Theorem	zz12s 28866	A surreal integer is a dyadic fraction. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ ℤs[1/2])
Theorem	z12no 28867	A dyadic is a surreal. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No)
Theorem	z12addscl 28868	The dyadics are closed under addition. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ ((𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2]) → (𝐴 +s 𝐵) ∈ ℤs[1/2])
Theorem	z12negscl 28869	The dyadics are closed under negation. (Contributed by Scott Fenton, 9-Nov-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → ( -s‘𝐴) ∈ ℤs[1/2])
Theorem	z12subscl 28870	The dyadics are closed under subtraction. (Contributed by Scott Fenton, 12-Dec-2025.)
⊢ ((𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2]) → (𝐴 −s 𝐵) ∈ ℤs[1/2])
Theorem	z12shalf 28871	Half of a dyadic is a dyadic. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → (𝐴 /su 2s) ∈ ℤs[1/2])
Theorem	z12negsclb 28872	A surreal is a dyadic fraction iff its negative is. (Contributed by Scott Fenton, 9-Nov-2025.)
⊢ (𝐴 ∈ No → (𝐴 ∈ ℤs[1/2] ↔ ( -s‘𝐴) ∈ ℤs[1/2]))
Theorem	z12zsodd 28873*	A dyadic fraction is either an integer or an odd number divided by a positive power of two. (Contributed by Scott Fenton, 5-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → (𝐴 ∈ ℤs ∨ ∃𝑥 ∈ ℤs ∃𝑦 ∈ ℕs 𝐴 = (((2s ·s 𝑥) +s 1s ) /su (2s↑s𝑦))))
Theorem	z12sge0 28874*	An expression for non-negative dyadic rationals. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (𝐴 ∈ ℤs[1/2] ↔ ∃𝑥 ∈ ℕ0s ∃𝑦 ∈ ℕ0s ∃𝑝 ∈ ℕ0s (𝐴 = (𝑥 +s (𝑦 /su (2s↑s𝑝))) ∧ 𝑦 <s (2s↑s𝑝))))
Theorem	z12bdaylem 28875	Lemma for z12bday 28876. Handle the non-negative case. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴) → (bday‘𝐴) ∈ ω)
Theorem	z12bday 28876	A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025.) (Proof shortened by Scott Fenton, 22-Feb-2026.)
⊢ (𝐴 ∈ ℤs[1/2] → (bday‘𝐴) ∈ ω)
Theorem	bdayfinlem 28877	Lemma for bdayfin 28878. Handle the non-negative case. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ (bday‘𝐴) ∈ ω) → 𝐴 ∈ ℤs[1/2])
Theorem	bdayfin 28878	A surreal has a finite birthday iff it is a dyadic fraction. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ (𝐴 ∈ No → (𝐴 ∈ ℤs[1/2] ↔ (bday‘𝐴) ∈ ω))
Theorem	dfz12s2 28879	The set of dyadic fractions is the same as the old set of ω. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ ℤs[1/2] = (O‘ω)
15.6.6  Real numbers
Syntax	creno 28880	Declare the syntax for the surreal reals.
class ℝs
Definition	df-reno 28881*	Define the surreal reals. These are the finite numbers without any infintesimal parts. Definition from [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ℝs = {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -s‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 −s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}
Theorem	elreno 28882*	Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -s‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 −s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s /su 𝑛))}))))
Theorem	reno 28883	A surreal real is a surreal number. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (𝐴 ∈ ℝs → 𝐴 ∈ No)
Theorem	renod 28884	A surreal real is a surreal number. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	recut 28885*	The cut involved in defining surreal reals is a genuine cut. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 −s ( 1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s /su 𝑛))})
Theorem	elreno2 28886*	Alternate characterization of the surreal reals. Theorem 4.4(b) of [Gonshor] p. 39. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -s‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 −s 𝑥𝑂)))))
Theorem	0reno 28887	Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 0s ∈ ℝs
Theorem	1reno 28888	Surreal one is a surreal real. (Contributed by Scott Fenton, 18-Feb-2026.)
⊢ 1s ∈ ℝs
Theorem	renegscl 28889	The surreal reals are closed under negation. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℝs → ( -s‘𝐴) ∈ ℝs)
Theorem	readdscl 28890	The surreal reals are closed under addition. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs) → (𝐴 +s 𝐵) ∈ ℝs)
Theorem	remulscllem1 28891*	Lemma for remulscl 28893. Split a product of reciprocals of naturals. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs 𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s ( 1s /su 𝑞))) ↔ ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛)))
Theorem	remulscllem2 28892*	Lemma for remulscl 28893. Bound 𝐴 and 𝐵 above and below. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ ((𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs) ∧ ((( -s‘𝑁) <s 𝐴 ∧ 𝐴 <s 𝑁) ∧ (( -s‘𝑀) <s 𝐵 ∧ 𝐵 <s 𝑀)))) → ∃𝑝 ∈ ℕs (( -s‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝))
Theorem	remulscl 28893	The surreal reals are closed under multiplication. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs) → (𝐴 ·s 𝐵) ∈ ℝs)
PART 16  ELEMENTARY GEOMETRY This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally: A Tarski structure 𝑓 is a set (of points) (Base‘𝑓) together with functions (Itv‘𝑓) and (dist‘𝑓) on ((Base‘𝑓) × (Base‘𝑓)) satisfying certain axioms (given in Definitions df-trkg 28920 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17330). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure 𝑓. One defines a betweenness ternary predicate Btw by positing that, for any 𝑥, 𝑦, 𝑧 ∈ (Base‘𝑓), one has "Btw 𝑥𝑦𝑧 " if and only if 𝑦 ∈ 𝑥(Itv‘𝑓)𝑧, and a congruence quaternary predicate Congr by positing that, for any 𝑥, 𝑦, 𝑧, 𝑡 ∈ (Base‘𝑓), one has "Congr 𝑥𝑦𝑧𝑡 " if and only if 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡. It is easy to check that if 𝑓 satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when (Base‘𝑓) is interpreted as the universe of discourse. Conversely, suppose that one is given a set 𝑎, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure 𝑓 such that (Base‘𝑓) is 𝑎, and (Itv‘𝑓) is the function which associates with each ⟨𝑥, 𝑦⟩ ∈ (𝑎 × 𝑎) the set of points 𝑧 ∈ 𝑎 such that "Btw 𝑥𝑧𝑦", and (dist‘𝑓) is the function which associates with each ⟨𝑥, 𝑦⟩ ∈ (𝑎 × 𝑎) the set of ordered pairs ⟨𝑧, 𝑡⟩ ∈ (𝑎 × 𝑎) such that "Congr 𝑥𝑦𝑧𝑡". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when 𝑎 is interpreted as the universe of discourse, then 𝑓 satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 instead of "Congr 𝑥𝑦𝑧𝑡", as it is more convenient. It is always possible to define dist for any particular geometry to produce equal results when congruence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 causes no loss of generality in tgjustc1 28942 and tgjustc2 28943, which in turn are supported by tgjustf 28940 and tgjustr 28941. A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at https://www.michaelbeeson.com/research/FormalTarski/ 28941. Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents 𝜑 →) by insert a ⊤ → in each hypothesis, using a1i 11, then using mptru 1576 to remove the final ⊤ → prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr 490, the theorem as stated, and ex 418. For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg 28920), of "Euclidean dimensionless Tarski structures" (df-trkge 28918) and of "Tarski structures of dimension no less than N" (df-trkgld 28919). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 29320 and iscgra 29321). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg 28979. The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures. Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement.
16.1  Definition and Tarski's Axioms of Geometry
Syntax	cstrkg 28894	Extends class notation with the class of Tarski geometries.
class TarskiG
Syntax	cstrkgc 28895	Extends class notation with the class of geometries fulfilling the congruence axioms.
class TarskiGC
Syntax	cstrkgb 28896	Extends class notation with the class of geometries fulfilling the betweenness axioms.
class TarskiGB
Syntax	cstrkgcb 28897	Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms.
class TarskiGCB
Syntax	cstrkgld 28898	Extends class notation with the relation for geometries fulfilling the lower dimension axioms.
class DimTarskiG≥
Syntax	cstrkge 28899	Extends class notation with the class of geometries fulfilling Euclid's axiom.
class TarskiGE
Syntax	citv 28900	Declare the syntax for the Interval (segment) index extractor.
class Itv