Metamath Proof Explorer

Theorem bdayfinbndlem2

Description: Lemma for bdayfinbnd . Conduct the induction. (Contributed by Scott Fenton, 26-Feb-2026)

Ref Expression
Assertion bdayfinbndlem2 
|- ( N e. NN0_s -> A. z e. No ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( m = 0s -> ( bday ` m ) = ( bday ` 0s ) )
2 bday0s 
 |-  ( bday ` 0s ) = (/)
3 1 2 eqtrdi 
 |-  ( m = 0s -> ( bday ` m ) = (/) )
4 3 sseq2d 
 |-  ( m = 0s -> ( ( bday ` z ) C_ ( bday ` m ) <-> ( bday ` z ) C_ (/) ) )
5 ss0b 
 |-  ( ( bday ` z ) C_ (/) <-> ( bday ` z ) = (/) )
6 4 5 bitrdi 
 |-  ( m = 0s -> ( ( bday ` z ) C_ ( bday ` m ) <-> ( bday ` z ) = (/) ) )
7 6 anbi1d 
 |-  ( m = 0s -> ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) <-> ( ( bday ` z ) = (/) /\ 0s <_s z ) ) )
8 eqeq2 
 |-  ( m = 0s -> ( z = m <-> z = 0s ) )
9 breq2 
 |-  ( m = 0s -> ( ( x +s p )  ( x +s p )
10 9 3anbi3d 
 |-  ( m = 0s -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
11 10 rexbidv 
 |-  ( m = 0s -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
12 11 2rexbidv 
 |-  ( m = 0s -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
13 8 12 orbi12d 
 |-  ( m = 0s -> ( ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
14 7 13 imbi12d 
 |-  ( m = 0s -> ( ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( ( ( bday ` z ) = (/) /\ 0s <_s z ) -> ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
15 14 ralbidv 
 |-  ( m = 0s -> ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. z e. No ( ( ( bday ` z ) = (/) /\ 0s <_s z ) -> ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
16 fveq2 
 |-  ( m = n -> ( bday ` m ) = ( bday ` n ) )
17 16 sseq2d 
 |-  ( m = n -> ( ( bday ` z ) C_ ( bday ` m ) <-> ( bday ` z ) C_ ( bday ` n ) ) )
18 17 anbi1d 
 |-  ( m = n -> ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) <-> ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) ) )
19 eqeq2 
 |-  ( m = n -> ( z = m <-> z = n ) )
20 breq2 
 |-  ( m = n -> ( ( x +s p )  ( x +s p )
21 20 3anbi3d 
 |-  ( m = n -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
22 21 rexbidv 
 |-  ( m = n -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
23 22 2rexbidv 
 |-  ( m = n -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
24 19 23 orbi12d 
 |-  ( m = n -> ( ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
25 18 24 imbi12d 
 |-  ( m = n -> ( ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
26 25 ralbidv 
 |-  ( m = n -> ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
27 fveq2 
 |-  ( m = ( n +s 1s ) -> ( bday ` m ) = ( bday ` ( n +s 1s ) ) )
28 27 sseq2d 
 |-  ( m = ( n +s 1s ) -> ( ( bday ` z ) C_ ( bday ` m ) <-> ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) ) )
29 28 anbi1d 
 |-  ( m = ( n +s 1s ) -> ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) <-> ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s z ) ) )
30 eqeq2 
 |-  ( m = ( n +s 1s ) -> ( z = m <-> z = ( n +s 1s ) ) )
31 breq2 
 |-  ( m = ( n +s 1s ) -> ( ( x +s p )  ( x +s p )
32 31 3anbi3d 
 |-  ( m = ( n +s 1s ) -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
33 32 rexbidv 
 |-  ( m = ( n +s 1s ) -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
34 33 2rexbidv 
 |-  ( m = ( n +s 1s ) -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
35 30 34 orbi12d 
 |-  ( m = ( n +s 1s ) -> ( ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = ( n +s 1s ) \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
36 29 35 imbi12d 
 |-  ( m = ( n +s 1s ) -> ( ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s z ) -> ( z = ( n +s 1s ) \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
37 36 ralbidv 
 |-  ( m = ( n +s 1s ) -> ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. z e. No ( ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s z ) -> ( z = ( n +s 1s ) \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
38 fveq2 
 |-  ( z = w -> ( bday ` z ) = ( bday ` w ) )
39 38 sseq1d 
 |-  ( z = w -> ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) <-> ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) ) )
40 breq2 
 |-  ( z = w -> ( 0s <_s z <-> 0s <_s w ) )
41 39 40 anbi12d 
 |-  ( z = w -> ( ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s z ) <-> ( ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s w ) ) )
42 eqeq1 
 |-  ( z = w -> ( z = ( n +s 1s ) <-> w = ( n +s 1s ) ) )
43 eqeq1 
 |-  ( z = w -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( x +s ( y /su ( 2s ^su p ) ) ) ) )
44 43 3anbi1d 
 |-  ( z = w -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
45 44 rexbidv 
 |-  ( z = w -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
46 45 2rexbidv 
 |-  ( z = w -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
47 oveq1 
 |-  ( x = a -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( y /su ( 2s ^su p ) ) ) )
48 47 eqeq2d 
 |-  ( x = a -> ( w = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( y /su ( 2s ^su p ) ) ) ) )
49 oveq1 
 |-  ( x = a -> ( x +s p ) = ( a +s p ) )
50 49 breq1d 
 |-  ( x = a -> ( ( x +s p )  ( a +s p )
51 48 50 3anbi13d 
 |-  ( x = a -> ( ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y
52 51 rexbidv 
 |-  ( x = a -> ( E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y
53 oveq1 
 |-  ( y = b -> ( y /su ( 2s ^su p ) ) = ( b /su ( 2s ^su p ) ) )
54 53 oveq2d 
 |-  ( y = b -> ( a +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su p ) ) ) )
55 54 eqeq2d 
 |-  ( y = b -> ( w = ( a +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su p ) ) ) ) )
56 breq1 
 |-  ( y = b -> ( y  b
57 55 56 3anbi12d 
 |-  ( y = b -> ( ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b
58 57 rexbidv 
 |-  ( y = b -> ( E. p e. NN0_s ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b
59 oveq2 
 |-  ( p = q -> ( 2s ^su p ) = ( 2s ^su q ) )
60 59 oveq2d 
 |-  ( p = q -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) )
61 60 oveq2d 
 |-  ( p = q -> ( a +s ( b /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su q ) ) ) )
62 61 eqeq2d 
 |-  ( p = q -> ( w = ( a +s ( b /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su q ) ) ) ) )
63 59 breq2d 
 |-  ( p = q -> ( b  b
64 oveq2 
 |-  ( p = q -> ( a +s p ) = ( a +s q ) )
65 64 breq1d 
 |-  ( p = q -> ( ( a +s p )  ( a +s q )
66 62 63 65 3anbi123d 
 |-  ( p = q -> ( ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b  ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
67 66 cbvrexvw 
 |-  ( E. p e. NN0_s ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b  E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
68 58 67 bitrdi 
 |-  ( y = b -> ( E. p e. NN0_s ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y  E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
69 52 68 cbvrex2vw 
 |-  ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
70 46 69 bitrdi 
 |-  ( z = w -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
71 42 70 orbi12d 
 |-  ( z = w -> ( ( z = ( n +s 1s ) \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( n +s 1s ) \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
72 41 71 imbi12d 
 |-  ( z = w -> ( ( ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s z ) -> ( z = ( n +s 1s ) \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( ( ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s w ) -> ( w = ( n +s 1s ) \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
73 72 cbvralvw 
 |-  ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s z ) -> ( z = ( n +s 1s ) \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. w e. No ( ( ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s w ) -> ( w = ( n +s 1s ) \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
74 37 73 bitrdi 
 |-  ( m = ( n +s 1s ) -> ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. w e. No ( ( ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s w ) -> ( w = ( n +s 1s ) \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
75 fveq2 
 |-  ( m = N -> ( bday ` m ) = ( bday ` N ) )
76 75 sseq2d 
 |-  ( m = N -> ( ( bday ` z ) C_ ( bday ` m ) <-> ( bday ` z ) C_ ( bday ` N ) ) )
77 76 anbi1d 
 |-  ( m = N -> ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) <-> ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) ) )
78 eqeq2 
 |-  ( m = N -> ( z = m <-> z = N ) )
79 breq2 
 |-  ( m = N -> ( ( x +s p )  ( x +s p )
80 79 3anbi3d 
 |-  ( m = N -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
81 80 rexbidv 
 |-  ( m = N -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
82 81 2rexbidv 
 |-  ( m = N -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
83 78 82 orbi12d 
 |-  ( m = N -> ( ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
84 77 83 imbi12d 
 |-  ( m = N -> ( ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
85 84 ralbidv 
 |-  ( m = N -> ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` m ) /\ 0s <_s z ) -> ( z = m \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. z e. No ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
86 bday0b 
 |-  ( z e. No -> ( ( bday ` z ) = (/) <-> z = 0s ) )
87 orc 
 |-  ( z = 0s -> ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
88 86 87 biimtrdi 
 |-  ( z e. No -> ( ( bday ` z ) = (/) -> ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
89 88 adantrd 
 |-  ( z e. No -> ( ( ( bday ` z ) = (/) /\ 0s <_s z ) -> ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
90 89 rgen 
 |-  A. z e. No ( ( ( bday ` z ) = (/) /\ 0s <_s z ) -> ( z = 0s \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
91 simpl 
 |-  ( ( n e. NN0_s /\ A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  n e. NN0_s )
92 simpr 
 |-  ( ( n e. NN0_s /\ A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
93 91 92 bdayfinbndcbv 
 |-  ( ( n e. NN0_s /\ A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. t e. No ( ( ( bday ` t ) C_ ( bday ` n ) /\ 0s <_s t ) -> ( t = n \/ E. c e. NN0_s E. d e. NN0_s E. r e. NN0_s ( t = ( c +s ( d /su ( 2s ^su r ) ) ) /\ d
94 91 93 bdayfinbndlem1 
 |-  ( ( n e. NN0_s /\ A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. w e. No ( ( ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s w ) -> ( w = ( n +s 1s ) \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
95 94 ex 
 |-  ( n e. NN0_s -> ( A. z e. No ( ( ( bday ` z ) C_ ( bday ` n ) /\ 0s <_s z ) -> ( z = n \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  A. w e. No ( ( ( bday ` w ) C_ ( bday ` ( n +s 1s ) ) /\ 0s <_s w ) -> ( w = ( n +s 1s ) \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
96 15 26 74 85 90 95 n0sind 
 |-  ( N e. NN0_s -> A. z e. No ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y