Metamath Proof Explorer

Theorem zs12bday

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

Ref Expression
Assertion zs12bday 
|- ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om )

Proof

Step Hyp Ref Expression
1 elzs12 
 |-  ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) )
2 fvoveq1 
 |-  ( z = x -> ( bday ` ( z /su ( 2s ^su y ) ) ) = ( bday ` ( x /su ( 2s ^su y ) ) ) )
3 2 eleq1d 
 |-  ( z = x -> ( ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om <-> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) )
4 oveq2 
 |-  ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) )
5 2sno 
 |-  2s e. No
6 exps0 
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
7 5 6 ax-mp 
 |-  ( 2s ^su 0s ) = 1s
8 4 7 eqtrdi 
 |-  ( m = 0s -> ( 2s ^su m ) = 1s )
9 8 oveq2d 
 |-  ( m = 0s -> ( z /su ( 2s ^su m ) ) = ( z /su 1s ) )
10 9 fveq2d 
 |-  ( m = 0s -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su 1s ) ) )
11 10 eleq1d 
 |-  ( m = 0s -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su 1s ) ) e. _om ) )
12 11 ralbidv 
 |-  ( m = 0s -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su 1s ) ) e. _om ) )
13 oveq2 
 |-  ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) )
14 13 oveq2d 
 |-  ( m = n -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su n ) ) )
15 14 fveq2d 
 |-  ( m = n -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su n ) ) ) )
16 15 eleq1d 
 |-  ( m = n -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) )
17 16 ralbidv 
 |-  ( m = n -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) )
18 oveq2 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) )
19 18 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su ( n +s 1s ) ) ) )
20 19 fveq2d 
 |-  ( m = ( n +s 1s ) -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) )
21 20 eleq1d 
 |-  ( m = ( n +s 1s ) -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
22 21 ralbidv 
 |-  ( m = ( n +s 1s ) -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
23 fvoveq1 
 |-  ( z = w -> ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) )
24 23 eleq1d 
 |-  ( z = w -> ( ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
25 24 cbvralvw 
 |-  ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
26 22 25 bitrdi 
 |-  ( m = ( n +s 1s ) -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
27 oveq2 
 |-  ( m = y -> ( 2s ^su m ) = ( 2s ^su y ) )
28 27 oveq2d 
 |-  ( m = y -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su y ) ) )
29 28 fveq2d 
 |-  ( m = y -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su y ) ) ) )
30 29 eleq1d 
 |-  ( m = y -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) )
31 30 ralbidv 
 |-  ( m = y -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) )
32 zno 
 |-  ( z e. ZZ_s -> z e. No )
33 divs1 
 |-  ( z e. No -> ( z /su 1s ) = z )
34 32 33 syl 
 |-  ( z e. ZZ_s -> ( z /su 1s ) = z )
35 34 fveq2d 
 |-  ( z e. ZZ_s -> ( bday ` ( z /su 1s ) ) = ( bday ` z ) )
36 zsbday 
 |-  ( z e. ZZ_s -> ( bday ` z ) e. _om )
37 35 36 eqeltrd 
 |-  ( z e. ZZ_s -> ( bday ` ( z /su 1s ) ) e. _om )
38 37 rgen 
 |-  A. z e. ZZ_s ( bday ` ( z /su 1s ) ) e. _om
39 zseo 
 |-  ( w e. ZZ_s -> ( E. t e. ZZ_s w = ( 2s x.s t ) \/ E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) ) )
40 expsp1 
 |-  ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) )
41 5 40 mpan 
 |-  ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) )
42 41 adantr 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) )
43 42 oveq2d 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s t ) /su ( ( 2s ^su n ) x.s 2s ) ) )
44 5 a1i 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> 2s e. No )
45 zno 
 |-  ( t e. ZZ_s -> t e. No )
46 45 adantl 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> t e. No )
47 44 46 mulscld 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s x.s t ) e. No )
48 expscl 
 |-  ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No )
49 5 48 mpan 
 |-  ( n e. NN0_s -> ( 2s ^su n ) e. No )
50 49 adantr 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su n ) e. No )
51 2ne0s 
 |-  2s =/= 0s
52 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ n e. NN0_s ) -> ( 2s ^su n ) =/= 0s )
53 5 51 52 mp3an12 
 |-  ( n e. NN0_s -> ( 2s ^su n ) =/= 0s )
54 53 adantr 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su n ) =/= 0s )
55 51 a1i 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> 2s =/= 0s )
56 47 50 44 54 55 divdivs1d 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) /su ( 2s ^su n ) ) /su 2s ) = ( ( 2s x.s t ) /su ( ( 2s ^su n ) x.s 2s ) ) )
57 44 46 50 54 divsassd 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su n ) ) = ( 2s x.s ( t /su ( 2s ^su n ) ) ) )
58 57 oveq1d 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) /su ( 2s ^su n ) ) /su 2s ) = ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) )
59 43 56 58 3eqtr2d 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) )
60 46 50 54 divscld 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) e. No )
61 60 44 55 divscan3d 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) = ( t /su ( 2s ^su n ) ) )
62 59 61 eqtrd 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( t /su ( 2s ^su n ) ) )
63 62 fveq2d 
 |-  ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) )
64 63 adantlr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) )
65 fvoveq1 
 |-  ( z = t -> ( bday ` ( z /su ( 2s ^su n ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) )
66 65 eleq1d 
 |-  ( z = t -> ( ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om <-> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) )
67 66 rspccva 
 |-  ( ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om /\ t e. ZZ_s ) -> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om )
68 67 adantll 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om )
69 64 68 eqeltrd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
70 fvoveq1 
 |-  ( w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
71 70 eleq1d 
 |-  ( w = ( 2s x.s t ) -> ( ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
72 69 71 syl5ibrcom 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
73 72 rexlimdva 
 |-  ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( E. t e. ZZ_s w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
74 45 adantl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t e. No )
75 no2times 
 |-  ( t e. No -> ( 2s x.s t ) = ( t +s t ) )
76 74 75 syl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) = ( t +s t ) )
77 76 oveq1d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( ( t +s t ) +s 1s ) )
78 1sno 
 |-  1s e. No
79 78 a1i 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 1s e. No )
80 74 74 79 addsassd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( t +s t ) +s 1s ) = ( t +s ( t +s 1s ) ) )
81 77 80 eqtrd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( t +s ( t +s 1s ) ) )
82 81 oveq1d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( t +s ( t +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
83 74 79 addscld 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t +s 1s ) e. No )
84 simpll 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> n e. NN0_s )
85 74 sltp1d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t
86 2nns 
 |-  2s e. NN_s
87 nnzs 
 |-  ( 2s e. NN_s -> 2s e. ZZ_s )
88 86 87 mp1i 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 2s e. ZZ_s )
89 simpr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t e. ZZ_s )
90 88 89 zmulscld 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) e. ZZ_s )
91 90 znod 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) e. No )
92 pncans 
 |-  ( ( ( 2s x.s t ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s t ) +s 1s ) -s 1s ) = ( 2s x.s t ) )
93 91 78 92 sylancl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) -s 1s ) = ( 2s x.s t ) )
94 93 eqcomd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) = ( ( ( 2s x.s t ) +s 1s ) -s 1s ) )
95 94 sneqd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( 2s x.s t ) } = { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } )
96 mulsrid 
 |-  ( 2s e. No -> ( 2s x.s 1s ) = 2s )
97 5 96 ax-mp 
 |-  ( 2s x.s 1s ) = 2s
98 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
99 97 98 eqtr4i 
 |-  ( 2s x.s 1s ) = ( 1s +s 1s )
100 99 oveq2i 
 |-  ( ( 2s x.s t ) +s ( 2s x.s 1s ) ) = ( ( 2s x.s t ) +s ( 1s +s 1s ) )
101 5 a1i 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 2s e. No )
102 101 74 79 addsdid 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s ( t +s 1s ) ) = ( ( 2s x.s t ) +s ( 2s x.s 1s ) ) )
103 91 79 79 addsassd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) +s 1s ) = ( ( 2s x.s t ) +s ( 1s +s 1s ) ) )
104 100 102 103 3eqtr4a 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s ( t +s 1s ) ) = ( ( ( 2s x.s t ) +s 1s ) +s 1s ) )
105 104 sneqd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( 2s x.s ( t +s 1s ) ) } = { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } )
106 95 105 oveq12d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( 2s x.s t ) } |s { ( 2s x.s ( t +s 1s ) ) } ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) )
107 1zs 
 |-  1s e. ZZ_s
108 107 a1i 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 1s e. ZZ_s )
109 90 108 zaddscld 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) e. ZZ_s )
110 zscut 
 |-  ( ( ( 2s x.s t ) +s 1s ) e. ZZ_s -> ( ( 2s x.s t ) +s 1s ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) )
111 109 110 syl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) )
112 106 111 81 3eqtr2d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( 2s x.s t ) } |s { ( 2s x.s ( t +s 1s ) ) } ) = ( t +s ( t +s 1s ) ) )
113 74 83 84 85 112 pw2cut 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) = ( ( t +s ( t +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
114 82 113 eqtr4d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
115 114 fveq2d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
116 49 ad2antrr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s ^su n ) e. No )
117 53 ad2antrr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s ^su n ) =/= 0s )
118 74 116 117 divscld 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) e. No )
119 83 116 117 divscld 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( t +s 1s ) /su ( 2s ^su n ) ) e. No )
120 74 116 117 divscan2d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) ) = t )
121 120 85 eqbrtrd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) )
122 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
123 86 122 ax-mp 
 |-  0s
124 expsgt0 
 |-  ( ( 2s e. No /\ n e. NN0_s /\ 0s  0s
125 5 123 124 mp3an13 
 |-  ( n e. NN0_s -> 0s
126 125 ad2antrr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 0s
127 118 83 116 126 sltmuldiv2d 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) )  ( t /su ( 2s ^su n ) )
128 121 127 mpbid 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) )
129 118 119 128 ssltsn 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( t /su ( 2s ^su n ) ) } <
130 imaundi 
 |-  ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
131 130 unieqi 
 |-  U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = U. ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
132 uniun 
 |-  U. ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
133 131 132 eqtri 
 |-  U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
134 bdayfn 
 |-  bday Fn No
135 fnsnfv 
 |-  ( ( bday Fn No /\ ( t /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday " { ( t /su ( 2s ^su n ) ) } ) )
136 134 118 135 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday " { ( t /su ( 2s ^su n ) ) } ) )
137 136 unieqd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. { ( bday ` ( t /su ( 2s ^su n ) ) ) } = U. ( bday " { ( t /su ( 2s ^su n ) ) } ) )
138 fvex 
 |-  ( bday ` ( t /su ( 2s ^su n ) ) ) e. _V
139 138 unisn 
 |-  U. { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday ` ( t /su ( 2s ^su n ) ) )
140 137 139 eqtr3di 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( t /su ( 2s ^su n ) ) } ) = ( bday ` ( t /su ( 2s ^su n ) ) ) )
141 140 68 eqeltrd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( t /su ( 2s ^su n ) ) } ) e. _om )
142 fnsnfv 
 |-  ( ( bday Fn No /\ ( ( t +s 1s ) /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
143 134 119 142 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
144 143 unieqd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) )
145 fvex 
 |-  ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _V
146 145 unisn 
 |-  U. { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) )
147 144 146 eqtr3di 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) )
148 fvoveq1 
 |-  ( z = ( t +s 1s ) -> ( bday ` ( z /su ( 2s ^su n ) ) ) = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) )
149 148 eleq1d 
 |-  ( z = ( t +s 1s ) -> ( ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om <-> ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _om ) )
150 simplr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om )
151 89 108 zaddscld 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t +s 1s ) e. ZZ_s )
152 149 150 151 rspcdva 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _om )
153 147 152 eqeltrd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) e. _om )
154 omun 
 |-  ( ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) e. _om /\ U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) e. _om ) -> ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
155 141 153 154 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
156 133 155 eqeltrid 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
157 peano2 
 |-  ( U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
158 156 157 syl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
159 nnon 
 |-  ( suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On )
160 158 159 syl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On )
161 imassrn 
 |-  ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ ran bday
162 bdayrn 
 |-  ran bday = On
163 161 162 sseqtri 
 |-  ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ On
164 onsucuni 
 |-  ( ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ On -> ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
165 163 164 mp1i 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
166 scutbdaybnd 
 |-  ( ( { ( t /su ( 2s ^su n ) ) } < ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
167 129 160 165 166 syl3anc 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
168 bdayelon 
 |-  ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On
169 onsssuc 
 |-  ( ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On /\ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) -> ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) <-> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) )
170 168 160 169 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) <-> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) )
171 167 170 mpbid 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
172 115 171 eqeltrd 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) )
173 peano2 
 |-  ( suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
174 158 173 syl 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om )
175 elnn 
 |-  ( ( ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) /\ suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
176 172 174 175 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
177 fvoveq1 
 |-  ( w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
178 177 eleq1d 
 |-  ( w = ( ( 2s x.s t ) +s 1s ) -> ( ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
179 176 178 syl5ibrcom 
 |-  ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
180 179 rexlimdva 
 |-  ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
181 73 180 jaod 
 |-  ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( ( E. t e. ZZ_s w = ( 2s x.s t ) \/ E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
182 39 181 syl5 
 |-  ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( w e. ZZ_s -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
183 182 ralrimiv 
 |-  ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om )
184 183 ex 
 |-  ( n e. NN0_s -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om -> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) )
185 12 17 26 31 38 184 n0sind 
 |-  ( y e. NN0_s -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om )
186 185 adantl 
 |-  ( ( x e. ZZ_s /\ y e. NN0_s ) -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om )
187 simpl 
 |-  ( ( x e. ZZ_s /\ y e. NN0_s ) -> x e. ZZ_s )
188 3 186 187 rspcdva 
 |-  ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om )
189 fveq2 
 |-  ( A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) = ( bday ` ( x /su ( 2s ^su y ) ) ) )
190 189 eleq1d 
 |-  ( A = ( x /su ( 2s ^su y ) ) -> ( ( bday ` A ) e. _om <-> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) )
191 188 190 syl5ibrcom 
 |-  ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) e. _om ) )
192 191 rexlimivv 
 |-  ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) e. _om )
193 1 192 sylbi 
 |-  ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om )