Metamath Proof Explorer

Theorem bdaypw2n0s

Description: Upper bound for the birthday of a proper fraction of a power of two. This is actually a strict equality, but we do not need this for the rest of our development. (Contributed by Scott Fenton, 21-Feb-2026)

Ref Expression
Assertion bdaypw2n0s 
|- ( ( A e. NN0_s /\ N e. NN0_s /\ A  ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( m = 0s -> ( m +s 1s ) = ( 0s +s 1s ) )
2 1sno 
 |-  1s e. No
3 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
4 2 3 ax-mp 
 |-  ( 0s +s 1s ) = 1s
5 1 4 eqtrdi 
 |-  ( m = 0s -> ( m +s 1s ) = 1s )
6 5 oveq2d 
 |-  ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su 1s ) )
7 2sno 
 |-  2s e. No
8 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
9 7 8 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
10 6 9 eqtrdi 
 |-  ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = 2s )
11 10 breq2d 
 |-  ( m = 0s -> ( a  a
12 10 oveq2d 
 |-  ( m = 0s -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su 2s ) )
13 12 fveq2d 
 |-  ( m = 0s -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su 2s ) ) )
14 5 fveq2d 
 |-  ( m = 0s -> ( bday ` ( m +s 1s ) ) = ( bday ` 1s ) )
15 bday1s 
 |-  ( bday ` 1s ) = 1o
16 14 15 eqtrdi 
 |-  ( m = 0s -> ( bday ` ( m +s 1s ) ) = 1o )
17 16 suceqd 
 |-  ( m = 0s -> suc ( bday ` ( m +s 1s ) ) = suc 1o )
18 df-2o 
 |-  2o = suc 1o
19 17 18 eqtr4di 
 |-  ( m = 0s -> suc ( bday ` ( m +s 1s ) ) = 2o )
20 13 19 sseq12d 
 |-  ( m = 0s -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su 2s ) ) C_ 2o ) )
21 11 20 imbi12d 
 |-  ( m = 0s -> ( ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a  ( bday ` ( a /su 2s ) ) C_ 2o ) ) )
22 21 ralbidv 
 |-  ( m = 0s -> ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a  ( bday ` ( a /su 2s ) ) C_ 2o ) ) )
23 oveq1 
 |-  ( m = n -> ( m +s 1s ) = ( n +s 1s ) )
24 23 oveq2d 
 |-  ( m = n -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( n +s 1s ) ) )
25 24 breq2d 
 |-  ( m = n -> ( a  a
26 24 oveq2d 
 |-  ( m = n -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) )
27 26 fveq2d 
 |-  ( m = n -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) )
28 23 fveq2d 
 |-  ( m = n -> ( bday ` ( m +s 1s ) ) = ( bday ` ( n +s 1s ) ) )
29 28 suceqd 
 |-  ( m = n -> suc ( bday ` ( m +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) )
30 27 29 sseq12d 
 |-  ( m = n -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
31 25 30 imbi12d 
 |-  ( m = n -> ( ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
32 31 ralbidv 
 |-  ( m = n -> ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
33 oveq1 
 |-  ( m = ( n +s 1s ) -> ( m +s 1s ) = ( ( n +s 1s ) +s 1s ) )
34 33 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( ( n +s 1s ) +s 1s ) ) )
35 34 breq2d 
 |-  ( m = ( n +s 1s ) -> ( a  a
36 34 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) )
37 36 fveq2d 
 |-  ( m = ( n +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) )
38 33 fveq2d 
 |-  ( m = ( n +s 1s ) -> ( bday ` ( m +s 1s ) ) = ( bday ` ( ( n +s 1s ) +s 1s ) ) )
39 38 suceqd 
 |-  ( m = ( n +s 1s ) -> suc ( bday ` ( m +s 1s ) ) = suc ( bday ` ( ( n +s 1s ) +s 1s ) ) )
40 37 39 sseq12d 
 |-  ( m = ( n +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
41 35 40 imbi12d 
 |-  ( m = ( n +s 1s ) -> ( ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
42 41 ralbidv 
 |-  ( m = ( n +s 1s ) -> ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
43 oveq1 
 |-  ( m = N -> ( m +s 1s ) = ( N +s 1s ) )
44 43 oveq2d 
 |-  ( m = N -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) )
45 44 breq2d 
 |-  ( m = N -> ( a  a
46 44 oveq2d 
 |-  ( m = N -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( N +s 1s ) ) ) )
47 46 fveq2d 
 |-  ( m = N -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) )
48 43 fveq2d 
 |-  ( m = N -> ( bday ` ( m +s 1s ) ) = ( bday ` ( N +s 1s ) ) )
49 48 suceqd 
 |-  ( m = N -> suc ( bday ` ( m +s 1s ) ) = suc ( bday ` ( N +s 1s ) ) )
50 47 49 sseq12d 
 |-  ( m = N -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) )
51 45 50 imbi12d 
 |-  ( m = N -> ( ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a  ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) )
52 51 ralbidv 
 |-  ( m = N -> ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) )
53 1n0s 
 |-  1s e. NN0_s
54 n0sleltp1 
 |-  ( ( a e. NN0_s /\ 1s e. NN0_s ) -> ( a <_s 1s <-> a
55 53 54 mpan2 
 |-  ( a e. NN0_s -> ( a <_s 1s <-> a
56 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
57 56 breq2i 
 |-  ( a  a
58 55 57 bitrdi 
 |-  ( a e. NN0_s -> ( a <_s 1s <-> a
59 n0sno 
 |-  ( a e. NN0_s -> a e. No )
60 sleloe 
 |-  ( ( a e. No /\ 1s e. No ) -> ( a <_s 1s <-> ( a
61 59 2 60 sylancl 
 |-  ( a e. NN0_s -> ( a <_s 1s <-> ( a
62 0sno 
 |-  0s e. No
63 sletri3 
 |-  ( ( a e. No /\ 0s e. No ) -> ( a = 0s <-> ( a <_s 0s /\ 0s <_s a ) ) )
64 59 62 63 sylancl 
 |-  ( a e. NN0_s -> ( a = 0s <-> ( a <_s 0s /\ 0s <_s a ) ) )
65 n0sge0 
 |-  ( a e. NN0_s -> 0s <_s a )
66 65 biantrud 
 |-  ( a e. NN0_s -> ( a <_s 0s <-> ( a <_s 0s /\ 0s <_s a ) ) )
67 64 66 bitr4d 
 |-  ( a e. NN0_s -> ( a = 0s <-> a <_s 0s ) )
68 0n0s 
 |-  0s e. NN0_s
69 n0sleltp1 
 |-  ( ( a e. NN0_s /\ 0s e. NN0_s ) -> ( a <_s 0s <-> a
70 68 69 mpan2 
 |-  ( a e. NN0_s -> ( a <_s 0s <-> a
71 67 70 bitrd 
 |-  ( a e. NN0_s -> ( a = 0s <-> a
72 4 breq2i 
 |-  ( a  a
73 71 72 bitrdi 
 |-  ( a e. NN0_s -> ( a = 0s <-> a
74 73 orbi1d 
 |-  ( a e. NN0_s -> ( ( a = 0s \/ a = 1s ) <-> ( a
75 61 74 bitr4d 
 |-  ( a e. NN0_s -> ( a <_s 1s <-> ( a = 0s \/ a = 1s ) ) )
76 58 75 bitr3d 
 |-  ( a e. NN0_s -> ( a  ( a = 0s \/ a = 1s ) ) )
77 oveq1 
 |-  ( a = 0s -> ( a /su 2s ) = ( 0s /su 2s ) )
78 9 oveq2i 
 |-  ( 0s /su ( 2s ^su 1s ) ) = ( 0s /su 2s )
79 53 a1i 
 |-  ( T. -> 1s e. NN0_s )
80 79 pw2divs0d 
 |-  ( T. -> ( 0s /su ( 2s ^su 1s ) ) = 0s )
81 80 mptru 
 |-  ( 0s /su ( 2s ^su 1s ) ) = 0s
82 78 81 eqtr3i 
 |-  ( 0s /su 2s ) = 0s
83 77 82 eqtrdi 
 |-  ( a = 0s -> ( a /su 2s ) = 0s )
84 83 fveq2d 
 |-  ( a = 0s -> ( bday ` ( a /su 2s ) ) = ( bday ` 0s ) )
85 bday0s 
 |-  ( bday ` 0s ) = (/)
86 84 85 eqtrdi 
 |-  ( a = 0s -> ( bday ` ( a /su 2s ) ) = (/) )
87 0ss 
 |-  (/) C_ 2o
88 86 87 eqsstrdi 
 |-  ( a = 0s -> ( bday ` ( a /su 2s ) ) C_ 2o )
89 oveq1 
 |-  ( a = 1s -> ( a /su 2s ) = ( 1s /su 2s ) )
90 nohalf 
 |-  ( 1s /su 2s ) = ( { 0s } |s { 1s } )
91 89 90 eqtrdi 
 |-  ( a = 1s -> ( a /su 2s ) = ( { 0s } |s { 1s } ) )
92 91 fveq2d 
 |-  ( a = 1s -> ( bday ` ( a /su 2s ) ) = ( bday ` ( { 0s } |s { 1s } ) ) )
93 62 a1i 
 |-  ( T. -> 0s e. No )
94 2 a1i 
 |-  ( T. -> 1s e. No )
95 0slt1s 
 |-  0s
96 95 a1i 
 |-  ( T. -> 0s
97 93 94 96 ssltsn 
 |-  ( T. -> { 0s } <
98 97 mptru 
 |-  { 0s } <
99 2on 
 |-  2o e. On
100 df-pr 
 |-  { (/) , 1o } = ( { (/) } u. { 1o } )
101 df2o3 
 |-  2o = { (/) , 1o }
102 imaundi 
 |-  ( bday " ( { 0s } u. { 1s } ) ) = ( ( bday " { 0s } ) u. ( bday " { 1s } ) )
103 bdayfn 
 |-  bday Fn No
104 fnsnfv 
 |-  ( ( bday Fn No /\ 0s e. No ) -> { ( bday ` 0s ) } = ( bday " { 0s } ) )
105 103 62 104 mp2an 
 |-  { ( bday ` 0s ) } = ( bday " { 0s } )
106 85 sneqi 
 |-  { ( bday ` 0s ) } = { (/) }
107 105 106 eqtr3i 
 |-  ( bday " { 0s } ) = { (/) }
108 fnsnfv 
 |-  ( ( bday Fn No /\ 1s e. No ) -> { ( bday ` 1s ) } = ( bday " { 1s } ) )
109 103 2 108 mp2an 
 |-  { ( bday ` 1s ) } = ( bday " { 1s } )
110 15 sneqi 
 |-  { ( bday ` 1s ) } = { 1o }
111 109 110 eqtr3i 
 |-  ( bday " { 1s } ) = { 1o }
112 107 111 uneq12i 
 |-  ( ( bday " { 0s } ) u. ( bday " { 1s } ) ) = ( { (/) } u. { 1o } )
113 102 112 eqtri 
 |-  ( bday " ( { 0s } u. { 1s } ) ) = ( { (/) } u. { 1o } )
114 100 101 113 3eqtr4ri 
 |-  ( bday " ( { 0s } u. { 1s } ) ) = 2o
115 ssid 
 |-  2o C_ 2o
116 114 115 eqsstri 
 |-  ( bday " ( { 0s } u. { 1s } ) ) C_ 2o
117 scutbdaybnd 
 |-  ( ( { 0s } < ( bday ` ( { 0s } |s { 1s } ) ) C_ 2o )
118 98 99 116 117 mp3an 
 |-  ( bday ` ( { 0s } |s { 1s } ) ) C_ 2o
119 92 118 eqsstrdi 
 |-  ( a = 1s -> ( bday ` ( a /su 2s ) ) C_ 2o )
120 88 119 jaoi 
 |-  ( ( a = 0s \/ a = 1s ) -> ( bday ` ( a /su 2s ) ) C_ 2o )
121 76 120 biimtrdi 
 |-  ( a e. NN0_s -> ( a  ( bday ` ( a /su 2s ) ) C_ 2o ) )
122 121 rgen 
 |-  A. a e. NN0_s ( a  ( bday ` ( a /su 2s ) ) C_ 2o )
123 nfv 
 |-  F/ a n e. NN0_s
124 nfra1 
 |-  F/ a A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) )
125 123 124 nfan 
 |-  F/ a ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
126 n0seo 
 |-  ( a e. NN0_s -> ( E. x e. NN0_s a = ( 2s x.s x ) \/ E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) ) )
127 breq1 
 |-  ( a = x -> ( a  x
128 fvoveq1 
 |-  ( a = x -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) )
129 128 sseq1d 
 |-  ( a = x -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
130 127 129 imbi12d 
 |-  ( a = x -> ( ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
131 130 rspccv 
 |-  ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
132 131 adantl 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( x e. NN0_s -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
133 132 imp32 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) )
134 sssucid 
 |-  suc ( bday ` ( n +s 1s ) ) C_ suc suc ( bday ` ( n +s 1s ) )
135 133 134 sstrdi 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc suc ( bday ` ( n +s 1s ) ) )
136 simpll 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> n e. NN0_s )
137 peano2n0s 
 |-  ( n e. NN0_s -> ( n +s 1s ) e. NN0_s )
138 136 137 syl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( n +s 1s ) e. NN0_s )
139 138 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x  ( n +s 1s ) e. NN0_s )
140 bdayn0p1 
 |-  ( ( n +s 1s ) e. NN0_s -> ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) )
141 139 140 syl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x  ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) )
142 141 suceqd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x  suc ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc suc ( bday ` ( n +s 1s ) ) )
143 135 142 sseqtrrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) )
144 143 expr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
145 expsp1 
 |-  ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) )
146 7 138 145 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) )
147 expscl 
 |-  ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No )
148 7 138 147 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No )
149 7 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 2s e. No )
150 148 149 mulscomd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) )
151 146 150 eqtrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) )
152 151 breq2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x )  ( 2s x.s x )
153 n0sno 
 |-  ( x e. NN0_s -> x e. No )
154 153 adantl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> x e. No )
155 2nns 
 |-  2s e. NN_s
156 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
157 155 156 ax-mp 
 |-  0s
158 157 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 0s
159 154 148 149 158 sltmul2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x  ( 2s x.s x )
160 152 159 bitr4d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x )  x
161 53 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 1s e. NN0_s )
162 154 138 161 pw2divscan4d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) )
163 162 fveq2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) )
164 163 sseq1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
165 164 bicomd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
166 144 160 165 3imtr4d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x )  ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
167 breq1 
 |-  ( a = ( 2s x.s x ) -> ( a  ( 2s x.s x )
168 id 
 |-  ( a = ( 2s x.s x ) -> a = ( 2s x.s x ) )
169 9 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s x ) = ( 2s x.s x )
170 168 169 eqtr4di 
 |-  ( a = ( 2s x.s x ) -> a = ( ( 2s ^su 1s ) x.s x ) )
171 170 oveq1d 
 |-  ( a = ( 2s x.s x ) -> ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) )
172 171 fveq2d 
 |-  ( a = ( 2s x.s x ) -> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) = ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) )
173 172 sseq1d 
 |-  ( a = ( 2s x.s x ) -> ( ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
174 167 173 imbi12d 
 |-  ( a = ( 2s x.s x ) -> ( ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) <-> ( ( 2s x.s x )  ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
175 166 174 syl5ibrcom 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( a = ( 2s x.s x ) -> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
176 175 rexlimdva 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( E. x e. NN0_s a = ( 2s x.s x ) -> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
177 n0zs 
 |-  ( x e. NN0_s -> x e. ZZ_s )
178 177 adantl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> x e. ZZ_s )
179 178 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  x e. ZZ_s )
180 179 znod 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  x e. No )
181 138 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( n +s 1s ) e. NN0_s )
182 180 181 pw2divscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( x /su ( 2s ^su ( n +s 1s ) ) ) e. No )
183 1zs 
 |-  1s e. ZZ_s
184 183 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  1s e. ZZ_s )
185 179 184 zaddscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( x +s 1s ) e. ZZ_s )
186 185 znod 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( x +s 1s ) e. No )
187 186 181 pw2divscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No )
188 180 sltp1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  x
189 180 186 181 pw2sltdiv1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( x  ( x /su ( 2s ^su ( n +s 1s ) ) )
190 188 189 mpbid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( x /su ( 2s ^su ( n +s 1s ) ) )
191 182 187 190 ssltsn 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  { ( x /su ( 2s ^su ( n +s 1s ) ) ) } <
192 imaundi 
 |-  ( bday " ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } u. { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) u. ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
193 fnsnfv 
 |-  ( ( bday Fn No /\ ( x /su ( 2s ^su ( n +s 1s ) ) ) e. No ) -> { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) )
194 103 182 193 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) )
195 oveq1 
 |-  ( a = x -> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( x /su ( 2s ^su ( n +s 1s ) ) ) )
196 195 fveq2d 
 |-  ( a = x -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) )
197 196 sseq1d 
 |-  ( a = x -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
198 127 197 imbi12d 
 |-  ( a = x -> ( ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
199 198 rspccv 
 |-  ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
200 199 imp 
 |-  ( ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) /\ x e. NN0_s ) -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
201 200 adantll 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
202 201 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
203 148 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) e. No )
204 203 203 addscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) e. No )
205 154 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> x e. No )
206 205 203 addscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( 2s ^su ( n +s 1s ) ) ) e. No )
207 peano2n0s 
 |-  ( x e. NN0_s -> ( x +s 1s ) e. NN0_s )
208 207 adantl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x +s 1s ) e. NN0_s )
209 208 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s 1s ) e. NN0_s )
210 209 n0snod 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s 1s ) e. No )
211 205 210 addscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( x +s 1s ) ) e. No )
212 simprr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) <_s x )
213 203 205 203 sleadd1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( 2s ^su ( n +s 1s ) ) ) ) )
214 212 213 mpbid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( 2s ^su ( n +s 1s ) ) ) )
215 205 sltp1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> x
216 203 205 210 212 215 slelttrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) )
217 203 210 216 sltled 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) <_s ( x +s 1s ) )
218 203 210 205 sleadd2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) <_s ( x +s 1s ) <-> ( x +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) )
219 217 218 mpbid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) )
220 204 206 211 214 219 sletrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) )
221 138 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( n +s 1s ) e. NN0_s )
222 7 221 145 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) )
223 7 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> 2s e. No )
224 203 223 mulscomd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) )
225 no2times 
 |-  ( ( 2s ^su ( n +s 1s ) ) e. No -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) )
226 203 225 syl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) )
227 222 224 226 3eqtrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) )
228 no2times 
 |-  ( x e. No -> ( 2s x.s x ) = ( x +s x ) )
229 205 228 syl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s x.s x ) = ( x +s x ) )
230 229 oveq1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s x.s x ) +s 1s ) = ( ( x +s x ) +s 1s ) )
231 2 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> 1s e. No )
232 205 205 231 addsassd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( x +s x ) +s 1s ) = ( x +s ( x +s 1s ) ) )
233 230 232 eqtrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s x.s x ) +s 1s ) = ( x +s ( x +s 1s ) ) )
234 220 227 233 3brtr4d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) )
235 234 expr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) ) )
236 slenlt 
 |-  ( ( ( 2s ^su ( n +s 1s ) ) e. No /\ x e. No ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> -. x
237 148 154 236 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> -. x
238 peano2n0s 
 |-  ( ( n +s 1s ) e. NN0_s -> ( ( n +s 1s ) +s 1s ) e. NN0_s )
239 138 238 syl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( n +s 1s ) +s 1s ) e. NN0_s )
240 expscl 
 |-  ( ( 2s e. No /\ ( ( n +s 1s ) +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No )
241 7 239 240 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No )
242 nnn0s 
 |-  ( 2s e. NN_s -> 2s e. NN0_s )
243 155 242 ax-mp 
 |-  2s e. NN0_s
244 n0mulscl 
 |-  ( ( 2s e. NN0_s /\ x e. NN0_s ) -> ( 2s x.s x ) e. NN0_s )
245 243 244 mpan 
 |-  ( x e. NN0_s -> ( 2s x.s x ) e. NN0_s )
246 245 adantl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s x ) e. NN0_s )
247 n0addscl 
 |-  ( ( ( 2s x.s x ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. NN0_s )
248 246 53 247 sylancl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. NN0_s )
249 248 n0snod 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. No )
250 slenlt 
 |-  ( ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No /\ ( ( 2s x.s x ) +s 1s ) e. No ) -> ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) <-> -. ( ( 2s x.s x ) +s 1s )
251 241 249 250 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) <-> -. ( ( 2s x.s x ) +s 1s )
252 235 237 251 3imtr3d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( -. x  -. ( ( 2s x.s x ) +s 1s )
253 252 con4d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  x
254 253 impr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  x
255 id 
 |-  ( ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
256 202 254 255 sylc 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) )
257 bdayelon 
 |-  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. On
258 bdayelon 
 |-  ( bday ` ( n +s 1s ) ) e. On
259 258 onsuci 
 |-  suc ( bday ` ( n +s 1s ) ) e. On
260 onsssuc 
 |-  ( ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) )
261 257 259 260 mp2an 
 |-  ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) )
262 256 261 sylib 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) )
263 262 snssd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } C_ suc suc ( bday ` ( n +s 1s ) ) )
264 194 263 eqsstrrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
265 151 breq2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( ( 2s x.s x ) +s 1s )
266 n0expscl 
 |-  ( ( 2s e. NN0_s /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. NN0_s )
267 243 138 266 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. NN0_s )
268 n0mulscl 
 |-  ( ( 2s e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) e. NN0_s ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s )
269 243 267 268 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s )
270 n0sltp1le 
 |-  ( ( ( ( 2s x.s x ) +s 1s ) e. NN0_s /\ ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) )
271 248 269 270 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) )
272 149 154 mulscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s x ) e. No )
273 2 a1i 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 1s e. No )
274 272 273 273 addsassd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( ( 2s x.s x ) +s ( 1s +s 1s ) ) )
275 mulsrid 
 |-  ( 2s e. No -> ( 2s x.s 1s ) = 2s )
276 7 275 ax-mp 
 |-  ( 2s x.s 1s ) = 2s
277 276 eqcomi 
 |-  2s = ( 2s x.s 1s )
278 56 277 eqtri 
 |-  ( 1s +s 1s ) = ( 2s x.s 1s )
279 278 oveq2i 
 |-  ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) )
280 149 154 273 addsdid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s ( x +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) )
281 280 eqcomd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) = ( 2s x.s ( x +s 1s ) ) )
282 279 281 eqtrid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( 2s x.s ( x +s 1s ) ) )
283 274 282 eqtrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s ( x +s 1s ) ) )
284 283 breq1d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) )
285 208 n0snod 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x +s 1s ) e. No )
286 285 148 149 158 slemul2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) )
287 286 bicomd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) )
288 284 287 bitrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) )
289 271 288 bitrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) )
290 265 289 bitrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) )
291 sleloe 
 |-  ( ( ( x +s 1s ) e. No /\ ( 2s ^su ( n +s 1s ) ) e. No ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( ( x +s 1s )
292 285 148 291 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( ( x +s 1s )
293 285 138 pw2divscld 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No )
294 293 adantrr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s )  ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No )
295 fnsnfv 
 |-  ( ( bday Fn No /\ ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) -> { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
296 103 294 295 sylancr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s )  { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
297 breq1 
 |-  ( a = ( x +s 1s ) -> ( a  ( x +s 1s )
298 fvoveq1 
 |-  ( a = ( x +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
299 298 sseq1d 
 |-  ( a = ( x +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) )
300 297 299 imbi12d 
 |-  ( a = ( x +s 1s ) -> ( ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( ( x +s 1s )  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
301 300 rspccv 
 |-  ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( ( x +s 1s ) e. NN0_s -> ( ( x +s 1s )  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
302 207 301 syl5 
 |-  ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( ( x +s 1s )  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
303 302 adantl 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( x e. NN0_s -> ( ( x +s 1s )  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) )
304 303 imp32 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s )  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) )
305 bdayelon 
 |-  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. On
306 onsssuc 
 |-  ( ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) )
307 305 259 306 mp2an 
 |-  ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) )
308 304 307 sylib 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s )  ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) )
309 308 snssd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s )  { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } C_ suc suc ( bday ` ( n +s 1s ) ) )
310 296 309 eqsstrrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s )  ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
311 310 expr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s )  ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) )
312 138 pw2divsidd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = 1s )
313 312 sneqd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } = { 1s } )
314 313 imaeq2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( bday " { 1s } ) )
315 df-1o 
 |-  1o = suc (/)
316 15 315 eqtri 
 |-  ( bday ` 1s ) = suc (/)
317 0ss 
 |-  (/) C_ ( bday ` ( n +s 1s ) )
318 ord0 
 |-  Ord (/)
319 258 onordi 
 |-  Ord ( bday ` ( n +s 1s ) )
320 ordsucsssuc 
 |-  ( ( Ord (/) /\ Ord ( bday ` ( n +s 1s ) ) ) -> ( (/) C_ ( bday ` ( n +s 1s ) ) <-> suc (/) C_ suc ( bday ` ( n +s 1s ) ) ) )
321 318 319 320 mp2an 
 |-  ( (/) C_ ( bday ` ( n +s 1s ) ) <-> suc (/) C_ suc ( bday ` ( n +s 1s ) ) )
322 317 321 mpbi 
 |-  suc (/) C_ suc ( bday ` ( n +s 1s ) )
323 316 322 eqsstri 
 |-  ( bday ` 1s ) C_ suc ( bday ` ( n +s 1s ) )
324 bdayelon 
 |-  ( bday ` 1s ) e. On
325 onsssuc 
 |-  ( ( ( bday ` 1s ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` 1s ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` 1s ) e. suc suc ( bday ` ( n +s 1s ) ) ) )
326 324 259 325 mp2an 
 |-  ( ( bday ` 1s ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` 1s ) e. suc suc ( bday ` ( n +s 1s ) ) )
327 323 326 mpbi 
 |-  ( bday ` 1s ) e. suc suc ( bday ` ( n +s 1s ) )
328 327 a1i 
 |-  ( n e. NN0_s -> ( bday ` 1s ) e. suc suc ( bday ` ( n +s 1s ) ) )
329 328 snssd 
 |-  ( n e. NN0_s -> { ( bday ` 1s ) } C_ suc suc ( bday ` ( n +s 1s ) ) )
330 109 329 eqsstrrid 
 |-  ( n e. NN0_s -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
331 330 adantr 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
332 331 adantr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
333 314 332 eqsstrd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
334 oveq1 
 |-  ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
335 334 sneqd 
 |-  ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } = { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } )
336 335 imaeq2d 
 |-  ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
337 336 sseq1d 
 |-  ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) <-> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) )
338 333 337 syl5ibrcom 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) )
339 311 338 jaod 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( x +s 1s )  ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) )
340 292 339 sylbid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) )
341 290 340 sylbid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) )
342 341 impr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) )
343 264 342 unssd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) u. ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) )
344 192 343 eqsstrid 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday " ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } u. { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) )
345 259 onsuci 
 |-  suc suc ( bday ` ( n +s 1s ) ) e. On
346 scutbdaybnd 
 |-  ( ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) )
347 345 346 mp3an2 
 |-  ( ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) )
348 191 344 347 syl2anc 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) )
349 179 181 pw2cutp1 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) )
350 349 fveq2d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) )
351 181 140 syl 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) )
352 351 suceqd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  suc ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc suc ( bday ` ( n +s 1s ) ) )
353 352 eqcomd 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  suc suc ( bday ` ( n +s 1s ) ) = suc ( bday ` ( ( n +s 1s ) +s 1s ) ) )
354 348 350 353 3sstr3d 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s )  ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) )
355 354 expr 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s )  ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
356 breq1 
 |-  ( a = ( ( 2s x.s x ) +s 1s ) -> ( a  ( ( 2s x.s x ) +s 1s )
357 oveq1 
 |-  ( a = ( ( 2s x.s x ) +s 1s ) -> ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) )
358 357 fveq2d 
 |-  ( a = ( ( 2s x.s x ) +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) = ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) )
359 358 sseq1d 
 |-  ( a = ( ( 2s x.s x ) +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
360 356 359 imbi12d 
 |-  ( a = ( ( 2s x.s x ) +s 1s ) -> ( ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) <-> ( ( ( 2s x.s x ) +s 1s )  ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
361 355 360 syl5ibrcom 
 |-  ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( a = ( ( 2s x.s x ) +s 1s ) -> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
362 361 rexlimdva 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) -> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
363 176 362 jaod 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( ( E. x e. NN0_s a = ( 2s x.s x ) \/ E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) ) -> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
364 126 363 syl5 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( a e. NN0_s -> ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
365 125 364 ralrimi 
 |-  ( ( n e. NN0_s /\ A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) )
366 365 ex 
 |-  ( n e. NN0_s -> ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) )
367 22 32 42 52 122 366 n0sind 
 |-  ( N e. NN0_s -> A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) )
368 breq1 
 |-  ( a = A -> ( a  A
369 oveq1 
 |-  ( a = A -> ( a /su ( 2s ^su ( N +s 1s ) ) ) = ( A /su ( 2s ^su ( N +s 1s ) ) ) )
370 369 fveq2d 
 |-  ( a = A -> ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) = ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) )
371 370 sseq1d 
 |-  ( a = A -> ( ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) <-> ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) )
372 368 371 imbi12d 
 |-  ( a = A -> ( ( a  ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) <-> ( A  ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) )
373 372 rspccv 
 |-  ( A. a e. NN0_s ( a  ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) -> ( A e. NN0_s -> ( A  ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) )
374 367 373 syl 
 |-  ( N e. NN0_s -> ( A e. NN0_s -> ( A  ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) )
375 374 com12 
 |-  ( A e. NN0_s -> ( N e. NN0_s -> ( A  ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) )
376 375 3imp 
 |-  ( ( A e. NN0_s /\ N e. NN0_s /\ A  ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) )