| Step |
Hyp |
Ref |
Expression |
| 1 |
|
n0s0suc |
|- ( N e. NN0_s -> ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) ) |
| 2 |
|
n0slt1e0 |
|- ( A e. NN0_s -> ( A A = 0s ) ) |
| 3 |
|
oveq1 |
|- ( A = 0s -> ( A /su 1s ) = ( 0s /su 1s ) ) |
| 4 |
|
0sno |
|- 0s e. No |
| 5 |
|
divs1 |
|- ( 0s e. No -> ( 0s /su 1s ) = 0s ) |
| 6 |
4 5
|
ax-mp |
|- ( 0s /su 1s ) = 0s |
| 7 |
3 6
|
eqtrdi |
|- ( A = 0s -> ( A /su 1s ) = 0s ) |
| 8 |
7
|
fveq2d |
|- ( A = 0s -> ( bday ` ( A /su 1s ) ) = ( bday ` 0s ) ) |
| 9 |
|
bday0s |
|- ( bday ` 0s ) = (/) |
| 10 |
8 9
|
eqtrdi |
|- ( A = 0s -> ( bday ` ( A /su 1s ) ) = (/) ) |
| 11 |
|
0ss |
|- (/) C_ suc (/) |
| 12 |
10 11
|
eqsstrdi |
|- ( A = 0s -> ( bday ` ( A /su 1s ) ) C_ suc (/) ) |
| 13 |
2 12
|
biimtrdi |
|- ( A e. NN0_s -> ( A ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) |
| 14 |
|
oveq2 |
|- ( N = 0s -> ( 2s ^su N ) = ( 2s ^su 0s ) ) |
| 15 |
|
2sno |
|- 2s e. No |
| 16 |
|
exps0 |
|- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) |
| 17 |
15 16
|
ax-mp |
|- ( 2s ^su 0s ) = 1s |
| 18 |
14 17
|
eqtrdi |
|- ( N = 0s -> ( 2s ^su N ) = 1s ) |
| 19 |
18
|
breq2d |
|- ( N = 0s -> ( A A |
| 20 |
18
|
oveq2d |
|- ( N = 0s -> ( A /su ( 2s ^su N ) ) = ( A /su 1s ) ) |
| 21 |
20
|
fveq2d |
|- ( N = 0s -> ( bday ` ( A /su ( 2s ^su N ) ) ) = ( bday ` ( A /su 1s ) ) ) |
| 22 |
|
fveq2 |
|- ( N = 0s -> ( bday ` N ) = ( bday ` 0s ) ) |
| 23 |
22 9
|
eqtrdi |
|- ( N = 0s -> ( bday ` N ) = (/) ) |
| 24 |
23
|
suceqd |
|- ( N = 0s -> suc ( bday ` N ) = suc (/) ) |
| 25 |
21 24
|
sseq12d |
|- ( N = 0s -> ( ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) <-> ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) |
| 26 |
19 25
|
imbi12d |
|- ( N = 0s -> ( ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) <-> ( A ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) ) |
| 27 |
13 26
|
imbitrrid |
|- ( N = 0s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) |
| 28 |
|
bdaypw2n0sbndlem |
|- ( ( A e. NN0_s /\ x e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) |
| 29 |
28
|
3exp |
|- ( A e. NN0_s -> ( x e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) |
| 30 |
29
|
com12 |
|- ( x e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) |
| 31 |
|
oveq2 |
|- ( N = ( x +s 1s ) -> ( 2s ^su N ) = ( 2s ^su ( x +s 1s ) ) ) |
| 32 |
31
|
breq2d |
|- ( N = ( x +s 1s ) -> ( A A |
| 33 |
31
|
oveq2d |
|- ( N = ( x +s 1s ) -> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su ( x +s 1s ) ) ) ) |
| 34 |
33
|
fveq2d |
|- ( N = ( x +s 1s ) -> ( bday ` ( A /su ( 2s ^su N ) ) ) = ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) ) |
| 35 |
|
fveq2 |
|- ( N = ( x +s 1s ) -> ( bday ` N ) = ( bday ` ( x +s 1s ) ) ) |
| 36 |
35
|
suceqd |
|- ( N = ( x +s 1s ) -> suc ( bday ` N ) = suc ( bday ` ( x +s 1s ) ) ) |
| 37 |
34 36
|
sseq12d |
|- ( N = ( x +s 1s ) -> ( ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) <-> ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) |
| 38 |
32 37
|
imbi12d |
|- ( N = ( x +s 1s ) -> ( ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) <-> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) |
| 39 |
38
|
imbi2d |
|- ( N = ( x +s 1s ) -> ( ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) <-> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) ) |
| 40 |
30 39
|
syl5ibrcom |
|- ( x e. NN0_s -> ( N = ( x +s 1s ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) ) |
| 41 |
40
|
rexlimiv |
|- ( E. x e. NN0_s N = ( x +s 1s ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) |
| 42 |
27 41
|
jaoi |
|- ( ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) |
| 43 |
1 42
|
syl |
|- ( N e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) |
| 44 |
43
|
3imp21 |
|- ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) |