Metamath Proof Explorer

Theorem bdaypw2bnd

Description: Birthday bounding rule for non-negative dyadic rationals. (Contributed by Scott Fenton, 25-Feb-2026)

Ref Expression
Hypotheses bdaypw2bnd.1 
|- ( ph -> N e. NN0_s )
bdaypw2bnd.2 
|- ( ph -> X e. NN0_s )
bdaypw2bnd.3 
|- ( ph -> Y e. NN0_s )
bdaypw2bnd.4 
|- ( ph -> P e. NN0_s )
bdaypw2bnd.5 
|- ( ph -> Y
bdaypw2bnd.6 
|- ( ph -> ( X +s P )
Assertion bdaypw2bnd 
|- ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) )

Proof

Step Hyp Ref Expression
1 bdaypw2bnd.1 
 |-  ( ph -> N e. NN0_s )
2 bdaypw2bnd.2 
 |-  ( ph -> X e. NN0_s )
3 bdaypw2bnd.3 
 |-  ( ph -> Y e. NN0_s )
4 bdaypw2bnd.4 
 |-  ( ph -> P e. NN0_s )
5 bdaypw2bnd.5 
 |-  ( ph -> Y
6 bdaypw2bnd.6 
 |-  ( ph -> ( X +s P )
7 2 n0snod 
 |-  ( ph -> X e. No )
8 3 n0snod 
 |-  ( ph -> Y e. No )
9 8 4 pw2divscld 
 |-  ( ph -> ( Y /su ( 2s ^su P ) ) e. No )
10 addsbday 
 |-  ( ( X e. No /\ ( Y /su ( 2s ^su P ) ) e. No ) -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) )
11 7 9 10 syl2anc 
 |-  ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) )
12 bdaypw2n0sbnd 
 |-  ( ( Y e. NN0_s /\ P e. NN0_s /\ Y  ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) )
13 3 4 5 12 syl3anc 
 |-  ( ph -> ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) )
14 bdayelon 
 |-  ( bday ` ( Y /su ( 2s ^su P ) ) ) e. On
15 bdayelon 
 |-  ( bday ` P ) e. On
16 15 onsuci 
 |-  suc ( bday ` P ) e. On
17 bdayelon 
 |-  ( bday ` X ) e. On
18 naddss2 
 |-  ( ( ( bday ` ( Y /su ( 2s ^su P ) ) ) e. On /\ suc ( bday ` P ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) )
19 14 16 17 18 mp3an 
 |-  ( ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) )
20 13 19 sylib 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) )
21 bdayn0p1 
 |-  ( P e. NN0_s -> ( bday ` ( P +s 1s ) ) = suc ( bday ` P ) )
22 4 21 syl 
 |-  ( ph -> ( bday ` ( P +s 1s ) ) = suc ( bday ` P ) )
23 22 oveq2d 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` ( P +s 1s ) ) ) = ( ( bday ` X ) +no suc ( bday ` P ) ) )
24 n0ons 
 |-  ( X e. NN0_s -> X e. On_s )
25 2 24 syl 
 |-  ( ph -> X e. On_s )
26 peano2n0s 
 |-  ( P e. NN0_s -> ( P +s 1s ) e. NN0_s )
27 4 26 syl 
 |-  ( ph -> ( P +s 1s ) e. NN0_s )
28 n0ons 
 |-  ( ( P +s 1s ) e. NN0_s -> ( P +s 1s ) e. On_s )
29 27 28 syl 
 |-  ( ph -> ( P +s 1s ) e. On_s )
30 addsonbday 
 |-  ( ( X e. On_s /\ ( P +s 1s ) e. On_s ) -> ( bday ` ( X +s ( P +s 1s ) ) ) = ( ( bday ` X ) +no ( bday ` ( P +s 1s ) ) ) )
31 25 29 30 syl2anc 
 |-  ( ph -> ( bday ` ( X +s ( P +s 1s ) ) ) = ( ( bday ` X ) +no ( bday ` ( P +s 1s ) ) ) )
32 n0ons 
 |-  ( N e. NN0_s -> N e. On_s )
33 1 32 syl 
 |-  ( ph -> N e. On_s )
34 n0addscl 
 |-  ( ( X e. NN0_s /\ ( P +s 1s ) e. NN0_s ) -> ( X +s ( P +s 1s ) ) e. NN0_s )
35 2 27 34 syl2anc 
 |-  ( ph -> ( X +s ( P +s 1s ) ) e. NN0_s )
36 n0ons 
 |-  ( ( X +s ( P +s 1s ) ) e. NN0_s -> ( X +s ( P +s 1s ) ) e. On_s )
37 35 36 syl 
 |-  ( ph -> ( X +s ( P +s 1s ) ) e. On_s )
38 onslt 
 |-  ( ( N e. On_s /\ ( X +s ( P +s 1s ) ) e. On_s ) -> ( N  ( bday ` N ) e. ( bday ` ( X +s ( P +s 1s ) ) ) ) )
39 33 37 38 syl2anc 
 |-  ( ph -> ( N  ( bday ` N ) e. ( bday ` ( X +s ( P +s 1s ) ) ) ) )
40 39 notbid 
 |-  ( ph -> ( -. N  -. ( bday ` N ) e. ( bday ` ( X +s ( P +s 1s ) ) ) ) )
41 n0addscl 
 |-  ( ( X e. NN0_s /\ P e. NN0_s ) -> ( X +s P ) e. NN0_s )
42 2 4 41 syl2anc 
 |-  ( ph -> ( X +s P ) e. NN0_s )
43 n0sltp1le 
 |-  ( ( ( X +s P ) e. NN0_s /\ N e. NN0_s ) -> ( ( X +s P )  ( ( X +s P ) +s 1s ) <_s N ) )
44 42 1 43 syl2anc 
 |-  ( ph -> ( ( X +s P )  ( ( X +s P ) +s 1s ) <_s N ) )
45 4 n0snod 
 |-  ( ph -> P e. No )
46 1sno 
 |-  1s e. No
47 46 a1i 
 |-  ( ph -> 1s e. No )
48 7 45 47 addsassd 
 |-  ( ph -> ( ( X +s P ) +s 1s ) = ( X +s ( P +s 1s ) ) )
49 48 breq1d 
 |-  ( ph -> ( ( ( X +s P ) +s 1s ) <_s N <-> ( X +s ( P +s 1s ) ) <_s N ) )
50 35 n0snod 
 |-  ( ph -> ( X +s ( P +s 1s ) ) e. No )
51 1 n0snod 
 |-  ( ph -> N e. No )
52 slenlt 
 |-  ( ( ( X +s ( P +s 1s ) ) e. No /\ N e. No ) -> ( ( X +s ( P +s 1s ) ) <_s N <-> -. N
53 50 51 52 syl2anc 
 |-  ( ph -> ( ( X +s ( P +s 1s ) ) <_s N <-> -. N
54 44 49 53 3bitrd 
 |-  ( ph -> ( ( X +s P )  -. N
55 bdayelon 
 |-  ( bday ` ( X +s ( P +s 1s ) ) ) e. On
56 bdayelon 
 |-  ( bday ` N ) e. On
57 ontri1 
 |-  ( ( ( bday ` ( X +s ( P +s 1s ) ) ) e. On /\ ( bday ` N ) e. On ) -> ( ( bday ` ( X +s ( P +s 1s ) ) ) C_ ( bday ` N ) <-> -. ( bday ` N ) e. ( bday ` ( X +s ( P +s 1s ) ) ) ) )
58 55 56 57 mp2an 
 |-  ( ( bday ` ( X +s ( P +s 1s ) ) ) C_ ( bday ` N ) <-> -. ( bday ` N ) e. ( bday ` ( X +s ( P +s 1s ) ) ) )
59 58 a1i 
 |-  ( ph -> ( ( bday ` ( X +s ( P +s 1s ) ) ) C_ ( bday ` N ) <-> -. ( bday ` N ) e. ( bday ` ( X +s ( P +s 1s ) ) ) ) )
60 40 54 59 3bitr4d 
 |-  ( ph -> ( ( X +s P )  ( bday ` ( X +s ( P +s 1s ) ) ) C_ ( bday ` N ) ) )
61 6 60 mpbid 
 |-  ( ph -> ( bday ` ( X +s ( P +s 1s ) ) ) C_ ( bday ` N ) )
62 31 61 eqsstrrd 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` ( P +s 1s ) ) ) C_ ( bday ` N ) )
63 23 62 eqsstrrd 
 |-  ( ph -> ( ( bday ` X ) +no suc ( bday ` P ) ) C_ ( bday ` N ) )
64 20 63 sstrd 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) )
65 11 64 sstrd 
 |-  ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) )