P. 285 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28401-28500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zseo 28401*	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 28402	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 28403	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 28404	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 28405	Value of surreal exponentiation at a natural number. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕs) → (𝐴↑s𝑁) = (seqs 1s ( ·s , (ℕs × {𝐴}))‘𝑁))
Theorem	exps0 28406	Surreal exponentiation to zero. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ (𝐴 ∈ No → (𝐴↑s 0s ) = 1s )
Theorem	exps1 28407	Surreal exponentiation to one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ (𝐴 ∈ No → (𝐴↑s 1s ) = 𝐴)
Theorem	expsp1 28408	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 28409*	Lemma for proving non-negative surreal integer exponentiation closure. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ 𝐹 ⊆ No     &   ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ·s 𝑦) ∈ 𝐹)    &   ⊢ 1s ∈ 𝐹    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ 𝐹)
Theorem	expscl 28410	Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ No )
Theorem	n0expscl 28411	Closure law for non-negative surreal integer exponentiation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℕ0s)
Theorem	nnexpscl 28412	Closure law for positive surreal integer exponentiation. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℕs)
Theorem	zexpscl 28413	Closure law for surreal integer exponentiation. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ ((𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s𝑁) ∈ ℤs)
Theorem	expadds 28414	Sum of exponents law for surreals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝐴↑s(𝑀 +s 𝑁)) = ((𝐴↑s𝑀) ·s (𝐴↑s𝑁)))
Theorem	expsne0 28415	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 28416	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 28417*	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 28418	Division closure for powers of two. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 /su (2s↑s𝑁)) ∈ No )
Theorem	pw2divsmuld 28419	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 28420	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 28421	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 28422	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 28423	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 28424	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 28425	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 28426	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 28427	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 28428	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 28429	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 28430	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	pw2sltdiv1d 28431	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	avgslt1d 28432	Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 𝐴 <s ((𝐴 +s 𝐵) /su 2s)))
Theorem	avgslt2d 28433	Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ((𝐴 +s 𝐵) /su 2s) <s 𝐵))
Theorem	pw2divs0d 28434	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 28435	Identity law for division over powers of two. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ (𝜑 → 𝑁 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → ((2s↑s𝑁) /su (2s↑s𝑁)) = 1s )
Theorem	pw2sltdivmul2d 28436	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 28437	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 28438	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 28439	Extend halfcut 28437 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 28440	Simplify pw2cut 28439 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 28441	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	bdaypw2n0sbndlem 28442	Lemma for bdaypw2n0sbnd 28443. 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	bdaypw2n0sbnd 28443	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 28444	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 28445*	Lemma for bdayfinbnd 28448. 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 28446*	Lemma for bdayfinbnd 28448. 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 28447*	Lemma for bdayfinbnd 28448. 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 28448*	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	zs12bdaylem1 28449	Lemma for zs12bday 28464. 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	zs12bdaylem2 28450	Lemma for zs12bday 28464. 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	elzs12 28451*	Membership in the dyadic fractions. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝐴 ∈ ℤs[1/2] ↔ ∃𝑥 ∈ ℤs ∃𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su (2s↑s𝑦)))
Theorem	elzs12i 28452	Inference form of membership in the dyadic fractions. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ ((𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s) → (𝐴 /su (2s↑s𝑁)) ∈ ℤs[1/2])
Theorem	zs12ex 28453	The class of dyadic fractions is a set. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ ℤs[1/2] ∈ V
Theorem	zzs12 28454	A surreal integer is a dyadic fraction. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ ℤs[1/2])
Theorem	zs12no 28455	A dyadic is a surreal. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No )
Theorem	zs12addscl 28456	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 28457	The dyadics are closed under negation. (Contributed by Scott Fenton, 9-Nov-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → ( -us ‘𝐴) ∈ ℤs[1/2])
Theorem	zs12subscl 28458	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 28459	Half of a dyadic is a dyadic. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → (𝐴 /su 2s) ∈ ℤs[1/2])
Theorem	zs12negsclb 28460	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 28461*	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 28462*	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	zs12bdaylem 28463	Lemma for zs12bday 28464. Handle the non-negative case. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴) → ( bday ‘𝐴) ∈ ω)
Theorem	zs12bday 28464	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 28465	Lemma for bdayfin 28466. Handle the non-negative case. (Contributed by Scott Fenton, 26-Feb-2026.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘𝐴) ∈ ω) → 𝐴 ∈ ℤs[1/2])
Theorem	bdayfin 28466	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	dfzs122 28467	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 28468	Declare the syntax for the surreal reals.
class ℝs
Definition	df-reno 28469*	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 28470*	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	reno 28471	A surreal real is a surreal number. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (𝐴 ∈ ℝs → 𝐴 ∈ No )
Theorem	renod 28472	A surreal real is a surreal number. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	recut 28473*	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 28474*	Alternate characterization of the surreal reals. Theorem 4.4(b) of [Gonshor] p. 39. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)))))
Theorem	0reno 28475	Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 0s ∈ ℝs
Theorem	1reno 28476	Surreal one is a surreal real. (Contributed by Scott Fenton, 18-Feb-2026.)
⊢ 1s ∈ ℝs
Theorem	renegscl 28477	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 28478	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 28479*	Lemma for remulscl 28481. 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 28480*	Lemma for remulscl 28481. 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 28481	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 28508 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17078). 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 28530 and tgjustc2 28531, which in turn are supported by tgjustf 28528 and tgjustr 28529. 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/ 28529. 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 1549 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 28508), of "Euclidean dimensionless Tarski structures" (df-trkge 28506) and of "Tarski structures of dimension no less than N" (df-trkgld 28507). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 28863 and iscgra 28864). 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 28566. 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 28482	Extends class notation with the class of Tarski geometries.
class TarskiG
Syntax	cstrkgc 28483	Extends class notation with the class of geometries fulfilling the congruence axioms.
class TarskiGC
Syntax	cstrkgb 28484	Extends class notation with the class of geometries fulfilling the betweenness axioms.
class TarskiGB
Syntax	cstrkgcb 28485	Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms.
class TarskiGCB
Syntax	cstrkgld 28486	Extends class notation with the relation for geometries fulfilling the lower dimension axioms.
class DimTarskiG≥
Syntax	cstrkge 28487	Extends class notation with the class of geometries fulfilling Euclid's axiom.
class TarskiGE
Syntax	citv 28488	Declare the syntax for the Interval (segment) index extractor.
class Itv
Syntax	clng 28489	Declare the syntax for the Line function.
class LineG
Definition	df-itv 28490	Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) Use its index-independent form itvid 28494 instead. (New usage is discouraged.)
⊢ Itv = Slot ;16
Definition	df-lng 28491	Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) Use its index-independent form lngid 28495 instead. (New usage is discouraged.)
⊢ LineG = Slot ;17
Theorem	itvndx 28492	Index value of the Interval (segment) slot. Use ndxarg 17127. (Contributed by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.)
⊢ (Itv‘ndx) = ;16
Theorem	lngndx 28493	Index value of the "line" slot. Use ndxarg 17127. (Contributed by Thierry Arnoux, 27-Mar-2019.) (New usage is discouraged.)
⊢ (LineG‘ndx) = ;17
Theorem	itvid 28494	Utility theorem: index-independent form of df-itv 28490. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ Itv = Slot (Itv‘ndx)
Theorem	lngid 28495	Utility theorem: index-independent form of df-lng 28491. (Contributed by Thierry Arnoux, 27-Mar-2019.)
⊢ LineG = Slot (LineG‘ndx)
Theorem	slotsinbpsd 28496	The slots Base, +g, ·𝑠 and dist are different from the slot Itv. Formerly part of ttglem 28931 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ (((Itv‘ndx) ≠ (Base‘ndx) ∧ (Itv‘ndx) ≠ (+g‘ndx)) ∧ ((Itv‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (Itv‘ndx) ≠ (dist‘ndx)))
Theorem	slotslnbpsd 28497	The slots Base, +g, ·𝑠 and dist are different from the slot LineG. Formerly part of ttglem 28931 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ (((LineG‘ndx) ≠ (Base‘ndx) ∧ (LineG‘ndx) ≠ (+g‘ndx)) ∧ ((LineG‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (LineG‘ndx) ≠ (dist‘ndx)))
Theorem	lngndxnitvndx 28498	The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval 28930. (Contributed by AV, 9-Nov-2024.)
⊢ (LineG‘ndx) ≠ (Itv‘ndx)
Theorem	trkgstr 28499	Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝑈⟩, ⟨(dist‘ndx), 𝐷⟩, ⟨(Itv‘ndx), 𝐼⟩}    ⇒   ⊢ 𝑊 Struct ⟨1, ;16⟩
Theorem	trkgbas 28500	The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝑈⟩, ⟨(dist‘ndx), 𝐷⟩, ⟨(Itv‘ndx), 𝐼⟩}    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝑈 = (Base‘𝑊))