Metamath Proof Explorer

Theorem zs12bdaylem2

Description: Lemma for zs12bday . Show the first half of the equality. (Contributed by Scott Fenton, 22-Feb-2026)

Ref Expression
Hypotheses zs12bdaylem.1 
|- ( ph -> N e. NN0_s )
zs12bdaylem.2 
|- ( ph -> M e. NN0_s )
zs12bdaylem.3 
|- ( ph -> P e. NN0_s )
zs12bdaylem.4 
|- ( ph -> ( ( 2s x.s M ) +s 1s )
Assertion zs12bdaylem2 
|- ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) )

Proof

Step Hyp Ref Expression
1 zs12bdaylem.1 
 |-  ( ph -> N e. NN0_s )
2 zs12bdaylem.2 
 |-  ( ph -> M e. NN0_s )
3 zs12bdaylem.3 
 |-  ( ph -> P e. NN0_s )
4 zs12bdaylem.4 
 |-  ( ph -> ( ( 2s x.s M ) +s 1s )
5 1 n0snod 
 |-  ( ph -> N e. No )
6 2sno 
 |-  2s e. No
7 6 a1i 
 |-  ( ph -> 2s e. No )
8 2 n0snod 
 |-  ( ph -> M e. No )
9 7 8 mulscld 
 |-  ( ph -> ( 2s x.s M ) e. No )
10 1sno 
 |-  1s e. No
11 10 a1i 
 |-  ( ph -> 1s e. No )
12 9 11 addscld 
 |-  ( ph -> ( ( 2s x.s M ) +s 1s ) e. No )
13 12 3 pw2divscld 
 |-  ( ph -> ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No )
14 addsbday 
 |-  ( ( N e. No /\ ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No ) -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) )
15 5 13 14 syl2anc 
 |-  ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) )
16 2nns 
 |-  2s e. NN_s
17 nnn0s 
 |-  ( 2s e. NN_s -> 2s e. NN0_s )
18 16 17 ax-mp 
 |-  2s e. NN0_s
19 n0mulscl 
 |-  ( ( 2s e. NN0_s /\ M e. NN0_s ) -> ( 2s x.s M ) e. NN0_s )
20 18 2 19 sylancr 
 |-  ( ph -> ( 2s x.s M ) e. NN0_s )
21 1n0s 
 |-  1s e. NN0_s
22 n0addscl 
 |-  ( ( ( 2s x.s M ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s M ) +s 1s ) e. NN0_s )
23 20 21 22 sylancl 
 |-  ( ph -> ( ( 2s x.s M ) +s 1s ) e. NN0_s )
24 bdaypw2n0sbnd 
 |-  ( ( ( ( 2s x.s M ) +s 1s ) e. NN0_s /\ P e. NN0_s /\ ( ( 2s x.s M ) +s 1s )  ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) )
25 23 3 4 24 syl3anc 
 |-  ( ph -> ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) )
26 bdayelon 
 |-  ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) e. On
27 bdayelon 
 |-  ( bday ` P ) e. On
28 27 onsuci 
 |-  suc ( bday ` P ) e. On
29 bdayelon 
 |-  ( bday ` N ) e. On
30 naddss2 
 |-  ( ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) e. On /\ suc ( bday ` P ) e. On /\ ( bday ` N ) e. On ) -> ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) )
31 26 28 29 30 mp3an 
 |-  ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) )
32 25 31 sylib 
 |-  ( ph -> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) )
33 n0addscl 
 |-  ( ( N e. NN0_s /\ P e. NN0_s ) -> ( N +s P ) e. NN0_s )
34 1 3 33 syl2anc 
 |-  ( ph -> ( N +s P ) e. NN0_s )
35 bdayn0p1 
 |-  ( ( N +s P ) e. NN0_s -> ( bday ` ( ( N +s P ) +s 1s ) ) = suc ( bday ` ( N +s P ) ) )
36 34 35 syl 
 |-  ( ph -> ( bday ` ( ( N +s P ) +s 1s ) ) = suc ( bday ` ( N +s P ) ) )
37 n0ons 
 |-  ( N e. NN0_s -> N e. On_s )
38 1 37 syl 
 |-  ( ph -> N e. On_s )
39 n0ons 
 |-  ( P e. NN0_s -> P e. On_s )
40 3 39 syl 
 |-  ( ph -> P e. On_s )
41 addsonbday 
 |-  ( ( N e. On_s /\ P e. On_s ) -> ( bday ` ( N +s P ) ) = ( ( bday ` N ) +no ( bday ` P ) ) )
42 38 40 41 syl2anc 
 |-  ( ph -> ( bday ` ( N +s P ) ) = ( ( bday ` N ) +no ( bday ` P ) ) )
43 42 suceqd 
 |-  ( ph -> suc ( bday ` ( N +s P ) ) = suc ( ( bday ` N ) +no ( bday ` P ) ) )
44 naddsuc2 
 |-  ( ( ( bday ` N ) e. On /\ ( bday ` P ) e. On ) -> ( ( bday ` N ) +no suc ( bday ` P ) ) = suc ( ( bday ` N ) +no ( bday ` P ) ) )
45 29 27 44 mp2an 
 |-  ( ( bday ` N ) +no suc ( bday ` P ) ) = suc ( ( bday ` N ) +no ( bday ` P ) )
46 43 45 eqtr4di 
 |-  ( ph -> suc ( bday ` ( N +s P ) ) = ( ( bday ` N ) +no suc ( bday ` P ) ) )
47 36 46 eqtrd 
 |-  ( ph -> ( bday ` ( ( N +s P ) +s 1s ) ) = ( ( bday ` N ) +no suc ( bday ` P ) ) )
48 32 47 sseqtrrd 
 |-  ( ph -> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) )
49 15 48 sstrd 
 |-  ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) )