Theorem bdaypw2n0sbndlem 28440

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

Assertion

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

Proof of Theorem bdaypw2n0sbndlem

Dummy variables 𝑎 𝑛 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7365	. . . . . . . . . . 11 ⊢ (𝑚 = 0s → (𝑚 +s 1s ) = ( 0s +s 1s ))
2		1sno 27806	. . . . . . . . . . . 12 ⊢ 1s ∈ No
3		addslid 27948	. . . . . . . . . . . 12 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
4	2, 3	ax-mp 5	. . . . . . . . . . 11 ⊢ ( 0s +s 1s ) = 1s
5	1, 4	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝑚 = 0s → (𝑚 +s 1s ) = 1s )
6	5	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑚 = 0s → (2s↑s(𝑚 +s 1s )) = (2s↑s 1s ))
7		2sno 28396	. . . . . . . . . 10 ⊢ 2s ∈ No
8		exps1 28405	. . . . . . . . . 10 ⊢ (2s ∈ No → (2s↑s 1s ) = 2s)
9	7, 8	ax-mp 5	. . . . . . . . 9 ⊢ (2s↑s 1s ) = 2s
10	6, 9	eqtrdi 2786	. . . . . . . 8 ⊢ (𝑚 = 0s → (2s↑s(𝑚 +s 1s )) = 2s)
11	10	breq2d 5109	. . . . . . 7 ⊢ (𝑚 = 0s → (𝑎 <s (2s↑s(𝑚 +s 1s )) ↔ 𝑎 <s 2s))
12	10	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑚 = 0s → (𝑎 /su (2s↑s(𝑚 +s 1s ))) = (𝑎 /su 2s))
13	12	fveq2d 6837	. . . . . . . 8 ⊢ (𝑚 = 0s → ( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) = ( bday ‘(𝑎 /su 2s)))
14	5	fveq2d 6837	. . . . . . . . . . 11 ⊢ (𝑚 = 0s → ( bday ‘(𝑚 +s 1s )) = ( bday ‘ 1s ))
15		bday1s 27810	. . . . . . . . . . 11 ⊢ ( bday ‘ 1s ) = 1o
16	14, 15	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝑚 = 0s → ( bday ‘(𝑚 +s 1s )) = 1o)
17	16	suceqd 6383	. . . . . . . . 9 ⊢ (𝑚 = 0s → suc ( bday ‘(𝑚 +s 1s )) = suc 1o)
18		df-2o 8398	. . . . . . . . 9 ⊢ 2o = suc 1o
19	17, 18	eqtr4di 2788	. . . . . . . 8 ⊢ (𝑚 = 0s → suc ( bday ‘(𝑚 +s 1s )) = 2o)
20	13, 19	sseq12d 3966	. . . . . . 7 ⊢ (𝑚 = 0s → (( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) ⊆ suc ( bday ‘(𝑚 +s 1s )) ↔ ( bday ‘(𝑎 /su 2s)) ⊆ 2o))
21	11, 20	imbi12d 344	. . . . . 6 ⊢ (𝑚 = 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 3158	. . . . 5 ⊢ (𝑚 = 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 7365	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑚 +s 1s ) = (𝑛 +s 1s ))
24	23	oveq2d 7374	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (2s↑s(𝑚 +s 1s )) = (2s↑s(𝑛 +s 1s )))
25	24	breq2d 5109	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑎 <s (2s↑s(𝑚 +s 1s )) ↔ 𝑎 <s (2s↑s(𝑛 +s 1s ))))
26	24	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑎 /su (2s↑s(𝑚 +s 1s ))) = (𝑎 /su (2s↑s(𝑛 +s 1s ))))
27	26	fveq2d 6837	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) = ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))))
28	23	fveq2d 6837	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → ( bday ‘(𝑚 +s 1s )) = ( bday ‘(𝑛 +s 1s )))
29	28	suceqd 6383	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → suc ( bday ‘(𝑚 +s 1s )) = suc ( bday ‘(𝑛 +s 1s )))
30	27, 29	sseq12d 3966	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) ⊆ suc ( bday ‘(𝑚 +s 1s )) ↔ ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s ))))
31	25, 30	imbi12d 344	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝑎 <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 3158	. . . . 5 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ ℕ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 7365	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 +s 1s ) → (𝑚 +s 1s ) = ((𝑛 +s 1s ) +s 1s ))
34	33	oveq2d 7374	. . . . . . . 8 ⊢ (𝑚 = (𝑛 +s 1s ) → (2s↑s(𝑚 +s 1s )) = (2s↑s((𝑛 +s 1s ) +s 1s )))
35	34	breq2d 5109	. . . . . . 7 ⊢ (𝑚 = (𝑛 +s 1s ) → (𝑎 <s (2s↑s(𝑚 +s 1s )) ↔ 𝑎 <s (2s↑s((𝑛 +s 1s ) +s 1s ))))
36	34	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 +s 1s ) → (𝑎 /su (2s↑s(𝑚 +s 1s ))) = (𝑎 /su (2s↑s((𝑛 +s 1s ) +s 1s ))))
37	36	fveq2d 6837	. . . . . . . 8 ⊢ (𝑚 = (𝑛 +s 1s ) → ( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) = ( bday ‘(𝑎 /su (2s↑s((𝑛 +s 1s ) +s 1s )))))
38	33	fveq2d 6837	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 +s 1s ) → ( bday ‘(𝑚 +s 1s )) = ( bday ‘((𝑛 +s 1s ) +s 1s )))
39	38	suceqd 6383	. . . . . . . 8 ⊢ (𝑚 = (𝑛 +s 1s ) → suc ( bday ‘(𝑚 +s 1s )) = suc ( bday ‘((𝑛 +s 1s ) +s 1s )))
40	37, 39	sseq12d 3966	. . . . . . 7 ⊢ (𝑚 = (𝑛 +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 344	. . . . . 6 ⊢ (𝑚 = (𝑛 +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 3158	. . . . 5 ⊢ (𝑚 = (𝑛 +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 7365	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (𝑚 +s 1s ) = (𝑁 +s 1s ))
44	43	oveq2d 7374	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (2s↑s(𝑚 +s 1s )) = (2s↑s(𝑁 +s 1s )))
45	44	breq2d 5109	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑎 <s (2s↑s(𝑚 +s 1s )) ↔ 𝑎 <s (2s↑s(𝑁 +s 1s ))))
46	44	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (𝑎 /su (2s↑s(𝑚 +s 1s ))) = (𝑎 /su (2s↑s(𝑁 +s 1s ))))
47	46	fveq2d 6837	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → ( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) = ( bday ‘(𝑎 /su (2s↑s(𝑁 +s 1s )))))
48	43	fveq2d 6837	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ( bday ‘(𝑚 +s 1s )) = ( bday ‘(𝑁 +s 1s )))
49	48	suceqd 6383	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → suc ( bday ‘(𝑚 +s 1s )) = suc ( bday ‘(𝑁 +s 1s )))
50	47, 49	sseq12d 3966	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (( bday ‘(𝑎 /su (2s↑s(𝑚 +s 1s )))) ⊆ suc ( bday ‘(𝑚 +s 1s )) ↔ ( bday ‘(𝑎 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s ))))
51	45, 50	imbi12d 344	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((𝑎 <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 3158	. . . . 5 ⊢ (𝑚 = 𝑁 → (∀𝑎 ∈ ℕ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 28326	. . . . . . . . . 10 ⊢ 1s ∈ ℕ0s
54		n0sleltp1 28343	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℕ0s ∧ 1s ∈ ℕ0s) → (𝑎 ≤s 1s ↔ 𝑎 <s ( 1s +s 1s )))
55	53, 54	mpan2 692	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ0s → (𝑎 ≤s 1s ↔ 𝑎 <s ( 1s +s 1s )))
56		1p1e2s 28393	. . . . . . . . . 10 ⊢ ( 1s +s 1s ) = 2s
57	56	breq2i 5105	. . . . . . . . 9 ⊢ (𝑎 <s ( 1s +s 1s ) ↔ 𝑎 <s 2s)
58	55, 57	bitrdi 287	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ0s → (𝑎 ≤s 1s ↔ 𝑎 <s 2s))
59		n0sno 28302	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ0s → 𝑎 ∈ No )
60		sleloe 27724	. . . . . . . . . 10 ⊢ ((𝑎 ∈ No ∧ 1s ∈ No ) → (𝑎 ≤s 1s ↔ (𝑎 <s 1s ∨ 𝑎 = 1s )))
61	59, 2, 60	sylancl 587	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ0s → (𝑎 ≤s 1s ↔ (𝑎 <s 1s ∨ 𝑎 = 1s )))
62		0sno 27805	. . . . . . . . . . . . . 14 ⊢ 0s ∈ No
63		sletri3 27725	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ No ∧ 0s ∈ No ) → (𝑎 = 0s ↔ (𝑎 ≤s 0s ∧ 0s ≤s 𝑎)))
64	59, 62, 63	sylancl 587	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ0s → (𝑎 = 0s ↔ (𝑎 ≤s 0s ∧ 0s ≤s 𝑎)))
65		n0sge0 28316	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ0s → 0s ≤s 𝑎)
66	65	biantrud 531	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ0s → (𝑎 ≤s 0s ↔ (𝑎 ≤s 0s ∧ 0s ≤s 𝑎)))
67	64, 66	bitr4d 282	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ0s → (𝑎 = 0s ↔ 𝑎 ≤s 0s ))
68		0n0s 28308	. . . . . . . . . . . . 13 ⊢ 0s ∈ ℕ0s
69		n0sleltp1 28343	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℕ0s ∧ 0s ∈ ℕ0s) → (𝑎 ≤s 0s ↔ 𝑎 <s ( 0s +s 1s )))
70	68, 69	mpan2 692	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ0s → (𝑎 ≤s 0s ↔ 𝑎 <s ( 0s +s 1s )))
71	67, 70	bitrd 279	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ0s → (𝑎 = 0s ↔ 𝑎 <s ( 0s +s 1s )))
72	4	breq2i 5105	. . . . . . . . . . 11 ⊢ (𝑎 <s ( 0s +s 1s ) ↔ 𝑎 <s 1s )
73	71, 72	bitrdi 287	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ0s → (𝑎 = 0s ↔ 𝑎 <s 1s ))
74	73	orbi1d 917	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ0s → ((𝑎 = 0s ∨ 𝑎 = 1s ) ↔ (𝑎 <s 1s ∨ 𝑎 = 1s )))
75	61, 74	bitr4d 282	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ0s → (𝑎 ≤s 1s ↔ (𝑎 = 0s ∨ 𝑎 = 1s )))
76	58, 75	bitr3d 281	. . . . . . 7 ⊢ (𝑎 ∈ ℕ0s → (𝑎 <s 2s ↔ (𝑎 = 0s ∨ 𝑎 = 1s )))
77		oveq1 7365	. . . . . . . . . . . 12 ⊢ (𝑎 = 0s → (𝑎 /su 2s) = ( 0s /su 2s))
78	9	oveq2i 7369	. . . . . . . . . . . . 13 ⊢ ( 0s /su (2s↑s 1s )) = ( 0s /su 2s)
79	53	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → 1s ∈ ℕ0s)
80	79	pw2divs0d 28432	. . . . . . . . . . . . . 14 ⊢ (⊤ → ( 0s /su (2s↑s 1s )) = 0s )
81	80	mptru 1549	. . . . . . . . . . . . 13 ⊢ ( 0s /su (2s↑s 1s )) = 0s
82	78, 81	eqtr3i 2760	. . . . . . . . . . . 12 ⊢ ( 0s /su 2s) = 0s
83	77, 82	eqtrdi 2786	. . . . . . . . . . 11 ⊢ (𝑎 = 0s → (𝑎 /su 2s) = 0s )
84	83	fveq2d 6837	. . . . . . . . . 10 ⊢ (𝑎 = 0s → ( bday ‘(𝑎 /su 2s)) = ( bday ‘ 0s ))
85		bday0s 27807	. . . . . . . . . 10 ⊢ ( bday ‘ 0s ) = ∅
86	84, 85	eqtrdi 2786	. . . . . . . . 9 ⊢ (𝑎 = 0s → ( bday ‘(𝑎 /su 2s)) = ∅)
87		0ss 4351	. . . . . . . . 9 ⊢ ∅ ⊆ 2o
88	86, 87	eqsstrdi 3977	. . . . . . . 8 ⊢ (𝑎 = 0s → ( bday ‘(𝑎 /su 2s)) ⊆ 2o)
89		oveq1 7365	. . . . . . . . . . 11 ⊢ (𝑎 = 1s → (𝑎 /su 2s) = ( 1s /su 2s))
90		nohalf 28401	. . . . . . . . . . 11 ⊢ ( 1s /su 2s) = ({ 0s } |s { 1s })
91	89, 90	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝑎 = 1s → (𝑎 /su 2s) = ({ 0s } |s { 1s }))
92	91	fveq2d 6837	. . . . . . . . 9 ⊢ (𝑎 = 1s → ( bday ‘(𝑎 /su 2s)) = ( bday ‘({ 0s } |s { 1s })))
93	62	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → 0s ∈ No )
94	2	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → 1s ∈ No )
95		0slt1s 27808	. . . . . . . . . . . . 13 ⊢ 0s <s 1s
96	95	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → 0s <s 1s )
97	93, 94, 96	ssltsn 27768	. . . . . . . . . . 11 ⊢ (⊤ → { 0s } <<s { 1s })
98	97	mptru 1549	. . . . . . . . . 10 ⊢ { 0s } <<s { 1s }
99		2on 8410	. . . . . . . . . 10 ⊢ 2o ∈ On
100		df-pr 4582	. . . . . . . . . . . 12 ⊢ {∅, 1o} = ({∅} ∪ {1o})
101		df2o3 8405	. . . . . . . . . . . 12 ⊢ 2o = {∅, 1o}
102		imaundi 6106	. . . . . . . . . . . . 13 ⊢ ( bday “ ({ 0s } ∪ { 1s })) = (( bday “ { 0s }) ∪ ( bday “ { 1s }))
103		bdayfn 27747	. . . . . . . . . . . . . . . 16 ⊢ bday Fn No
104		fnsnfv 6912	. . . . . . . . . . . . . . . 16 ⊢ (( bday Fn No ∧ 0s ∈ No ) → {( bday ‘ 0s )} = ( bday “ { 0s }))
105	103, 62, 104	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ {( bday ‘ 0s )} = ( bday “ { 0s })
106	85	sneqi 4590	. . . . . . . . . . . . . . 15 ⊢ {( bday ‘ 0s )} = {∅}
107	105, 106	eqtr3i 2760	. . . . . . . . . . . . . 14 ⊢ ( bday “ { 0s }) = {∅}
108		fnsnfv 6912	. . . . . . . . . . . . . . . 16 ⊢ (( bday Fn No ∧ 1s ∈ No ) → {( bday ‘ 1s )} = ( bday “ { 1s }))
109	103, 2, 108	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ {( bday ‘ 1s )} = ( bday “ { 1s })
110	15	sneqi 4590	. . . . . . . . . . . . . . 15 ⊢ {( bday ‘ 1s )} = {1o}
111	109, 110	eqtr3i 2760	. . . . . . . . . . . . . 14 ⊢ ( bday “ { 1s }) = {1o}
112	107, 111	uneq12i 4117	. . . . . . . . . . . . 13 ⊢ (( bday “ { 0s }) ∪ ( bday “ { 1s })) = ({∅} ∪ {1o})
113	102, 112	eqtri 2758	. . . . . . . . . . . 12 ⊢ ( bday “ ({ 0s } ∪ { 1s })) = ({∅} ∪ {1o})
114	100, 101, 113	3eqtr4ri 2769	. . . . . . . . . . 11 ⊢ ( bday “ ({ 0s } ∪ { 1s })) = 2o
115		ssid 3955	. . . . . . . . . . 11 ⊢ 2o ⊆ 2o
116	114, 115	eqsstri 3979	. . . . . . . . . 10 ⊢ ( bday “ ({ 0s } ∪ { 1s })) ⊆ 2o
117		scutbdaybnd 27791	. . . . . . . . . 10 ⊢ (({ 0s } <<s { 1s } ∧ 2o ∈ On ∧ ( bday “ ({ 0s } ∪ { 1s })) ⊆ 2o) → ( bday ‘({ 0s } |s { 1s })) ⊆ 2o)
118	98, 99, 116, 117	mp3an 1464	. . . . . . . . 9 ⊢ ( bday ‘({ 0s } |s { 1s })) ⊆ 2o
119	92, 118	eqsstrdi 3977	. . . . . . . 8 ⊢ (𝑎 = 1s → ( bday ‘(𝑎 /su 2s)) ⊆ 2o)
120	88, 119	jaoi 858	. . . . . . 7 ⊢ ((𝑎 = 0s ∨ 𝑎 = 1s ) → ( bday ‘(𝑎 /su 2s)) ⊆ 2o)
121	76, 120	biimtrdi 253	. . . . . 6 ⊢ (𝑎 ∈ ℕ0s → (𝑎 <s 2s → ( bday ‘(𝑎 /su 2s)) ⊆ 2o))
122	121	rgen 3052	. . . . 5 ⊢ ∀𝑎 ∈ ℕ0s (𝑎 <s 2s → ( bday ‘(𝑎 /su 2s)) ⊆ 2o)
123		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑛 ∈ ℕ0s
124		nfra1 3259	. . . . . . . 8 ⊢ Ⅎ𝑎∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))
125	123, 124	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑎(𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s ))))
126		n0seo 28398	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ0s → (∃𝑥 ∈ ℕ0s 𝑎 = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑎 = ((2s ·s 𝑥) +s 1s )))
127		breq1 5100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → (𝑎 <s (2s↑s(𝑛 +s 1s )) ↔ 𝑥 <s (2s↑s(𝑛 +s 1s ))))
128		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) = ( bday ‘(𝑥 /su (2s↑s(𝑛 +s 1s )))))
129	128	sseq1d 3964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → (( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )) ↔ ( bday ‘(𝑥 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s ))))
130	127, 129	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑥 → ((𝑎 <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 3572	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑎 ∈ ℕ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 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ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 418	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 6398	. . . . . . . . . . . . . . 15 ⊢ suc ( bday ‘(𝑛 +s 1s )) ⊆ suc suc ( bday ‘(𝑛 +s 1s ))
135	133, 134	sstrdi 3945	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → 𝑛 ∈ ℕ0s)
137		peano2n0s 28309	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ0s → (𝑛 +s 1s ) ∈ ℕ0s)
138	136, 137	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → (𝑛 +s 1s ) ∈ ℕ0s)
139	138	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 28346	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 +s 1s ) ∈ ℕ0s → ( bday ‘((𝑛 +s 1s ) +s 1s )) = suc ( bday ‘(𝑛 +s 1s )))
141	139, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 6383	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 3970	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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 456	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ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 28406	. . . . . . . . . . . . . . . 16 ⊢ ((2s ∈ No ∧ (𝑛 +s 1s ) ∈ ℕ0s) → (2s↑s((𝑛 +s 1s ) +s 1s )) = ((2s↑s(𝑛 +s 1s )) ·s 2s))
146	7, 138, 145	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 28408	. . . . . . . . . . . . . . . . 17 ⊢ ((2s ∈ No ∧ (𝑛 +s 1s ) ∈ ℕ0s) → (2s↑s(𝑛 +s 1s )) ∈ No )
148	7, 138, 147	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → 2s ∈ No )
150	148, 149	mulscomd 28120	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 2770	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 5109	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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		n0sno 28302	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ0s → 𝑥 ∈ No )
154	153	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → 𝑥 ∈ No )
155		2nns 28395	. . . . . . . . . . . . . . . 16 ⊢ 2s ∈ ℕs
156		nnsgt0 28317	. . . . . . . . . . . . . . . 16 ⊢ (2s ∈ ℕs → 0s <s 2s)
157	155, 156	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 0s <s 2s
158	157	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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	sltmul2d 28152	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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 282	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ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 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 28421	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 6837	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 3964	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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 223	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ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 294	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ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 5100	. . . . . . . . . . . 12 ⊢ (𝑎 = (2s ·s 𝑥) → (𝑎 <s (2s↑s((𝑛 +s 1s ) +s 1s )) ↔ (2s ·s 𝑥) <s (2s↑s((𝑛 +s 1s ) +s 1s ))))
168		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (2s ·s 𝑥) → 𝑎 = (2s ·s 𝑥))
169	9	oveq1i 7368	. . . . . . . . . . . . . . . 16 ⊢ ((2s↑s 1s ) ·s 𝑥) = (2s ·s 𝑥)
170	168, 169	eqtr4di 2788	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (2s ·s 𝑥) → 𝑎 = ((2s↑s 1s ) ·s 𝑥))
171	170	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (2s ·s 𝑥) → (𝑎 /su (2s↑s((𝑛 +s 1s ) +s 1s ))) = (((2s↑s 1s ) ·s 𝑥) /su (2s↑s((𝑛 +s 1s ) +s 1s ))))
172	171	fveq2d 6837	. . . . . . . . . . . . 13 ⊢ (𝑎 = (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 3964	. . . . . . . . . . . 12 ⊢ (𝑎 = (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 344	. . . . . . . . . . 11 ⊢ (𝑎 = (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 247	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ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 3136	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ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 28366	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ0s → 𝑥 ∈ ℤs)
178	177	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → 𝑥 ∈ ℤs)
179	178	adantrr 718	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ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 28360	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 28416	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 28368	. . . . . . . . . . . . . . . . . . 19 ⊢ 1s ∈ ℤs
184	183	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ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 28372	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ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 28360	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 28416	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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	sltp1d 27995	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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	pw2sltdiv1d 28429	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 232	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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	ssltsn 27768	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 6106	. . . . . . . . . . . . . . 15 ⊢ ( 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 6912	. . . . . . . . . . . . . . . . . 18 ⊢ (( 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 588	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ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 7365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑥 → (𝑎 /su (2s↑s(𝑛 +s 1s ))) = (𝑥 /su (2s↑s(𝑛 +s 1s ))))
196	195	fveq2d 6837	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑥 → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) = ( bday ‘(𝑥 /su (2s↑s(𝑛 +s 1s )))))
197	196	sseq1d 3964	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑥 → (( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )) ↔ ( bday ‘(𝑥 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s ))))
198	127, 197	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑥 → ((𝑎 <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 3572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑎 ∈ ℕ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 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑎 ∈ ℕ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 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ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 718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 27960	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 27960	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 28309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ ℕ0s → (𝑥 +s 1s ) ∈ ℕ0s)
208	207	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → (𝑥 +s 1s ) ∈ ℕ0s)
209	208	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ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	n0snod 28304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 27960	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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	sleadd1d 27975	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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	sltp1d 27995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ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	slelttrd 27735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ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	sltled 27743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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	sleadd2d 27976	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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	sletrd 27736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ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 718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 28120	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 28394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2s↑s(𝑛 +s 1s )) ∈ No → (2s ·s (2s↑s(𝑛 +s 1s ))) = ((2s↑s(𝑛 +s 1s )) +s (2s↑s(𝑛 +s 1s ))))
226	203, 225	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 2774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ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 28394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ No → (2s ·s 𝑥) = (𝑥 +s 𝑥))
229	205, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 7373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ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 27986	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ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 2770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ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 5129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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 456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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		slenlt 27722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2s↑s(𝑛 +s 1s )) ∈ No ∧ 𝑥 ∈ No ) → ((2s↑s(𝑛 +s 1s )) ≤s 𝑥 ↔ ¬ 𝑥 <s (2s↑s(𝑛 +s 1s ))))
237	148, 154, 236	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 28309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 +s 1s ) ∈ ℕ0s → ((𝑛 +s 1s ) +s 1s ) ∈ ℕ0s)
239	138, 238	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ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 28408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2s ∈ No ∧ ((𝑛 +s 1s ) +s 1s ) ∈ ℕ0s) → (2s↑s((𝑛 +s 1s ) +s 1s )) ∈ No )
241	7, 239, 240	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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 28306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2s ∈ ℕs → 2s ∈ ℕ0s)
243	155, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2s ∈ ℕ0s
244		n0mulscl 28323	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2s ∈ ℕ0s ∧ 𝑥 ∈ ℕ0s) → (2s ·s 𝑥) ∈ ℕ0s)
245	243, 244	mpan 691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ℕ0s → (2s ·s 𝑥) ∈ ℕ0s)
246	245	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → (2s ·s 𝑥) ∈ ℕ0s)
247		n0addscl 28322	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((2s ·s 𝑥) ∈ ℕ0s ∧ 1s ∈ ℕ0s) → ((2s ·s 𝑥) +s 1s ) ∈ ℕ0s)
248	246, 53, 247	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ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	n0snod 28304	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → ((2s ·s 𝑥) +s 1s ) ∈ No )
250		slenlt 27722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((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 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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 454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ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 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 <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 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ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		bdayelon 27750	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( bday ‘(𝑥 /su (2s↑s(𝑛 +s 1s )))) ∈ On
258		bdayelon 27750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( bday ‘(𝑛 +s 1s )) ∈ On
259	258	onsuci 7781	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc ( bday ‘(𝑛 +s 1s )) ∈ On
260		onsssuc 6408	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( 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 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (( 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 218	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ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 4764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ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 3968	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 5109	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ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 28409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2s ∈ ℕ0s ∧ (𝑛 +s 1s ) ∈ ℕ0s) → (2s↑s(𝑛 +s 1s )) ∈ ℕ0s)
267	243, 138, 266	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 28323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2s ∈ ℕ0s ∧ (2s↑s(𝑛 +s 1s )) ∈ ℕ0s) → (2s ·s (2s↑s(𝑛 +s 1s ))) ∈ ℕ0s)
269	243, 267, 268	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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		n0sltp1le 28342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((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 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ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 28115	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ0s ∧ ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑛 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) ⊆ suc ( bday ‘(𝑛 +s 1s )))) ∧ 𝑥 ∈ ℕ0s) → (2s ·s 𝑥) ∈ No )
273	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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 27986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 28093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2s ∈ No → (2s ·s 1s ) = 2s)
276	7, 275	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2s ·s 1s ) = 2s
277	276	eqcomi 2744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2s = (2s ·s 1s )
278	56, 277	eqtri 2758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ( 1s +s 1s ) = (2s ·s 1s )
279	278	oveq2i 7369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2s ·s 𝑥) +s ( 1s +s 1s )) = ((2s ·s 𝑥) +s (2s ·s 1s ))
280	149, 154, 273	addsdid 28136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ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 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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 2782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 2770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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	n0snod 28304	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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	slemul2d 28154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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 279	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ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 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ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 279	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ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		sleloe 27724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 +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 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ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 28416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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 718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 6912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (( 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 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 5100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (𝑥 +s 1s ) → (𝑎 <s (2s↑s(𝑛 +s 1s )) ↔ (𝑥 +s 1s ) <s (2s↑s(𝑛 +s 1s ))))
298		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (𝑥 +s 1s ) → ( bday ‘(𝑎 /su (2s↑s(𝑛 +s 1s )))) = ( bday ‘((𝑥 +s 1s ) /su (2s↑s(𝑛 +s 1s )))))
299	298	sseq1d 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (𝑥 +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 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑥 +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 3572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑎 ∈ ℕ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 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑎 ∈ ℕ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 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ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 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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		bdayelon 27750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ( bday ‘((𝑥 +s 1s ) /su (2s↑s(𝑛 +s 1s )))) ∈ On
306		onsssuc 6408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 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 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (( 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 218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 4764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 3968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ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 28433	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ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 4591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ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 6018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 8397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1o = suc ∅
316	15, 315	eqtri 2758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ( bday ‘ 1s ) = suc ∅
317		0ss 4351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ⊆ ( bday ‘(𝑛 +s 1s ))
318		ord0 6370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Ord ∅
319	258	onordi 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Ord ( bday ‘(𝑛 +s 1s ))
320		ordsucsssuc 7765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Ord ∅ ∧ Ord ( bday ‘(𝑛 +s 1s ))) → (∅ ⊆ ( bday ‘(𝑛 +s 1s )) ↔ suc ∅ ⊆ suc ( bday ‘(𝑛 +s 1s ))))
321	318, 319, 320	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∅ ⊆ ( bday ‘(𝑛 +s 1s )) ↔ suc ∅ ⊆ suc ( bday ‘(𝑛 +s 1s )))
322	317, 321	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ suc ∅ ⊆ suc ( bday ‘(𝑛 +s 1s ))
323	316, 322	eqsstri 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ( bday ‘ 1s ) ⊆ suc ( bday ‘(𝑛 +s 1s ))
324		bdayelon 27750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ( bday ‘ 1s ) ∈ On
325		onsssuc 6408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((( 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 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( bday ‘ 1s ) ⊆ suc ( bday ‘(𝑛 +s 1s )) ↔ ( bday ‘ 1s ) ∈ suc suc ( bday ‘(𝑛 +s 1s )))
327	323, 326	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ( bday ‘ 1s ) ∈ suc suc ( bday ‘(𝑛 +s 1s ))
328	327	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ℕ0s → ( bday ‘ 1s ) ∈ suc suc ( bday ‘(𝑛 +s 1s )))
329	328	snssd 4764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℕ0s → {( bday ‘ 1s )} ⊆ suc suc ( bday ‘(𝑛 +s 1s )))
330	109, 329	eqsstrrid 3972	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ℕ0s → ( bday “ { 1s }) ⊆ suc suc ( bday ‘(𝑛 +s 1s )))
331	330	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ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 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ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 3967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ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 7365	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 +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 4591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 +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 6018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 +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 3964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 +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 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ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 860	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ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 240	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ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 240	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ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 454	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ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 4143	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 3971	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 7781	. . . . . . . . . . . . . . 15 ⊢ suc suc ( bday ‘(𝑛 +s 1s )) ∈ On
346		scutbdaybnd 27791	. . . . . . . . . . . . . . 15 ⊢ (({(𝑥 /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 1452	. . . . . . . . . . . . . 14 ⊢ (({(𝑥 /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 585	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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 28438	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 6837	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ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 6383	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ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 2741	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ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 3987	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ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 456	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ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 5100	. . . . . . . . . . . 12 ⊢ (𝑎 = ((2s ·s 𝑥) +s 1s ) → (𝑎 <s (2s↑s((𝑛 +s 1s ) +s 1s )) ↔ ((2s ·s 𝑥) +s 1s ) <s (2s↑s((𝑛 +s 1s ) +s 1s ))))
357		oveq1 7365	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((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 6837	. . . . . . . . . . . . 13 ⊢ (𝑎 = ((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 3964	. . . . . . . . . . . 12 ⊢ (𝑎 = ((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 344	. . . . . . . . . . 11 ⊢ (𝑎 = ((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 247	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ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 3136	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ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 860	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ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 34	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ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 3233	. . . . . 6 ⊢ ((𝑛 ∈ ℕ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 412	. . . . 5 ⊢ (𝑛 ∈ ℕ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 28311	. . . 4 ⊢ (𝑁 ∈ ℕ0s → ∀𝑎 ∈ ℕ0s (𝑎 <s (2s↑s(𝑁 +s 1s )) → ( bday ‘(𝑎 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s ))))
368		breq1 5100	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑎 <s (2s↑s(𝑁 +s 1s )) ↔ 𝐴 <s (2s↑s(𝑁 +s 1s ))))
369		oveq1 7365	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑎 /su (2s↑s(𝑁 +s 1s ))) = (𝐴 /su (2s↑s(𝑁 +s 1s ))))
370	369	fveq2d 6837	. . . . . . 7 ⊢ (𝑎 = 𝐴 → ( bday ‘(𝑎 /su (2s↑s(𝑁 +s 1s )))) = ( bday ‘(𝐴 /su (2s↑s(𝑁 +s 1s )))))
371	370	sseq1d 3964	. . . . . 6 ⊢ (𝑎 = 𝐴 → (( bday ‘(𝑎 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s )) ↔ ( bday ‘(𝐴 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s ))))
372	368, 371	imbi12d 344	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑎 <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 3572	. . . 4 ⊢ (∀𝑎 ∈ ℕ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 17	. . 3 ⊢ (𝑁 ∈ ℕ0s → (𝐴 ∈ ℕ0s → (𝐴 <s (2s↑s(𝑁 +s 1s )) → ( bday ‘(𝐴 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s )))))
375	374	com12 32	. 2 ⊢ (𝐴 ∈ ℕ0s → (𝑁 ∈ ℕ0s → (𝐴 <s (2s↑s(𝑁 +s 1s )) → ( bday ‘(𝐴 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s )))))
376	375	3imp 1111	1 ⊢ ((𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s (2s↑s(𝑁 +s 1s ))) → ( bday ‘(𝐴 /su (2s↑s(𝑁 +s 1s )))) ⊆ suc ( bday ‘(𝑁 +s 1s )))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114  ∀wral 3050  ∃wrex 3059   ∪ cun 3898   ⊆ wss 3900  ∅c0 4284  {csn 4579  {cpr 4581   class class class wbr 5097   “ cima 5626  Ord word 6315  Oncon0 6316  suc csuc 6318   Fn wfn 6486  ‘cfv 6491  (class class class)co 7358  1_oc1o 8390  2_oc2o 8391   No csur 27609   <s cslt 27610   bday cbday 27611   ≤s csle 27714   <<s csslt 27755   |s cscut 27757   0_s c0s 27801   1_s c1s 27802   +_s cadds 27939   ·_s cmuls 28086   /_su cdivs 28167  ℕ_0scnn0s 28291  ℕ_scnns 28292  ℤ_sczs 28355  2_sc2s 28387  ↑_scexps 28389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-rep 5223  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-dc 10358

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3349  df-reu 3350  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-ot 4588  df-uni 4863  df-int 4902  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6258  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-oadd 8401  df-nadd 8594  df-no 27612  df-slt 27613  df-bday 27614  df-sle 27715  df-sslt 27756  df-scut 27758  df-0s 27803  df-1s 27804  df-made 27823  df-old 27824  df-left 27826  df-right 27827  df-norec 27918  df-norec2 27929  df-adds 27940  df-negs 28001  df-subs 28002  df-muls 28087  df-divs 28168  df-ons 28231  df-seqs 28263  df-n0s 28293  df-nns 28294  df-zs 28356  df-2s 28388  df-exps 28390

This theorem is referenced by:  bdaypw2n0sbnd  28441