Theorem bdayfinbndlem2

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

	Ref	Expression
Assertion	bdayfinbndlem2	Could not format assertion : No typesetting found for |- ( 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=0_s\to \mathrm{bday}\left(m\right)=\mathrm{bday}\left(0_s\right)$$
2		bday0	$$⊢\mathrm{bday}\left(0_s\right)=\varnothing$$
3	1 2	eqtrdi	$$⊢m=0_s\to \mathrm{bday}\left(m\right)=\varnothing$$
4	3	sseq2d	$$⊢m=0_s\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\leftrightarrow \mathrm{bday}\left(z\right)\subseteq \varnothing \right)$$
5		ss0b	$$⊢\mathrm{bday}\left(z\right)\subseteq \varnothing \leftrightarrow \mathrm{bday}\left(z\right)=\varnothing$$
6	4 5	bitrdi	$$⊢m=0_s\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\leftrightarrow \mathrm{bday}\left(z\right)=\varnothing \right)$$
7	6	anbi1d	$$⊢m=0_s\to \left(\left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\wedge 0_s{\le }_{s}z\right)\leftrightarrow \left(\mathrm{bday}\left(z\right)=\varnothing \wedge 0_s{\le }_{s}z\right)\right)$$
8		eqeq2	$$⊢m=0_s\to \left(z=m\leftrightarrow z=0_s\right)$$
9		breq2	$$⊢m=0_s\to \left(\left(x{+}_{s}p\right){<}_{s}m\leftrightarrow \left(x{+}_{s}p\right){<}_s{0}_s\right)$$
10	9	3anbi3d	Could not format ( m = 0s -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
11	10	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 ( 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\to \mathrm{bday}\left(m\right)=\mathrm{bday}\left(n\right)$$
17	16	sseq2d	$$⊢m=n\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\leftrightarrow \mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(n\right)\right)$$
18	17	anbi1d	$$⊢m=n\to \left(\left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\wedge 0_s{\le }_{s}z\right)\leftrightarrow \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(n\right)\wedge 0_s{\le }_{s}z\right)\right)$$
19		eqeq2	$$⊢m=n\to \left(z=m\leftrightarrow z=n\right)$$
20		breq2	$$⊢m=n\to \left(\left(x{+}_{s}p\right){<}_{s}m\leftrightarrow \left(x{+}_{s}p\right){<}_{s}n\right)$$
21	20	3anbi3d	Could not format ( m = n -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
22	21	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 ( 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{1}_s\to \mathrm{bday}\left(m\right)=\mathrm{bday}\left(n{+}_s{1}_s\right)$$
28	27	sseq2d	$$⊢m=n{+}_s{1}_s\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\leftrightarrow \mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\right)$$
29	28	anbi1d	$$⊢m=n{+}_s{1}_s\to \left(\left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\wedge 0_s{\le }_{s}z\right)\leftrightarrow \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\wedge 0_s{\le }_{s}z\right)\right)$$
30		eqeq2	$$⊢m=n{+}_s{1}_s\to \left(z=m\leftrightarrow z=n{+}_s{1}_s\right)$$
31		breq2	$$⊢m=n{+}_s{1}_s\to \left(\left(x{+}_{s}p\right){<}_{s}m\leftrightarrow \left(x{+}_{s}p\right){<}_s\left(n{+}_s{1}_s\right)\right)$$
32	31	3anbi3d	Could not format ( m = ( n +s 1s ) -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
33	32	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 ( 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\to \mathrm{bday}\left(z\right)=\mathrm{bday}\left(w\right)$$
39	38	sseq1d	$$⊢z=w\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\leftrightarrow \mathrm{bday}\left(w\right)\subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\right)$$
40		breq2	$$⊢z=w\to \left(0_s{\le }_{s}z\leftrightarrow 0_s{\le }_{s}w\right)$$
41	39 40	anbi12d	$$⊢z=w\to \left(\left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\wedge 0_s{\le }_{s}z\right)\leftrightarrow \left(\mathrm{bday}\left(w\right)\subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\wedge 0_s{\le }_{s}w\right)\right)$$
42		eqeq1	$$⊢z=w\to \left(z=n{+}_s{1}_s\leftrightarrow w=n{+}_s{1}_s\right)$$
43		eqeq1	Could not format ( z = w -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( z = w -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
44	43	3anbi1d	Could not format ( z = w -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
45	44	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( x = a -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( y /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( x = a -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( y /su ( 2s ^su p ) ) ) ) with typecode |-
48	47	eqeq2d	Could not format ( x = a -> ( w = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( x = a -> ( w = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
49		oveq1	$$⊢x=a\to x{+}_{s}p=a{+}_{s}p$$
50	49	breq1d	$$⊢x=a\to \left(\left(x{+}_{s}p\right){<}_s\left(n{+}_s{1}_s\right)\leftrightarrow \left(a{+}_{s}p\right){<}_s\left(n{+}_s{1}_s\right)\right)$$
51	48 50	3anbi13d	Could not format ( x = a -> ( ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y
52	51	rexbidv	Could not format ( 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 ( 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	Could not format ( y = b -> ( y /su ( 2s ^su p ) ) = ( b /su ( 2s ^su p ) ) ) : No typesetting found for |- ( y = b -> ( y /su ( 2s ^su p ) ) = ( b /su ( 2s ^su p ) ) ) with typecode |-
54	53	oveq2d	Could not format ( y = b -> ( a +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( y = b -> ( a +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su p ) ) ) ) with typecode |-
55	54	eqeq2d	Could not format ( y = b -> ( w = ( a +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( y = b -> ( w = ( a +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su p ) ) ) ) ) with typecode |-
56		breq1	Could not format ( y = b -> ( y b ( y b
57	55 56	3anbi12d	Could not format ( y = b -> ( ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b ( ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b
58	57	rexbidv	Could not format ( 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 ( 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	Could not format ( p = q -> ( 2s ^su p ) = ( 2s ^su q ) ) : No typesetting found for |- ( p = q -> ( 2s ^su p ) = ( 2s ^su q ) ) with typecode |-
60	59	oveq2d	Could not format ( p = q -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) ) : No typesetting found for |- ( p = q -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) ) with typecode |-
61	60	oveq2d	Could not format ( p = q -> ( a +s ( b /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( p = q -> ( a +s ( b /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su q ) ) ) ) with typecode |-
62	61	eqeq2d	Could not format ( p = q -> ( w = ( a +s ( b /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( p = q -> ( w = ( a +s ( b /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su q ) ) ) ) ) with typecode |-
63	59	breq2d	Could not format ( p = q -> ( b b ( b b
64		oveq2	$$⊢p=q\to a{+}_{s}p=a{+}_{s}q$$
65	64	breq1d	$$⊢p=q\to \left(\left(a{+}_{s}p\right){<}_s\left(n{+}_s{1}_s\right)\leftrightarrow \left(a{+}_{s}q\right){<}_s\left(n{+}_s{1}_s\right)\right)$$
66	62 63 65	3anbi123d	Could not format ( p = q -> ( ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b ( ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
67	66	cbvrexvw	Could not format ( 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 E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
68	58 67	bitrdi	Could not format ( 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 ( 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	Could not format ( 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 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( 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\to \mathrm{bday}\left(m\right)=\mathrm{bday}\left(N\right)$$
76	75	sseq2d	$$⊢m=N\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\leftrightarrow \mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(N\right)\right)$$
77	76	anbi1d	$$⊢m=N\to \left(\left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(m\right)\wedge 0_s{\le }_{s}z\right)\leftrightarrow \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(N\right)\wedge 0_s{\le }_{s}z\right)\right)$$
78		eqeq2	$$⊢m=N\to \left(z=m\leftrightarrow z=N\right)$$
79		breq2	$$⊢m=N\to \left(\left(x{+}_{s}p\right){<}_{s}m\leftrightarrow \left(x{+}_{s}p\right){<}_{s}N\right)$$
80	79	3anbi3d	Could not format ( m = N -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
81	80	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 ( 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\in \mathrm{No}\to \left(\mathrm{bday}\left(z\right)=\varnothing \leftrightarrow z=0_s\right)$$
87		orc	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( 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	Could not format 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 ( 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	Could not format ( ( 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 ) : No typesetting found for |- ( ( 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 ) with typecode |-
92		simpr	Could not format ( ( 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 ( 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	Could not format ( ( 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 ( 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	Could not format ( ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( 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