Theorem bdaypw2n0bndlem

Description: Lemma for bdaypw2n0bnd . Prove the case with a successor. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Assertion	bdaypw2n0bndlem	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑚 = 0s → ( 𝑚 +s 1s ) = ( 0s +s 1s ) )
2		1no	⊢ 1s ∈ No
3		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
4	2 3	ax-mp	⊢ ( 0s +s 1s ) = 1s
5	1 4	eqtrdi	⊢ ( 𝑚 = 0s → ( 𝑚 +s 1s ) = 1s )
6	5	oveq2d	⊢ ( 𝑚 = 0s → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s 1s ) )
7		2no	⊢ 2s ∈ No
8		exps1	⊢ ( 2s ∈ No → ( 2s ↑s 1s ) = 2s )
9	7 8	ax-mp	⊢ ( 2s ↑s 1s ) = 2s
10	6 9	eqtrdi	⊢ ( 𝑚 = 0s → ( 2s ↑s ( 𝑚 +s 1s ) ) = 2s )
11	10	breq2d	⊢ ( 𝑚 = 0s → ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) ↔ 𝑎 <s 2s ) )
12	10	oveq2d	⊢ ( 𝑚 = 0s → ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 𝑎 /su 2s ) )
13	12	fveq2d	⊢ ( 𝑚 = 0s → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) = ( bday ‘ ( 𝑎 /su 2s ) ) )
14	5	fveq2d	⊢ ( 𝑚 = 0s → ( bday ‘ ( 𝑚 +s 1s ) ) = ( bday ‘ 1s ) )
15		bday1	⊢ ( bday ‘ 1s ) = 1o
16	14 15	eqtrdi	⊢ ( 𝑚 = 0s → ( bday ‘ ( 𝑚 +s 1s ) ) = 1o )
17	16	suceqd	⊢ ( 𝑚 = 0s → suc ( bday ‘ ( 𝑚 +s 1s ) ) = suc 1o )
18		df-2o	⊢ 2o = suc 1o
19	17 18	eqtr4di	⊢ ( 𝑚 = 0s → suc ( bday ‘ ( 𝑚 +s 1s ) ) = 2o )
20	13 19	sseq12d	⊢ ( 𝑚 = 0s → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ↔ ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o ) )
21	11 20	imbi12d	⊢ ( 𝑚 = 0s → ( ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ( 𝑎 <s 2s → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o ) ) )
22	21	ralbidv	⊢ ( 𝑚 = 0s → ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s 2s → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o ) ) )
23		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 +s 1s ) = ( 𝑛 +s 1s ) )
24	23	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
25	24	breq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) ↔ 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
26	24	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
27	26	fveq2d	⊢ ( 𝑚 = 𝑛 → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) = ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
28	23	fveq2d	⊢ ( 𝑚 = 𝑛 → ( bday ‘ ( 𝑚 +s 1s ) ) = ( bday ‘ ( 𝑛 +s 1s ) ) )
29	28	suceqd	⊢ ( 𝑚 = 𝑛 → suc ( bday ‘ ( 𝑚 +s 1s ) ) = suc ( bday ‘ ( 𝑛 +s 1s ) ) )
30	27 29	sseq12d	⊢ ( 𝑚 = 𝑛 → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ↔ ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
31	25 30	imbi12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
32	31	ralbidv	⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
33		oveq1	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑚 +s 1s ) = ( ( 𝑛 +s 1s ) +s 1s ) )
34	33	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) )
35	34	breq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) ↔ 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
36	34	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
37	36	fveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) = ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
38	33	fveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( bday ‘ ( 𝑚 +s 1s ) ) = ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) )
39	38	suceqd	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → suc ( bday ‘ ( 𝑚 +s 1s ) ) = suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) )
40	37 39	sseq12d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ↔ ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
41	35 40	imbi12d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
42	41	ralbidv	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
43		oveq1	⊢ ( 𝑚 = 𝑁 → ( 𝑚 +s 1s ) = ( 𝑁 +s 1s ) )
44	43	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s ( 𝑁 +s 1s ) ) )
45	44	breq2d	⊢ ( 𝑚 = 𝑁 → ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) ↔ 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
46	44	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
47	46	fveq2d	⊢ ( 𝑚 = 𝑁 → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) = ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) )
48	43	fveq2d	⊢ ( 𝑚 = 𝑁 → ( bday ‘ ( 𝑚 +s 1s ) ) = ( bday ‘ ( 𝑁 +s 1s ) ) )
49	48	suceqd	⊢ ( 𝑚 = 𝑁 → suc ( bday ‘ ( 𝑚 +s 1s ) ) = suc ( bday ‘ ( 𝑁 +s 1s ) ) )
50	47 49	sseq12d	⊢ ( 𝑚 = 𝑁 → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ↔ ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) )
51	45 50	imbi12d	⊢ ( 𝑚 = 𝑁 → ( ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ( 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ) )
52	51	ralbidv	⊢ ( 𝑚 = 𝑁 → ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑚 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑚 +s 1s ) ) ) ↔ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ) )
53		1n0s	⊢ 1s ∈ ℕ0s
54		n0lesltp1	⊢ ( ( 𝑎 ∈ ℕ0s ∧ 1s ∈ ℕ0s ) → ( 𝑎 ≤s 1s ↔ 𝑎 <s ( 1s +s 1s ) ) )
55	53 54	mpan2	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 ≤s 1s ↔ 𝑎 <s ( 1s +s 1s ) ) )
56		1p1e2s	⊢ ( 1s +s 1s ) = 2s
57	56	breq2i	⊢ ( 𝑎 <s ( 1s +s 1s ) ↔ 𝑎 <s 2s )
58	55 57	bitrdi	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 ≤s 1s ↔ 𝑎 <s 2s ) )
59		n0no	⊢ ( 𝑎 ∈ ℕ0s → 𝑎 ∈ No )
60		lesloe	⊢ ( ( 𝑎 ∈ No ∧ 1s ∈ No ) → ( 𝑎 ≤s 1s ↔ ( 𝑎 <s 1s ∨ 𝑎 = 1s ) ) )
61	59 2 60	sylancl	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 ≤s 1s ↔ ( 𝑎 <s 1s ∨ 𝑎 = 1s ) ) )
62		0no	⊢ 0s ∈ No
63		lestri3	⊢ ( ( 𝑎 ∈ No ∧ 0s ∈ No ) → ( 𝑎 = 0s ↔ ( 𝑎 ≤s 0s ∧ 0s ≤s 𝑎 ) ) )
64	59 62 63	sylancl	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 = 0s ↔ ( 𝑎 ≤s 0s ∧ 0s ≤s 𝑎 ) ) )
65		n0sge0	⊢ ( 𝑎 ∈ ℕ0s → 0s ≤s 𝑎 )
66	65	biantrud	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 ≤s 0s ↔ ( 𝑎 ≤s 0s ∧ 0s ≤s 𝑎 ) ) )
67	64 66	bitr4d	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 = 0s ↔ 𝑎 ≤s 0s ) )
68		0n0s	⊢ 0s ∈ ℕ0s
69		n0lesltp1	⊢ ( ( 𝑎 ∈ ℕ0s ∧ 0s ∈ ℕ0s ) → ( 𝑎 ≤s 0s ↔ 𝑎 <s ( 0s +s 1s ) ) )
70	68 69	mpan2	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 ≤s 0s ↔ 𝑎 <s ( 0s +s 1s ) ) )
71	67 70	bitrd	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 = 0s ↔ 𝑎 <s ( 0s +s 1s ) ) )
72	4	breq2i	⊢ ( 𝑎 <s ( 0s +s 1s ) ↔ 𝑎 <s 1s )
73	71 72	bitrdi	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 = 0s ↔ 𝑎 <s 1s ) )
74	73	orbi1d	⊢ ( 𝑎 ∈ ℕ0s → ( ( 𝑎 = 0s ∨ 𝑎 = 1s ) ↔ ( 𝑎 <s 1s ∨ 𝑎 = 1s ) ) )
75	61 74	bitr4d	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 ≤s 1s ↔ ( 𝑎 = 0s ∨ 𝑎 = 1s ) ) )
76	58 75	bitr3d	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 <s 2s ↔ ( 𝑎 = 0s ∨ 𝑎 = 1s ) ) )
77		oveq1	⊢ ( 𝑎 = 0s → ( 𝑎 /su 2s ) = ( 0s /su 2s ) )
78	9	oveq2i	⊢ ( 0s /su ( 2s ↑s 1s ) ) = ( 0s /su 2s )
79	53	a1i	⊢ ( ⊤ → 1s ∈ ℕ0s )
80	79	pw2divs0d	⊢ ( ⊤ → ( 0s /su ( 2s ↑s 1s ) ) = 0s )
81	80	mptru	⊢ ( 0s /su ( 2s ↑s 1s ) ) = 0s
82	78 81	eqtr3i	⊢ ( 0s /su 2s ) = 0s
83	77 82	eqtrdi	⊢ ( 𝑎 = 0s → ( 𝑎 /su 2s ) = 0s )
84	83	fveq2d	⊢ ( 𝑎 = 0s → ( bday ‘ ( 𝑎 /su 2s ) ) = ( bday ‘ 0s ) )
85		bday0	⊢ ( bday ‘ 0s ) = ∅
86	84 85	eqtrdi	⊢ ( 𝑎 = 0s → ( bday ‘ ( 𝑎 /su 2s ) ) = ∅ )
87		0ss	⊢ ∅ ⊆ 2o
88	86 87	eqsstrdi	⊢ ( 𝑎 = 0s → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o )
89		oveq1	⊢ ( 𝑎 = 1s → ( 𝑎 /su 2s ) = ( 1s /su 2s ) )
90		nohalf	⊢ ( 1s /su 2s ) = ( { 0s } |s { 1s } )
91	89 90	eqtrdi	⊢ ( 𝑎 = 1s → ( 𝑎 /su 2s ) = ( { 0s } |s { 1s } ) )
92	91	fveq2d	⊢ ( 𝑎 = 1s → ( bday ‘ ( 𝑎 /su 2s ) ) = ( bday ‘ ( { 0s } |s { 1s } ) ) )
93	62	a1i	⊢ ( ⊤ → 0s ∈ No )
94	2	a1i	⊢ ( ⊤ → 1s ∈ No )
95		0lt1s	⊢ 0s <s 1s
96	95	a1i	⊢ ( ⊤ → 0s <s 1s )
97	93 94 96	sltssn	⊢ ( ⊤ → { 0s } <<s { 1s } )
98	97	mptru	⊢ { 0s } <<s { 1s }
99		2on	⊢ 2o ∈ On
100		df-pr	⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } )
101		df2o3	⊢ 2o = { ∅ , 1o }
102		imaundi	⊢ ( bday “ ( { 0s } ∪ { 1s } ) ) = ( ( bday “ { 0s } ) ∪ ( bday “ { 1s } ) )
103		bdayfn	⊢ bday Fn No
104		fnsnfv	⊢ ( ( bday Fn No ∧ 0s ∈ No ) → { ( bday ‘ 0s ) } = ( bday “ { 0s } ) )
105	103 62 104	mp2an	⊢ { ( bday ‘ 0s ) } = ( bday “ { 0s } )
106	85	sneqi	⊢ { ( bday ‘ 0s ) } = { ∅ }
107	105 106	eqtr3i	⊢ ( bday “ { 0s } ) = { ∅ }
108		fnsnfv	⊢ ( ( bday Fn No ∧ 1s ∈ No ) → { ( bday ‘ 1s ) } = ( bday “ { 1s } ) )
109	103 2 108	mp2an	⊢ { ( bday ‘ 1s ) } = ( bday “ { 1s } )
110	15	sneqi	⊢ { ( bday ‘ 1s ) } = { 1o }
111	109 110	eqtr3i	⊢ ( bday “ { 1s } ) = { 1o }
112	107 111	uneq12i	⊢ ( ( bday “ { 0s } ) ∪ ( bday “ { 1s } ) ) = ( { ∅ } ∪ { 1o } )
113	102 112	eqtri	⊢ ( bday “ ( { 0s } ∪ { 1s } ) ) = ( { ∅ } ∪ { 1o } )
114	100 101 113	3eqtr4ri	⊢ ( bday “ ( { 0s } ∪ { 1s } ) ) = 2o
115		ssid	⊢ 2o ⊆ 2o
116	114 115	eqsstri	⊢ ( bday “ ( { 0s } ∪ { 1s } ) ) ⊆ 2o
117		cutbdaybnd	⊢ ( ( { 0s } <<s { 1s } ∧ 2o ∈ On ∧ ( bday “ ( { 0s } ∪ { 1s } ) ) ⊆ 2o ) → ( bday ‘ ( { 0s } |s { 1s } ) ) ⊆ 2o )
118	98 99 116 117	mp3an	⊢ ( bday ‘ ( { 0s } |s { 1s } ) ) ⊆ 2o
119	92 118	eqsstrdi	⊢ ( 𝑎 = 1s → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o )
120	88 119	jaoi	⊢ ( ( 𝑎 = 0s ∨ 𝑎 = 1s ) → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o )
121	76 120	biimtrdi	⊢ ( 𝑎 ∈ ℕ0s → ( 𝑎 <s 2s → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o ) )
122	121	rgen	⊢ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s 2s → ( bday ‘ ( 𝑎 /su 2s ) ) ⊆ 2o )
123		nfv	⊢ Ⅎ 𝑎 𝑛 ∈ ℕ0s
124		nfra1	⊢ Ⅎ 𝑎 ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) )
125	123 124	nfan	⊢ Ⅎ 𝑎 ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
126		n0seo	⊢ ( 𝑎 ∈ ℕ0s → ( ∃ 𝑥 ∈ ℕ0s 𝑎 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
127		breq1	⊢ ( 𝑎 = 𝑥 → ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ↔ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
128		fvoveq1	⊢ ( 𝑎 = 𝑥 → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
129	128	sseq1d	⊢ ( 𝑎 = 𝑥 → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
130	127 129	imbi12d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ↔ ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
131	130	rspccv	⊢ ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( 𝑥 ∈ ℕ0s → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
132	131	adantl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( 𝑥 ∈ ℕ0s → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
133	132	imp32	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) )
134		sssucid	⊢ suc ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) )
135	133 134	sstrdi	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
136		simpll	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 𝑛 ∈ ℕ0s )
137		peano2n0s	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) ∈ ℕ0s )
138	136 137	syl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
139	138	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
140		bdayn0p1	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) = suc ( bday ‘ ( 𝑛 +s 1s ) ) )
141	139 140	syl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) = suc ( bday ‘ ( 𝑛 +s 1s ) ) )
142	141	suceqd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) = suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
143	135 142	sseqtrrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) )
144	143	expr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
145		expsp1	⊢ ( ( 2s ∈ No ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) )
146	7 138 145	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) )
147		expscl	⊢ ( ( 2s ∈ No ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
148	7 138 147	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
149	7	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 2s ∈ No )
150	148 149	mulscomd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) = ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
151	146 150	eqtrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
152	151	breq2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( 2s ·s 𝑥 ) <s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
153		n0no	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
154	153	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 𝑥 ∈ No )
155		2nns	⊢ 2s ∈ ℕs
156		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
157	155 156	ax-mp	⊢ 0s <s 2s
158	157	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 0s <s 2s )
159	154 148 149 158	ltmuls2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ↔ ( 2s ·s 𝑥 ) <s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
160	152 159	bitr4d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
161	53	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 1s ∈ ℕ0s )
162	154 138 161	pw2divscan4d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
163	162	fveq2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
164	163	sseq1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
165	164	bicomd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
166	144 160 165	3imtr4d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
167		breq1	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( 2s ·s 𝑥 ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
168		id	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → 𝑎 = ( 2s ·s 𝑥 ) )
169	9	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s 𝑥 ) = ( 2s ·s 𝑥 )
170	168 169	eqtr4di	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → 𝑎 = ( ( 2s ↑s 1s ) ·s 𝑥 ) )
171	170	oveq1d	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
172	171	fveq2d	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) = ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
173	172	sseq1d	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
174	167 173	imbi12d	⊢ ( 𝑎 = ( 2s ·s 𝑥 ) → ( ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ↔ ( ( 2s ·s 𝑥 ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( ( ( 2s ↑s 1s ) ·s 𝑥 ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
175	166 174	syl5ibrcom	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑎 = ( 2s ·s 𝑥 ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
176	175	rexlimdva	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( ∃ 𝑥 ∈ ℕ0s 𝑎 = ( 2s ·s 𝑥 ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
177		n0zs	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ ℤs )
178	177	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 𝑥 ∈ ℤs )
179	178	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → 𝑥 ∈ ℤs )
180	179	znod	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → 𝑥 ∈ No )
181	138	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
182	180 181	pw2divscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
183		1zs	⊢ 1s ∈ ℤs
184	183	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → 1s ∈ ℤs )
185	179 184	zaddscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑥 +s 1s ) ∈ ℤs )
186	185	znod	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑥 +s 1s ) ∈ No )
187	186 181	pw2divscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
188	180	ltsp1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → 𝑥 <s ( 𝑥 +s 1s ) )
189	180 186 181	pw2ltsdiv1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑥 <s ( 𝑥 +s 1s ) ↔ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
190	188 189	mpbid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
191	182 187 190	sltssn	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
192		imaundi	⊢ ( bday “ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ∪ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( ( bday “ { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∪ ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
193		fnsnfv	⊢ ( ( bday Fn No ∧ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No ) → { ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } = ( bday “ { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
194	103 182 193	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → { ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } = ( bday “ { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
195		oveq1	⊢ ( 𝑎 = 𝑥 → ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
196	195	fveq2d	⊢ ( 𝑎 = 𝑥 → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
197	196	sseq1d	⊢ ( 𝑎 = 𝑥 → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
198	127 197	imbi12d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ↔ ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
199	198	rspccv	⊢ ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( 𝑥 ∈ ℕ0s → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
200	199	imp	⊢ ( ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
201	200	adantll	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
202	201	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
203	148	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
204	203 203	addscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
205	154	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → 𝑥 ∈ No )
206	205 203	addscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 𝑥 +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
207		peano2n0s	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 +s 1s ) ∈ ℕ0s )
208	207	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 +s 1s ) ∈ ℕ0s )
209	208	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 𝑥 +s 1s ) ∈ ℕ0s )
210	209	n0nod	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 𝑥 +s 1s ) ∈ No )
211	205 210	addscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 𝑥 +s ( 𝑥 +s 1s ) ) ∈ No )
212		simprr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 )
213	203 205 203	leadds1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ↔ ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ≤s ( 𝑥 +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
214	212 213	mpbid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ≤s ( 𝑥 +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
215	205	ltsp1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → 𝑥 <s ( 𝑥 +s 1s ) )
216	203 205 210 212 215	leltstrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) <s ( 𝑥 +s 1s ) )
217	203 210 216	ltlesd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s ( 𝑥 +s 1s ) )
218	203 210 205	leadds2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s ( 𝑥 +s 1s ) ↔ ( 𝑥 +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ≤s ( 𝑥 +s ( 𝑥 +s 1s ) ) ) )
219	217 218	mpbid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 𝑥 +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ≤s ( 𝑥 +s ( 𝑥 +s 1s ) ) )
220	204 206 211 214 219	lestrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ≤s ( 𝑥 +s ( 𝑥 +s 1s ) ) )
221	138	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
222	7 221 145	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) )
223	7	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → 2s ∈ No )
224	203 223	mulscomd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) = ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
225		no2times	⊢ ( ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No → ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
226	203 225	syl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
227	222 224 226	3eqtrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) +s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
228		no2times	⊢ ( 𝑥 ∈ No → ( 2s ·s 𝑥 ) = ( 𝑥 +s 𝑥 ) )
229	205 228	syl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ·s 𝑥 ) = ( 𝑥 +s 𝑥 ) )
230	229	oveq1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 𝑥 +s 𝑥 ) +s 1s ) )
231	2	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → 1s ∈ No )
232	205 205 231	addsassd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 𝑥 +s 𝑥 ) +s 1s ) = ( 𝑥 +s ( 𝑥 +s 1s ) ) )
233	230 232	eqtrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( ( 2s ·s 𝑥 ) +s 1s ) = ( 𝑥 +s ( 𝑥 +s 1s ) ) )
234	220 227 233	3brtr4d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ) ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ≤s ( ( 2s ·s 𝑥 ) +s 1s ) )
235	234	expr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ≤s ( ( 2s ·s 𝑥 ) +s 1s ) ) )
236		lenlts	⊢ ( ( ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No ∧ 𝑥 ∈ No ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ↔ ¬ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
237	148 154 236	syl2anc	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ≤s 𝑥 ↔ ¬ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
238		peano2n0s	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → ( ( 𝑛 +s 1s ) +s 1s ) ∈ ℕ0s )
239	138 238	syl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑛 +s 1s ) +s 1s ) ∈ ℕ0s )
240		expscl	⊢ ( ( 2s ∈ No ∧ ( ( 𝑛 +s 1s ) +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ∈ No )
241	7 239 240	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ∈ No )
242		nnn0s	⊢ ( 2s ∈ ℕs → 2s ∈ ℕ0s )
243	155 242	ax-mp	⊢ 2s ∈ ℕ0s
244		n0mulscl	⊢ ( ( 2s ∈ ℕ0s ∧ 𝑥 ∈ ℕ0s ) → ( 2s ·s 𝑥 ) ∈ ℕ0s )
245	243 244	mpan	⊢ ( 𝑥 ∈ ℕ0s → ( 2s ·s 𝑥 ) ∈ ℕ0s )
246	245	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ·s 𝑥 ) ∈ ℕ0s )
247		n0addscl	⊢ ( ( ( 2s ·s 𝑥 ) ∈ ℕ0s ∧ 1s ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) +s 1s ) ∈ ℕ0s )
248	246 53 247	sylancl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) +s 1s ) ∈ ℕ0s )
249	248	n0nod	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) +s 1s ) ∈ No )
250		lenlts	⊢ ( ( ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ∈ No ∧ ( ( 2s ·s 𝑥 ) +s 1s ) ∈ No ) → ( ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ≤s ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ¬ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
251	241 249 250	syl2anc	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ≤s ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ¬ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
252	235 237 251	3imtr3d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ¬ 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ¬ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
253	252	con4d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
254	253	impr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) )
255		id	⊢ ( ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( 𝑥 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
256	202 254 255	sylc	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) )
257		bdayon	⊢ ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ On
258		bdayon	⊢ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On
259	258	onsuci	⊢ suc ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On
260		onsssuc	⊢ ( ( ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ On ∧ suc ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On ) → ( ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
261	257 259 260	mp2an	⊢ ( ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
262	256 261	sylib	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
263	262	snssd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → { ( bday ‘ ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
264	194 263	eqsstrrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday “ { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
265	151	breq2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
266		n0expscl	⊢ ( ( 2s ∈ ℕ0s ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ ℕ0s )
267	243 138 266	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ ℕ0s )
268		n0mulscl	⊢ ( ( 2s ∈ ℕ0s ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ ℕ0s ) → ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ ℕ0s )
269	243 267 268	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ ℕ0s )
270		n0ltsp1le	⊢ ( ( ( ( 2s ·s 𝑥 ) +s 1s ) ∈ ℕ0s ∧ ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
271	248 269 270	syl2anc	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
272	149 154	mulscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ·s 𝑥 ) ∈ No )
273	2	a1i	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → 1s ∈ No )
274	272 273 273	addsassd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( ( 2s ·s 𝑥 ) +s ( 1s +s 1s ) ) )
275		mulsrid	⊢ ( 2s ∈ No → ( 2s ·s 1s ) = 2s )
276	7 275	ax-mp	⊢ ( 2s ·s 1s ) = 2s
277	276	eqcomi	⊢ 2s = ( 2s ·s 1s )
278	56 277	eqtri	⊢ ( 1s +s 1s ) = ( 2s ·s 1s )
279	278	oveq2i	⊢ ( ( 2s ·s 𝑥 ) +s ( 1s +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s ( 2s ·s 1s ) )
280	149 154 273	addsdid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 2s ·s ( 𝑥 +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s ( 2s ·s 1s ) ) )
281	280	eqcomd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) +s ( 2s ·s 1s ) ) = ( 2s ·s ( 𝑥 +s 1s ) ) )
282	279 281	eqtrid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s 𝑥 ) +s ( 1s +s 1s ) ) = ( 2s ·s ( 𝑥 +s 1s ) ) )
283	274 282	eqtrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s ( 𝑥 +s 1s ) ) )
284	283	breq1d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( 2s ·s ( 𝑥 +s 1s ) ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
285	208	n0nod	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑥 +s 1s ) ∈ No )
286	285 148 149 158	lemuls2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ↔ ( 2s ·s ( 𝑥 +s 1s ) ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
287	286	bicomd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ·s ( 𝑥 +s 1s ) ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
288	284 287	bitrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) ≤s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
289	271 288	bitrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
290	265 289	bitrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
291		lesloe	⊢ ( ( ( 𝑥 +s 1s ) ∈ No ∧ ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No ) → ( ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ↔ ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ∨ ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
292	285 148 291	syl2anc	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) ↔ ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ∨ ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
293	285 138	pw2divscld	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
294	293	adantrr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
295		fnsnfv	⊢ ( ( bday Fn No ∧ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No ) → { ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } = ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
296	103 294 295	sylancr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → { ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } = ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
297		breq1	⊢ ( 𝑎 = ( 𝑥 +s 1s ) → ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) ↔ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
298		fvoveq1	⊢ ( 𝑎 = ( 𝑥 +s 1s ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
299	298	sseq1d	⊢ ( 𝑎 = ( 𝑥 +s 1s ) → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
300	297 299	imbi12d	⊢ ( 𝑎 = ( 𝑥 +s 1s ) → ( ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ↔ ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
301	300	rspccv	⊢ ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( ( 𝑥 +s 1s ) ∈ ℕ0s → ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
302	207 301	syl5	⊢ ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( 𝑥 ∈ ℕ0s → ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
303	302	adantl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( 𝑥 ∈ ℕ0s → ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) )
304	303	imp32	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) )
305		bdayon	⊢ ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ On
306		onsssuc	⊢ ( ( ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ On ∧ suc ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On ) → ( ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
307	305 259 306	mp2an	⊢ ( ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
308	304 307	sylib	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
309	308	snssd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → { ( bday ‘ ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
310	296 309	eqsstrrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
311	310	expr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
312	138	pw2divsidd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = 1s )
313	312	sneqd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → { ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } = { 1s } )
314	313	imaeq2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( bday “ { ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) = ( bday “ { 1s } ) )
315		df-1o	⊢ 1o = suc ∅
316	15 315	eqtri	⊢ ( bday ‘ 1s ) = suc ∅
317		0ss	⊢ ∅ ⊆ ( bday ‘ ( 𝑛 +s 1s ) )
318		ord0	⊢ Ord ∅
319	258	onordi	⊢ Ord ( bday ‘ ( 𝑛 +s 1s ) )
320		ordsucsssuc	⊢ ( ( Ord ∅ ∧ Ord ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( ∅ ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ↔ suc ∅ ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
321	318 319 320	mp2an	⊢ ( ∅ ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ↔ suc ∅ ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) )
322	317 321	mpbi	⊢ suc ∅ ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) )
323	316 322	eqsstri	⊢ ( bday ‘ 1s ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) )
324		bdayon	⊢ ( bday ‘ 1s ) ∈ On
325		onsssuc	⊢ ( ( ( bday ‘ 1s ) ∈ On ∧ suc ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On ) → ( ( bday ‘ 1s ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ 1s ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
326	324 259 325	mp2an	⊢ ( ( bday ‘ 1s ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ 1s ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
327	323 326	mpbi	⊢ ( bday ‘ 1s ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) )
328	327	a1i	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ 1s ) ∈ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
329	328	snssd	⊢ ( 𝑛 ∈ ℕ0s → { ( bday ‘ 1s ) } ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
330	109 329	eqsstrrid	⊢ ( 𝑛 ∈ ℕ0s → ( bday “ { 1s } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
331	330	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( bday “ { 1s } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
332	331	adantr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( bday “ { 1s } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
333	314 332	eqsstrd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( bday “ { ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
334		oveq1	⊢ ( ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) → ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
335	334	sneqd	⊢ ( ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) → { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } = { ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
336	335	imaeq2d	⊢ ( ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) = ( bday “ { ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
337	336	sseq1d	⊢ ( ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) → ( ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday “ { ( ( 2s ↑s ( 𝑛 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
338	333 337	syl5ibrcom	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
339	311 338	jaod	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 𝑥 +s 1s ) <s ( 2s ↑s ( 𝑛 +s 1s ) ) ∨ ( 𝑥 +s 1s ) = ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
340	292 339	sylbid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑥 +s 1s ) ≤s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
341	290 340	sylbid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) )
342	341	impr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
343	264 342	unssd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( ( bday “ { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∪ ( bday “ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
344	192 343	eqsstrid	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday “ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ∪ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
345	259	onsuci	⊢ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On
346		cutbdaybnd	⊢ ( ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ∧ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On ∧ ( bday “ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ∪ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( bday ‘ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
347	345 346	mp3an2	⊢ ( ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ∧ ( bday “ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ∪ { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ( bday ‘ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
348	191 344 347	syl2anc	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday ‘ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ⊆ suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
349	179 181	pw2cutp1	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
350	349	fveq2d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday ‘ ( { ( 𝑥 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝑥 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( bday ‘ ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
351	181 140	syl	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) = suc ( bday ‘ ( 𝑛 +s 1s ) ) )
352	351	suceqd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) = suc suc ( bday ‘ ( 𝑛 +s 1s ) ) )
353	352	eqcomd	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → suc suc ( bday ‘ ( 𝑛 +s 1s ) ) = suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) )
354	348 350 353	3sstr3d	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) → ( bday ‘ ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) )
355	354	expr	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
356		breq1	⊢ ( 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
357		oveq1	⊢ ( 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
358	357	fveq2d	⊢ ( 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) = ( bday ‘ ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
359	358	sseq1d	⊢ ( 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ↔ ( bday ‘ ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
360	356 359	imbi12d	⊢ ( 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ↔ ( ( ( 2s ·s 𝑥 ) +s 1s ) <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
361	355 360	syl5ibrcom	⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) ∧ 𝑥 ∈ ℕ0s ) → ( 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
362	361	rexlimdva	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( ∃ 𝑥 ∈ ℕ0s 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
363	176 362	jaod	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( ( ∃ 𝑥 ∈ ℕ0s 𝑎 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑎 = ( ( 2s ·s 𝑥 ) +s 1s ) ) → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
364	126 363	syl5	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ( 𝑎 ∈ ℕ0s → ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
365	125 364	ralrimi	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) ) → ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
366	365	ex	⊢ ( 𝑛 ∈ ℕ0s → ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑛 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑛 +s 1s ) ) ) → ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( ( 𝑛 +s 1s ) +s 1s ) ) ) ) )
367	22 32 42 52 122 366	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) )
368		breq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) ↔ 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
369		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) = ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
370	369	fveq2d	⊢ ( 𝑎 = 𝐴 → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) = ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) )
371	370	sseq1d	⊢ ( 𝑎 = 𝐴 → ( ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ↔ ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) )
372	368 371	imbi12d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ↔ ( 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ) )
373	372	rspccv	⊢ ( ∀ 𝑎 ∈ ℕ0s ( 𝑎 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝑎 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ) )
374	367 373	syl	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ) )
375	374	com12	⊢ ( 𝐴 ∈ ℕ0s → ( 𝑁 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) ) ) )
376	375	3imp	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s ( 2s ↑s ( 𝑁 +s 1s ) ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑁 +s 1s ) ) )