Metamath Proof Explorer

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 
|- ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om )

Proof

Step Hyp Ref Expression
1 z12bdaylem 
 |-  ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( bday ` A ) e. _om )
2 0no 
 |-  0s e. No
3 z12no 
 |-  ( A e. ZZ_s[1/2] -> A e. No )
4 lestric 
 |-  ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
5 2 3 4 sylancr 
 |-  ( A e. ZZ_s[1/2] -> ( 0s <_s A \/ A <_s 0s ) )
6 5 ord 
 |-  ( A e. ZZ_s[1/2] -> ( -. 0s <_s A -> A <_s 0s ) )
7 lenegs 
 |-  ( ( A e. No /\ 0s e. No ) -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
8 3 2 7 sylancl 
 |-  ( A e. ZZ_s[1/2] -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
9 neg0s 
 |-  ( -us ` 0s ) = 0s
10 9 breq1i 
 |-  ( ( -us ` 0s ) <_s ( -us ` A ) <-> 0s <_s ( -us ` A ) )
11 8 10 bitrdi 
 |-  ( A e. ZZ_s[1/2] -> ( A <_s 0s <-> 0s <_s ( -us ` A ) ) )
12 z12negscl 
 |-  ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] )
13 z12bdaylem 
 |-  ( ( ( -us ` A ) e. ZZ_s[1/2] /\ 0s <_s ( -us ` A ) ) -> ( bday ` ( -us ` A ) ) e. _om )
14 13 ex 
 |-  ( ( -us ` A ) e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` ( -us ` A ) ) e. _om ) )
15 12 14 syl 
 |-  ( A e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` ( -us ` A ) ) e. _om ) )
16 negbday 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
17 3 16 syl 
 |-  ( A e. ZZ_s[1/2] -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
18 17 eleq1d 
 |-  ( A e. ZZ_s[1/2] -> ( ( bday ` ( -us ` A ) ) e. _om <-> ( bday ` A ) e. _om ) )
19 15 18 sylibd 
 |-  ( A e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` A ) e. _om ) )
20 11 19 sylbid 
 |-  ( A e. ZZ_s[1/2] -> ( A <_s 0s -> ( bday ` A ) e. _om ) )
21 6 20 syld 
 |-  ( A e. ZZ_s[1/2] -> ( -. 0s <_s A -> ( bday ` A ) e. _om ) )
22 21 imp 
 |-  ( ( A e. ZZ_s[1/2] /\ -. 0s <_s A ) -> ( bday ` A ) e. _om )
23 1 22 pm2.61dan 
 |-  ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om )