Theorem z12bday

Description: A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025) (Proof shortened by Scott Fenton, 22-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		z12bdaylem	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴 ) → ( bday ‘ 𝐴 ) ∈ ω )
2		0no	⊢ 0s ∈ No
3		z12no	⊢ ( 𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No )
4		lestric	⊢ ( ( 0s ∈ No ∧ 𝐴 ∈ No ) → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
5	2 3 4	sylancr	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
6	5	ord	⊢ ( 𝐴 ∈ ℤs[1/2] → ( ¬ 0s ≤s 𝐴 → 𝐴 ≤s 0s ) )
7		lenegs	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
8	3 2 7	sylancl	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
9		neg0s	⊢ ( -us ‘ 0s ) = 0s
10	9	breq1i	⊢ ( ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ↔ 0s ≤s ( -us ‘ 𝐴 ) )
11	8 10	bitrdi	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ≤s 0s ↔ 0s ≤s ( -us ‘ 𝐴 ) ) )
12		z12negscl	⊢ ( 𝐴 ∈ ℤs[1/2] → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] )
13		z12bdaylem	⊢ ( ( ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ∧ 0s ≤s ( -us ‘ 𝐴 ) ) → ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω )
14	13	ex	⊢ ( ( -us ‘ 𝐴 ) ∈ ℤs[1/2] → ( 0s ≤s ( -us ‘ 𝐴 ) → ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) )
15	12 14	syl	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 0s ≤s ( -us ‘ 𝐴 ) → ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ) )
16		negbday	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
17	3 16	syl	⊢ ( 𝐴 ∈ ℤs[1/2] → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
18	17	eleq1d	⊢ ( 𝐴 ∈ ℤs[1/2] → ( ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω ↔ ( bday ‘ 𝐴 ) ∈ ω ) )
19	15 18	sylibd	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 0s ≤s ( -us ‘ 𝐴 ) → ( bday ‘ 𝐴 ) ∈ ω ) )
20	11 19	sylbid	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ≤s 0s → ( bday ‘ 𝐴 ) ∈ ω ) )
21	6 20	syld	⊢ ( 𝐴 ∈ ℤs[1/2] → ( ¬ 0s ≤s 𝐴 → ( bday ‘ 𝐴 ) ∈ ω ) )
22	21	imp	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ ¬ 0s ≤s 𝐴 ) → ( bday ‘ 𝐴 ) ∈ ω )
23	1 22	pm2.61dan	⊢ ( 𝐴 ∈ ℤs[1/2] → ( bday ‘ 𝐴 ) ∈ ω )