Theorem bdayfin

Description: A surreal has a finite birthday iff it is a dyadic fraction. (Contributed by Scott Fenton, 26-Feb-2026)

	Ref	Expression
Assertion	bdayfin	⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ℤs[1/2] ↔ ( bday ‘ 𝐴 ) ∈ ω ) )

Proof

Step	Hyp	Ref	Expression
1		z12bday	⊢ ( 𝐴 ∈ ℤs[1/2] → ( bday ‘ 𝐴 ) ∈ ω )
2		bdayfinlem	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 𝐴 ∈ ℤs[1/2] )
3	2	3exp	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 → ( ( bday ‘ 𝐴 ) ∈ ω → 𝐴 ∈ ℤs[1/2] ) ) )
4		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
5		bdayfinlem	⊢ ( ( ( -us ‘ 𝐴 ) ∈ No ∧ 0s ≤s ( -us ‘ 𝐴 ) ∧ ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] )
6	5	3expib	⊢ ( ( -us ‘ 𝐴 ) ∈ No → ( ( 0s ≤s ( -us ‘ 𝐴 ) ∧ ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ) )
7	4 6	syl	⊢ ( 𝐴 ∈ No → ( ( 0s ≤s ( -us ‘ 𝐴 ) ∧ ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ) )
8		0no	⊢ 0s ∈ No
9		lenegs	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
10	8 9	mpan2	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
11		neg0s	⊢ ( -us ‘ 0s ) = 0s
12	11	breq1i	⊢ ( ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ↔ 0s ≤s ( -us ‘ 𝐴 ) )
13	10 12	bitrdi	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s ↔ 0s ≤s ( -us ‘ 𝐴 ) ) )
14		negbday	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
15	14	eqcomd	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ( bday ‘ ( -us ‘ 𝐴 ) ) )
16	15	eleq1d	⊢ ( 𝐴 ∈ No → ( ( bday ‘ 𝐴 ) ∈ ω ↔ ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) )
17	13 16	anbi12d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ≤s 0s ∧ ( bday ‘ 𝐴 ) ∈ ω ) ↔ ( 0s ≤s ( -us ‘ 𝐴 ) ∧ ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) ) )
18		z12negsclb	⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ℤs[1/2] ↔ ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ) )
19	7 17 18	3imtr4d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ≤s 0s ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 𝐴 ∈ ℤs[1/2] ) )
20	19	expd	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s → ( ( bday ‘ 𝐴 ) ∈ ω → 𝐴 ∈ ℤs[1/2] ) ) )
21		lestric	⊢ ( ( 0s ∈ No ∧ 𝐴 ∈ No ) → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
22	8 21	mpan	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
23	3 20 22	mpjaod	⊢ ( 𝐴 ∈ No → ( ( bday ‘ 𝐴 ) ∈ ω → 𝐴 ∈ ℤs[1/2] ) )
24	1 23	impbid2	⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ℤs[1/2] ↔ ( bday ‘ 𝐴 ) ∈ ω ) )