Theorem cutpw2

Description: A cut expression for inverses of powers of two. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	cutpw2	⊢ ( 𝑁 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑁 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑚 = 0s → ( 𝑚 +s 1s ) = ( 0s +s 1s ) )
2		1sno	⊢ 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		2sno	⊢ 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	oveq2d	⊢ ( 𝑚 = 0s → ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 1s /su 2s ) )
12		oveq2	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = ( 2s ↑s 0s ) )
13		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
14	7 13	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
15	12 14	eqtrdi	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = 1s )
16	15	oveq2d	⊢ ( 𝑚 = 0s → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su 1s ) )
17		divs1	⊢ ( 1s ∈ No → ( 1s /su 1s ) = 1s )
18	2 17	ax-mp	⊢ ( 1s /su 1s ) = 1s
19	16 18	eqtrdi	⊢ ( 𝑚 = 0s → ( 1s /su ( 2s ↑s 𝑚 ) ) = 1s )
20	19	sneqd	⊢ ( 𝑚 = 0s → { ( 1s /su ( 2s ↑s 𝑚 ) ) } = { 1s } )
21	20	oveq2d	⊢ ( 𝑚 = 0s → ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) = ( { 0s } |s { 1s } ) )
22	11 21	eqeq12d	⊢ ( 𝑚 = 0s → ( ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 1s /su 2s ) = ( { 0s } |s { 1s } ) ) )
23		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 +s 1s ) = ( 𝑛 +s 1s ) )
24	23	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
25	24	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
26		oveq2	⊢ ( 𝑚 = 𝑛 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑛 ) )
27	26	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su ( 2s ↑s 𝑛 ) ) )
28	27	sneqd	⊢ ( 𝑚 = 𝑛 → { ( 1s /su ( 2s ↑s 𝑚 ) ) } = { ( 1s /su ( 2s ↑s 𝑛 ) ) } )
29	28	oveq2d	⊢ ( 𝑚 = 𝑛 → ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
30	25 29	eqeq12d	⊢ ( 𝑚 = 𝑛 → ( ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) )
31		oveq1	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑚 +s 1s ) = ( ( 𝑛 +s 1s ) +s 1s ) )
32	31	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) )
33	32	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) )
34		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s 𝑚 ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
35	34	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
36	35	sneqd	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → { ( 1s /su ( 2s ↑s 𝑚 ) ) } = { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
37	36	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
38	33 37	eqeq12d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
39		oveq1	⊢ ( 𝑚 = 𝑁 → ( 𝑚 +s 1s ) = ( 𝑁 +s 1s ) )
40	39	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 2s ↑s ( 𝑚 +s 1s ) ) = ( 2s ↑s ( 𝑁 +s 1s ) ) )
41	40	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( 1s /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
42		oveq2	⊢ ( 𝑚 = 𝑁 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑁 ) )
43	42	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su ( 2s ↑s 𝑁 ) ) )
44	43	sneqd	⊢ ( 𝑚 = 𝑁 → { ( 1s /su ( 2s ↑s 𝑚 ) ) } = { ( 1s /su ( 2s ↑s 𝑁 ) ) } )
45	44	oveq2d	⊢ ( 𝑚 = 𝑁 → ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑁 ) ) } ) )
46	41 45	eqeq12d	⊢ ( 𝑚 = 𝑁 → ( ( 1s /su ( 2s ↑s ( 𝑚 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 1s /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑁 ) ) } ) ) )
47		nohalf	⊢ ( 1s /su 2s ) = ( { 0s } |s { 1s } )
48		peano2n0s	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) ∈ ℕ0s )
49		expsp1	⊢ ( ( 2s ∈ No ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) )
50	7 49	mpan	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) )
51	48 50	syl	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) )
52	51	oveq2d	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( 1s /su ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) ) )
53	2	a1i	⊢ ( 𝑛 ∈ ℕ0s → 1s ∈ No )
54		expscl	⊢ ( ( 2s ∈ No ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
55	7 54	mpan	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
56	48 55	syl	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
57	7	a1i	⊢ ( 𝑛 ∈ ℕ0s → 2s ∈ No )
58		2ne0s	⊢ 2s ≠ 0s
59		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ≠ 0s )
60	7 58 59	mp3an12	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) ≠ 0s )
61	48 60	syl	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) ≠ 0s )
62	58	a1i	⊢ ( 𝑛 ∈ ℕ0s → 2s ≠ 0s )
63	53 56 57 61 62	divdivs1d	⊢ ( 𝑛 ∈ ℕ0s → ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) /su 2s ) = ( 1s /su ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 2s ) ) )
64	52 63	eqtr4d	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) /su 2s ) )
65	53 56 61	divscld	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
66		addslid	⊢ ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No → ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
67	65 66	syl	⊢ ( 𝑛 ∈ ℕ0s → ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
68	67	oveq1d	⊢ ( 𝑛 ∈ ℕ0s → ( ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) /su 2s ) = ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) /su 2s ) )
69	64 68	eqtr4d	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) /su 2s ) )
70	69	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) /su 2s ) )
71		0sno	⊢ 0s ∈ No
72	71	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → 0s ∈ No )
73	2	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → 1s ∈ No )
74	56	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No )
75	61	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) ≠ 0s )
76	73 74 75	divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
77		muls02	⊢ ( ( 2s ↑s ( 𝑛 +s 1s ) ) ∈ No → ( 0s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) = 0s )
78	74 77	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 0s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) = 0s )
79		0slt1s	⊢ 0s <s 1s
80	78 79	eqbrtrdi	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 0s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s 1s )
81		2nns	⊢ 2s ∈ ℕs
82		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
83	81 82	ax-mp	⊢ 0s <s 2s
84		expsgt0	⊢ ( ( 2s ∈ No ∧ ( 𝑛 +s 1s ) ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s ( 𝑛 +s 1s ) ) )
85	7 83 84	mp3an13	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → 0s <s ( 2s ↑s ( 𝑛 +s 1s ) ) )
86	48 85	syl	⊢ ( 𝑛 ∈ ℕ0s → 0s <s ( 2s ↑s ( 𝑛 +s 1s ) ) )
87	86	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → 0s <s ( 2s ↑s ( 𝑛 +s 1s ) ) )
88	72 73 74 87	sltmuldivd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 0s ·s ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s 1s ↔ 0s <s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
89	80 88	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → 0s <s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
90		muls01	⊢ ( 2s ∈ No → ( 2s ·s 0s ) = 0s )
91	7 90	ax-mp	⊢ ( 2s ·s 0s ) = 0s
92	91	sneqi	⊢ { ( 2s ·s 0s ) } = { 0s }
93	92	a1i	⊢ ( 𝑛 ∈ ℕ0s → { ( 2s ·s 0s ) } = { 0s } )
94		expsp1	⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
95	7 94	mpan	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
96	95	oveq2d	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 1s /su ( ( 2s ↑s 𝑛 ) ·s 2s ) ) )
97		expscl	⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ∈ No )
98	7 97	mpan	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ∈ No )
99		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ≠ 0s )
100	7 58 99	mp3an12	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ≠ 0s )
101	53 98 57 100 62	divdivs1d	⊢ ( 𝑛 ∈ ℕ0s → ( ( 1s /su ( 2s ↑s 𝑛 ) ) /su 2s ) = ( 1s /su ( ( 2s ↑s 𝑛 ) ·s 2s ) ) )
102	96 101	eqtr4d	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 1s /su ( 2s ↑s 𝑛 ) ) /su 2s ) )
103	102	oveq2d	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ·s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 2s ·s ( ( 1s /su ( 2s ↑s 𝑛 ) ) /su 2s ) ) )
104	53 98 100	divscld	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s 𝑛 ) ) ∈ No )
105	104 57 62	divscan2d	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ·s ( ( 1s /su ( 2s ↑s 𝑛 ) ) /su 2s ) ) = ( 1s /su ( 2s ↑s 𝑛 ) ) )
106	103 105	eqtrd	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ·s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 1s /su ( 2s ↑s 𝑛 ) ) )
107	106	sneqd	⊢ ( 𝑛 ∈ ℕ0s → { ( 2s ·s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } = { ( 1s /su ( 2s ↑s 𝑛 ) ) } )
108	93 107	oveq12d	⊢ ( 𝑛 ∈ ℕ0s → ( { ( 2s ·s 0s ) } |s { ( 2s ·s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
109		eqcom	⊢ ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ↔ ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
110	109	biimpi	⊢ ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) → ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
111	108 110	sylan9eq	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( 2s ·s 0s ) } |s { ( 2s ·s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
112	76 66	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
113	111 112	eqtr4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( 2s ·s 0s ) } |s { ( 2s ·s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) } ) = ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
114		eqid	⊢ ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
115	72 76 89 113 114	halfcut	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) = ( ( 0s +s ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) /su 2s ) )
116	70 115	eqtr4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
117	116	ex	⊢ ( 𝑛 ∈ ℕ0s → ( ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) → ( 1s /su ( 2s ↑s ( ( 𝑛 +s 1s ) +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
118	22 30 38 46 47 117	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑁 ) ) } ) )