Metamath Proof Explorer

Theorem pw2bday

Description: The inverses of powers of two have finite birthdays. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Assertion pw2bday 
|- ( N e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) )
2 2sno 
 |-  2s e. No
3 exps0 
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
4 2 3 ax-mp 
 |-  ( 2s ^su 0s ) = 1s
5 1 4 eqtrdi 
 |-  ( m = 0s -> ( 2s ^su m ) = 1s )
6 5 oveq2d 
 |-  ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su 1s ) )
7 1sno 
 |-  1s e. No
8 divs1 
 |-  ( 1s e. No -> ( 1s /su 1s ) = 1s )
9 7 8 ax-mp 
 |-  ( 1s /su 1s ) = 1s
10 6 9 eqtrdi 
 |-  ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = 1s )
11 10 fveq2d 
 |-  ( m = 0s -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` 1s ) )
12 bday1s 
 |-  ( bday ` 1s ) = 1o
13 11 12 eqtrdi 
 |-  ( m = 0s -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = 1o )
14 13 eleq1d 
 |-  ( m = 0s -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> 1o e. _om ) )
15 oveq2 
 |-  ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) )
16 15 oveq2d 
 |-  ( m = n -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su n ) ) )
17 16 fveq2d 
 |-  ( m = n -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
18 17 eleq1d 
 |-  ( m = n -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) )
19 oveq2 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) )
20 19 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
21 20 fveq2d 
 |-  ( m = ( n +s 1s ) -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) )
22 21 eleq1d 
 |-  ( m = ( n +s 1s ) -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
23 oveq2 
 |-  ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) )
24 23 oveq2d 
 |-  ( m = N -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su N ) ) )
25 24 fveq2d 
 |-  ( m = N -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su N ) ) ) )
26 25 eleq1d 
 |-  ( m = N -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om ) )
27 1onn 
 |-  1o e. _om
28 cutpw2 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) )
29 28 fveq2d 
 |-  ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) )
30 0sno 
 |-  0s e. No
31 30 a1i 
 |-  ( n e. NN0_s -> 0s e. No )
32 7 a1i 
 |-  ( n e. NN0_s -> 1s e. No )
33 expscl 
 |-  ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No )
34 2 33 mpan 
 |-  ( n e. NN0_s -> ( 2s ^su n ) e. No )
35 2ne0s 
 |-  2s =/= 0s
36 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ n e. NN0_s ) -> ( 2s ^su n ) =/= 0s )
37 2 35 36 mp3an12 
 |-  ( n e. NN0_s -> ( 2s ^su n ) =/= 0s )
38 32 34 37 divscld 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su n ) ) e. No )
39 muls02 
 |-  ( ( 2s ^su n ) e. No -> ( 0s x.s ( 2s ^su n ) ) = 0s )
40 34 39 syl 
 |-  ( n e. NN0_s -> ( 0s x.s ( 2s ^su n ) ) = 0s )
41 0slt1s 
 |-  0s
42 40 41 eqbrtrdi 
 |-  ( n e. NN0_s -> ( 0s x.s ( 2s ^su n ) )
43 2nns 
 |-  2s e. NN_s
44 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
45 43 44 ax-mp 
 |-  0s
46 expsgt0 
 |-  ( ( 2s e. No /\ n e. NN0_s /\ 0s  0s
47 2 45 46 mp3an13 
 |-  ( n e. NN0_s -> 0s
48 31 32 34 47 sltmuldivd 
 |-  ( n e. NN0_s -> ( ( 0s x.s ( 2s ^su n ) )  0s
49 42 48 mpbid 
 |-  ( n e. NN0_s -> 0s
50 31 38 49 ssltsn 
 |-  ( n e. NN0_s -> { 0s } <
51 suc0 
 |-  suc (/) = { (/) }
52 bday0s 
 |-  ( bday ` 0s ) = (/)
53 52 sneqi 
 |-  { ( bday ` 0s ) } = { (/) }
54 bdayfn 
 |-  bday Fn No
55 fnsnfv 
 |-  ( ( bday Fn No /\ 0s e. No ) -> { ( bday ` 0s ) } = ( bday " { 0s } ) )
56 54 30 55 mp2an 
 |-  { ( bday ` 0s ) } = ( bday " { 0s } )
57 51 53 56 3eqtr2i 
 |-  suc (/) = ( bday " { 0s } )
58 57 a1i 
 |-  ( n e. NN0_s -> suc (/) = ( bday " { 0s } ) )
59 fnsnfv 
 |-  ( ( bday Fn No /\ ( 1s /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) )
60 54 59 mpan 
 |-  ( ( 1s /su ( 2s ^su n ) ) e. No -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) )
61 38 60 syl 
 |-  ( n e. NN0_s -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) )
62 58 61 uneq12d 
 |-  ( n e. NN0_s -> ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) = ( ( bday " { 0s } ) u. ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) )
63 imaundi 
 |-  ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) = ( ( bday " { 0s } ) u. ( bday " { ( 1s /su ( 2s ^su n ) ) } ) )
64 62 63 eqtr4di 
 |-  ( n e. NN0_s -> ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) = ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) )
65 0ss 
 |-  (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) )
66 ord0 
 |-  Ord (/)
67 bdayelon 
 |-  ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On
68 67 onordi 
 |-  Ord ( bday ` ( 1s /su ( 2s ^su n ) ) )
69 ordsucsssuc 
 |-  ( ( Ord (/) /\ Ord ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) -> ( (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) )
70 66 68 69 mp2an 
 |-  ( (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
71 65 70 mpbi 
 |-  suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) )
72 fvex 
 |-  ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _V
73 72 sucid 
 |-  ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. suc ( bday ` ( 1s /su ( 2s ^su n ) ) )
74 snssi 
 |-  ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
75 73 74 ax-mp 
 |-  { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) )
76 71 75 unssi 
 |-  ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) )
77 64 76 eqsstrrdi 
 |-  ( n e. NN0_s -> ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
78 67 onsuci 
 |-  suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On
79 scutbdaybnd 
 |-  ( ( { 0s } < ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
80 78 79 mp3an2 
 |-  ( ( { 0s } < ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
81 50 77 80 syl2anc 
 |-  ( n e. NN0_s -> ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
82 29 81 eqsstrd 
 |-  ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
83 bdayelon 
 |-  ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. On
84 onsssuc 
 |-  ( ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On ) -> ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) )
85 83 78 84 mp2an 
 |-  ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
86 82 85 sylib 
 |-  ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) )
87 peano2 
 |-  ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om )
88 peano2 
 |-  ( suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om )
89 87 88 syl 
 |-  ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om )
90 elnn 
 |-  ( ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) /\ suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
91 86 89 90 syl2an 
 |-  ( ( n e. NN0_s /\ ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
92 91 ex 
 |-  ( n e. NN0_s -> ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
93 14 18 22 26 27 92 n0sind 
 |-  ( N e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om )