Metamath Proof Explorer

Theorem bdayfinlem

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

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

Proof

Step Hyp Ref Expression
1 bdayn0sf1o 
 |-  ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om
2 f1ocnvdm 
 |-  ( ( ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om /\ ( bday ` A ) e. _om ) -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. NN0_s )
3 1 2 mpan 
 |-  ( ( bday ` A ) e. _om -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. NN0_s )
4 3 3ad2ant3 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. NN0_s )
5 4 n0zsd 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s )
6 zzs12 
 |-  ( ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] )
7 5 6 syl 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] )
8 eleq1 
 |-  ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) -> ( A e. ZZ_s[1/2] <-> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) )
9 7 8 syl5ibrcom 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) -> A e. ZZ_s[1/2] ) )
10 n0zs 
 |-  ( x e. NN0_s -> x e. ZZ_s )
11 zzs12 
 |-  ( x e. ZZ_s -> x e. ZZ_s[1/2] )
12 10 11 syl 
 |-  ( x e. NN0_s -> x e. ZZ_s[1/2] )
13 12 adantr 
 |-  ( ( x e. NN0_s /\ y e. NN0_s ) -> x e. ZZ_s[1/2] )
14 n0zs 
 |-  ( y e. NN0_s -> y e. ZZ_s )
15 elzs12i 
 |-  ( ( y e. ZZ_s /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] )
16 14 15 sylan 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] )
17 16 adantll 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] )
18 zs12addscl 
 |-  ( ( x e. ZZ_s[1/2] /\ ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) -> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] )
19 13 17 18 syl2an2r 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] )
20 eleq1 
 |-  ( A = ( x +s ( y /su ( 2s ^su z ) ) ) -> ( A e. ZZ_s[1/2] <-> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) )
21 20 3ad2ant1 
 |-  ( ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y  ( A e. ZZ_s[1/2] <-> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) )
22 19 21 syl5ibrcom 
 |-  ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y  A e. ZZ_s[1/2] ) )
23 22 rexlimdva 
 |-  ( ( x e. NN0_s /\ y e. NN0_s ) -> ( E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y  A e. ZZ_s[1/2] ) )
24 23 rexlimivv 
 |-  ( E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y  A e. ZZ_s[1/2] )
25 24 a1i 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y  A e. ZZ_s[1/2] ) )
26 simp1 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> A e. No )
27 4 fvresd 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( ( bday |` NN0_s ) ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) = ( bday ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) )
28 f1ocnvfv2 
 |-  ( ( ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om /\ ( bday ` A ) e. _om ) -> ( ( bday |` NN0_s ) ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) = ( bday ` A ) )
29 1 28 mpan 
 |-  ( ( bday ` A ) e. _om -> ( ( bday |` NN0_s ) ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) = ( bday ` A ) )
30 29 3ad2ant3 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( ( bday |` NN0_s ) ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) = ( bday ` A ) )
31 27 30 eqtr3d 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( bday ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) = ( bday ` A ) )
32 31 eqimsscd 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( bday ` A ) C_ ( bday ` ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) ) )
33 simp2 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> 0s <_s A )
34 4 26 32 33 bdayfinbnd 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) \/ E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y
35 9 25 34 mpjaod 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] )