P. 284 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28301-28400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	n0zsd 28301	A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤs)
Theorem	1zs 28302	One is a surreal integer. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ 1s ∈ ℤs
Theorem	znegscl 28303	The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℤs → ( -us ‘𝐴) ∈ ℤs)
Theorem	znegscld 28304	The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) ∈ ℤs)
Theorem	zaddscl 28305	The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs) → (𝐴 +s 𝐵) ∈ ℤs)
Theorem	zaddscld 28306	The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝐵 ∈ ℤs)    ⇒   ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ ℤs)
Theorem	zsubscld 28307	The surreal integers are closed under subtraction. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝐵 ∈ ℤs)    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ ℤs)
Theorem	zmulscld 28308	The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝐵 ∈ ℤs)    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ ℤs)
Theorem	elzn0s 28309	A surreal integer is a surreal that is a non-negative integer or whose negative is a non-negative integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℤs ↔ (𝐴 ∈ No ∧ (𝐴 ∈ ℕ0s ∨ ( -us ‘𝐴) ∈ ℕ0s)))
Theorem	elzs2 28310	A surreal integer is either a positive integer, zero, or the negative of a positive integer. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑁 ∈ ℤs ↔ (𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘𝑁) ∈ ℕs)))
Theorem	eln0zs 28311	Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑁 ∈ ℕ0s ↔ (𝑁 ∈ ℤs ∧ 0s ≤s 𝑁))
Theorem	elnnzs 28312	Positive surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑁 ∈ ℕs ↔ (𝑁 ∈ ℤs ∧ 0s <s 𝑁))
Theorem	elznns 28313	Surreal integer property expressed in terms of positive integers and non-negative integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑁 ∈ ℤs ↔ (𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ ( -us ‘𝑁) ∈ ℕ0s)))
Theorem	zn0subs 28314	The non-negative difference of surreal integers is a non-negative integer. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs) → (𝑀 ≤s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕ0s))
Theorem	peano5uzs 28315*	Peano's inductive postulate for upper surreal integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝑁 ∈ ℤs)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 +s 1s ) ∈ 𝐴)    ⇒   ⊢ (𝜑 → {𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘} ⊆ 𝐴)
Theorem	uzsind 28316*	Induction on the upper surreal integers that start at 𝑀. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑗 = (𝑘 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑀 ∈ ℤs → 𝜓)    &   ⊢ ((𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁) → 𝜏)
Theorem	zsbday 28317	A surreal integer has a finite birthday. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℤs → ( bday ‘𝐴) ∈ ω)
Theorem	zscut 28318	A cut expression for surreal integers. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s )}))
Theorem	zsoring 28319	The surreal integers form an ordered ring. Note that we have to restrict the operations here since No is a proper class. (Contributed by Scott Fenton, 23-Dec-2025.)
⊢ ℤs = (Base‘𝐾)    &   ⊢ ( +s ↾ (ℤs × ℤs)) = (+g‘𝐾)    &   ⊢ ( ·s ↾ (ℤs × ℤs)) = (.r‘𝐾)    &   ⊢ ( ≤s ∩ (ℤs × ℤs)) = (le‘𝐾)    &   ⊢ 0s = (0g‘𝐾)    ⇒   ⊢ 𝐾 ∈ oRing
15.6.5  Dyadic fractions
Syntax	c2s 28320	Declare the syntax for surreal two.
class 2s
Definition	df-2s 28321	Define surreal two. This is the simplest number greater than one. See 1p1e2s 28326 for its addition version. (Contributed by Scott Fenton, 27-May-2025.)
⊢ 2s = ({ 1s } |s ∅)
Syntax	cexps 28322	Declare the syntax for surreal exponentiation.
class ↑s
Definition	df-exps 28323*	Define surreal exponentiation. Compare df-exp 13987. (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 × {𝑥}))‘( -us ‘𝑦))))))
Syntax	czs12 28324	Define the syntax for the set of surreal dyadic fractions.
class ℤs[1/2]
Definition	df-zs12 28325*	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 28326	One plus one is two. Surreal version. (Contributed by Scott Fenton, 27-May-2025.)
⊢ ( 1s +s 1s ) = 2s
Theorem	no2times 28327	Version of 2times 12277 for surreal numbers. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ (𝐴 ∈ No → (2s ·s 𝐴) = (𝐴 +s 𝐴))
Theorem	2nns 28328	Surreal two is a surreal natural. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ 2s ∈ ℕs
Theorem	2sno 28329	Surreal two is a surreal number. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ 2s ∈ No
Theorem	2ne0s 28330	Surreal two is non-zero. (Contributed by Scott Fenton, 23-Jul-2025.)
⊢ 2s ≠ 0s
Theorem	n0seo 28331*	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 28332*	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 28333	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 28334	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 28335	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 × {𝐴}))‘( -us ‘𝐵))))))
Theorem	expsnnval 28336	Value of surreal exponentiation at a natural number. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕs) → (𝐴↑s𝑁) = (seqs 1s ( ·s , (ℕs × {𝐴}))‘𝑁))
Theorem	exps0 28337	Surreal exponentiation to zero. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ (𝐴 ∈ No → (𝐴↑s 0s ) = 1s )
Theorem	exps1 28338	Surreal exponentiation to one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ (𝐴 ∈ No → (𝐴↑s 1s ) = 𝐴)
Theorem	expsp1 28339	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 28340*	Lemma for proving non-negative surreal integer exponentiation closure. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ 𝐹 ⊆ No     &   ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ·s 𝑦) ∈ 𝐹)    &   ⊢ 1s ∈ 𝐹    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ 𝐹)
Theorem	expscl 28341	Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ No )
Theorem	n0expscl 28342	Closure law for non-negative surreal integer exponentiation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℕ0s)
Theorem	nnexpscl 28343	Closure law for positive surreal integer exponentiation. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℕs)
Theorem	zexpscl 28344	Closure law for surreal integer exponentiation. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ ((𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℤs)
Theorem	expadds 28345	Sum of exponents law for surreals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s(𝑀 +s 𝑁)) = ((𝐴↑s𝑀) ·s (𝐴↑s𝑁)))
Theorem	expsne0 28346	A non-negative surreal integer power is non-zero if its base is non-zero. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ≠ 0s )
Theorem	expsgt0 28347	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 28348*	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 28349	Division closure for powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 /su (2s↑s𝑁)) ∈ No )
Theorem	pw2divsmuld 28350	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 28351	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 28352	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 28353	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 28354	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 28355	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 28356	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 28357	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 28358	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 28359	Move negative sign inside of a power of two division. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ( -us ‘(𝐴 /su (2s↑s𝑁))) = (( -us ‘𝐴) /su (2s↑s𝑁)))
Theorem	pw2sltdivmuld 28360	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	pw2sltmuldiv2d 28361	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	avgslt1d 28362	Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 𝐴 <s ((𝐴 +s 𝐵) /su 2s)))
Theorem	avgslt2d 28363	Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ((𝐴 +s 𝐵) /su 2s) <s 𝐵))
Theorem	halfcut 28364	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 28365	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 28366	Extend halfcut 28364 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 28367	Simplify pw2cut 28366 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	elzs12 28368*	Membership in the dyadic fractions. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝐴 ∈ ℤs[1/2] ↔ ∃𝑥 ∈ ℤs ∃𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su (2s↑s𝑦)))
Theorem	zs12ex 28369	The class of dyadic fractions is a set. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ℤs[1/2] ∈ V
Theorem	zzs12 28370	A surreal integer is a dyadic fraction. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ ℤs[1/2])
Theorem	zs12no 28371	A dyadic is a surreal. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No )
Theorem	zs12addscl 28372	The dyadics are closed under addition. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ ((𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2]) → (𝐴 +s 𝐵) ∈ ℤs[1/2])
Theorem	zs12negscl 28373	The dyadics are closed under negation. (Contributed by Scott Fenton, 9-Nov-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → ( -us ‘𝐴) ∈ ℤs[1/2])
Theorem	zs12subscl 28374	The dyadics are closed under subtraction. (Contributed by Scott Fenton, 12-Dec-2025.)
⊢ ((𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2]) → (𝐴 -s 𝐵) ∈ ℤs[1/2])
Theorem	zs12half 28375	Half of a dyadic is a dyadic. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → (𝐴 /su 2s) ∈ ℤs[1/2])
Theorem	zs12negsclb 28376	A surreal is a dyadic fraction iff its negative is. (Contributed by Scott Fenton, 9-Nov-2025.)
⊢ (𝐴 ∈ No → (𝐴 ∈ ℤs[1/2] ↔ ( -us ‘𝐴) ∈ ℤs[1/2]))
Theorem	zs12zodd 28377*	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	zs12ge0 28378*	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	zs12bday 28379	A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → ( bday ‘𝐴) ∈ ω)
15.6.6  Real numbers
Syntax	creno 28380	Declare the syntax for the surreal reals.
class ℝs
Definition	df-reno 28381*	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 (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}
Theorem	elreno 28382*	Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s /su 𝑛))}))))
Theorem	recut 28383*	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	0reno 28384	Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 0s ∈ ℝs
Theorem	renegscl 28385	The surreal reals are closed under negation. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℝs → ( -us ‘𝐴) ∈ ℝs)
Theorem	readdscl 28386	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 28387*	Lemma for remulscl 28389. 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 28388*	Lemma for remulscl 28389. Bound 𝐴 and 𝐵 above and below. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ((𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs) ∧ ((( -us ‘𝑁) <s 𝐴 ∧ 𝐴 <s 𝑁) ∧ (( -us ‘𝑀) <s 𝐵 ∧ 𝐵 <s 𝑀)))) → ∃𝑝 ∈ ℕs (( -us ‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝))
Theorem	remulscl 28389	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 28416 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17076). 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 28438 and tgjustc2 28439, which in turn are supported by tgjustf 28436 and tgjustr 28437. 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/ 28437. 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 1547 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 484, the theorem as stated, and ex 412. 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 28416), of "Euclidean dimensionless Tarski structures" (df-trkge 28414) and of "Tarski structures of dimension no less than N" (df-trkgld 28415). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 28771 and iscgra 28772). 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 28474. 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 28390	Extends class notation with the class of Tarski geometries.
class TarskiG
Syntax	cstrkgc 28391	Extends class notation with the class of geometries fulfilling the congruence axioms.
class TarskiGC
Syntax	cstrkgb 28392	Extends class notation with the class of geometries fulfilling the betweenness axioms.
class TarskiGB
Syntax	cstrkgcb 28393	Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms.
class TarskiGCB
Syntax	cstrkgld 28394	Extends class notation with the relation for geometries fulfilling the lower dimension axioms.
class DimTarskiG≥
Syntax	cstrkge 28395	Extends class notation with the class of geometries fulfilling Euclid's axiom.
class TarskiGE
Syntax	citv 28396	Declare the syntax for the Interval (segment) index extractor.
class Itv
Syntax	clng 28397	Declare the syntax for the Line function.
class LineG
Definition	df-itv 28398	Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) Use its index-independent form itvid 28402 instead. (New usage is discouraged.)
⊢ Itv = Slot ;16
Definition	df-lng 28399	Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) Use its index-independent form lngid 28403 instead. (New usage is discouraged.)
⊢ LineG = Slot ;17
Theorem	itvndx 28400	Index value of the Interval (segment) slot. Use ndxarg 17125. (Contributed by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.)
⊢ (Itv‘ndx) = ;16