Metamath Proof Explorer

Theorem zs12bdaylem

Description: Lemma for zs12bday . Handle the non-negative case. (Contributed by Scott Fenton, 22-Feb-2026)

Ref Expression
Assertion zs12bdaylem 
|- ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( bday ` A ) e. _om )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> A e. ZZ_s[1/2] )
2 zs12no 
 |-  ( A e. ZZ_s[1/2] -> A e. No )
3 zs12ge0 
 |-  ( ( A e. No /\ 0s <_s A ) -> ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
4 2 3 sylan 
 |-  ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
5 1 4 mpbid 
 |-  ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
6 simpl1 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  x e. NN0_s )
7 6 n0snod 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  x e. No )
8 simpl2 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  y e. NN0_s )
9 8 n0snod 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  y e. No )
10 simpl3 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  p e. NN0_s )
11 9 10 pw2divscld 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( y /su ( 2s ^su p ) ) e. No )
12 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 ) ) ) ) )
13 7 11 12 syl2anc 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) )
14 n0sbday 
 |-  ( x e. NN0_s -> ( bday ` x ) e. _om )
15 6 14 syl 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( bday ` x ) e. _om )
16 simpr 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  y
17 bdaypw2n0sbnd 
 |-  ( ( y e. NN0_s /\ p e. NN0_s /\ y  ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) )
18 8 10 16 17 syl3anc 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) )
19 n0sbday 
 |-  ( p e. NN0_s -> ( bday ` p ) e. _om )
20 peano2 
 |-  ( ( bday ` p ) e. _om -> suc ( bday ` p ) e. _om )
21 19 20 syl 
 |-  ( p e. NN0_s -> suc ( bday ` p ) e. _om )
22 21 3ad2ant3 
 |-  ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> suc ( bday ` p ) e. _om )
23 22 adantr 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  suc ( bday ` p ) e. _om )
24 bdayelon 
 |-  ( bday ` ( y /su ( 2s ^su p ) ) ) e. On
25 24 onordi 
 |-  Ord ( bday ` ( y /su ( 2s ^su p ) ) )
26 ordom 
 |-  Ord _om
27 ordtr2 
 |-  ( ( Ord ( bday ` ( y /su ( 2s ^su p ) ) ) /\ Ord _om ) -> ( ( ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) /\ suc ( bday ` p ) e. _om ) -> ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) )
28 25 26 27 mp2an 
 |-  ( ( ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) /\ suc ( bday ` p ) e. _om ) -> ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om )
29 18 23 28 syl2anc 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om )
30 omnaddcl 
 |-  ( ( ( bday ` x ) e. _om /\ ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) -> ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om )
31 15 29 30 syl2anc 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om )
32 bdayelon 
 |-  ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. On
33 32 onordi 
 |-  Ord ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) )
34 ordtr2 
 |-  ( ( Ord ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) /\ Ord _om ) -> ( ( ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) /\ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) )
35 33 26 34 mp2an 
 |-  ( ( ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) /\ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om )
36 13 31 35 syl2anc 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om )
37 fveq2 
 |-  ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) = ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) )
38 37 eleq1d 
 |-  ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( ( bday ` A ) e. _om <-> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) )
39 36 38 syl5ibrcom 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y  ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) e. _om ) )
40 39 ex 
 |-  ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> ( y  ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) e. _om ) ) )
41 40 impcomd 
 |-  ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( bday ` A ) e. _om ) )
42 41 3expa 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ p e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( bday ` A ) e. _om ) )
43 42 rexlimdva 
 |-  ( ( x e. NN0_s /\ y e. NN0_s ) -> ( E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( bday ` A ) e. _om ) )
44 43 rexlimivv 
 |-  ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( bday ` A ) e. _om )
45 5 44 syl 
 |-  ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( bday ` A ) e. _om )