Metamath Proof Explorer


Theorem bdaypw2n0sbnd

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

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

Proof

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 ) )