Theorem pw2cut

Description: Extend halfcut to arbitrary powers of two. Part of theorem 4.2 of Gonshor p. 28. (Contributed by Scott Fenton, 18-Aug-2025)

	Ref	Expression
Hypotheses	pw2cut.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2cut.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	pw2cut.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
	pw2cut.4	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
	pw2cut.5	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) = ( 𝐴 +s 𝐵 ) )
Assertion	pw2cut	⊢ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pw2cut.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2cut.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		pw2cut.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
4		pw2cut.4	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
5		pw2cut.5	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) = ( 𝐴 +s 𝐵 ) )
6		oveq2	⊢ ( 𝑥 = 0s → ( 2s ↑s 𝑥 ) = ( 2s ↑s 0s ) )
7		2no	⊢ 2s ∈ No
8		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
9	7 8	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
10	6 9	eqtrdi	⊢ ( 𝑥 = 0s → ( 2s ↑s 𝑥 ) = 1s )
11	10	oveq2d	⊢ ( 𝑥 = 0s → ( 𝐴 /su ( 2s ↑s 𝑥 ) ) = ( 𝐴 /su 1s ) )
12	11	sneqd	⊢ ( 𝑥 = 0s → { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐴 /su 1s ) } )
13	10	oveq2d	⊢ ( 𝑥 = 0s → ( 𝐵 /su ( 2s ↑s 𝑥 ) ) = ( 𝐵 /su 1s ) )
14	13	sneqd	⊢ ( 𝑥 = 0s → { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐵 /su 1s ) } )
15	12 14	oveq12d	⊢ ( 𝑥 = 0s → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) )
16		oveq1	⊢ ( 𝑥 = 0s → ( 𝑥 +s 1s ) = ( 0s +s 1s ) )
17		1no	⊢ 1s ∈ No
18		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
19	17 18	ax-mp	⊢ ( 0s +s 1s ) = 1s
20	16 19	eqtrdi	⊢ ( 𝑥 = 0s → ( 𝑥 +s 1s ) = 1s )
21	20	oveq2d	⊢ ( 𝑥 = 0s → ( 2s ↑s ( 𝑥 +s 1s ) ) = ( 2s ↑s 1s ) )
22		exps1	⊢ ( 2s ∈ No → ( 2s ↑s 1s ) = 2s )
23	7 22	ax-mp	⊢ ( 2s ↑s 1s ) = 2s
24	21 23	eqtrdi	⊢ ( 𝑥 = 0s → ( 2s ↑s ( 𝑥 +s 1s ) ) = 2s )
25	24	oveq2d	⊢ ( 𝑥 = 0s → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) )
26	15 25	eqeq12d	⊢ ( 𝑥 = 0s → ( ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ↔ ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) ) )
27	26	imbi2d	⊢ ( 𝑥 = 0s → ( ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ↔ ( 𝜑 → ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) ) ) )
28		oveq2	⊢ ( 𝑥 = 𝑦 → ( 2s ↑s 𝑥 ) = ( 2s ↑s 𝑦 ) )
29	28	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 /su ( 2s ↑s 𝑥 ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
30	29	sneqd	⊢ ( 𝑥 = 𝑦 → { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } )
31	28	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 /su ( 2s ↑s 𝑥 ) ) = ( 𝐵 /su ( 2s ↑s 𝑦 ) ) )
32	31	sneqd	⊢ ( 𝑥 = 𝑦 → { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } )
33	30 32	oveq12d	⊢ ( 𝑥 = 𝑦 → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) )
34		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 +s 1s ) = ( 𝑦 +s 1s ) )
35	34	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 2s ↑s ( 𝑥 +s 1s ) ) = ( 2s ↑s ( 𝑦 +s 1s ) ) )
36	35	oveq2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) )
37	33 36	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ↔ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) )
38	37	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ↔ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) ) )
39		oveq2	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 2s ↑s 𝑥 ) = ( 2s ↑s ( 𝑦 +s 1s ) ) )
40	39	oveq2d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝐴 /su ( 2s ↑s 𝑥 ) ) = ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) )
41	40	sneqd	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } )
42	39	oveq2d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝐵 /su ( 2s ↑s 𝑥 ) ) = ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) )
43	42	sneqd	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } )
44	41 43	oveq12d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) )
45		oveq1	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑥 +s 1s ) = ( ( 𝑦 +s 1s ) +s 1s ) )
46	45	oveq2d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 2s ↑s ( 𝑥 +s 1s ) ) = ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) )
47	46	oveq2d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) )
48	44 47	eqeq12d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ↔ ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) ) )
49	48	imbi2d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ↔ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) ) ) )
50		oveq2	⊢ ( 𝑥 = 𝑁 → ( 2s ↑s 𝑥 ) = ( 2s ↑s 𝑁 ) )
51	50	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝐴 /su ( 2s ↑s 𝑥 ) ) = ( 𝐴 /su ( 2s ↑s 𝑁 ) ) )
52	51	sneqd	⊢ ( 𝑥 = 𝑁 → { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } )
53	50	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝐵 /su ( 2s ↑s 𝑥 ) ) = ( 𝐵 /su ( 2s ↑s 𝑁 ) ) )
54	53	sneqd	⊢ ( 𝑥 = 𝑁 → { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } = { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } )
55	52 54	oveq12d	⊢ ( 𝑥 = 𝑁 → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) )
56		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 +s 1s ) = ( 𝑁 +s 1s ) )
57	56	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 2s ↑s ( 𝑥 +s 1s ) ) = ( 2s ↑s ( 𝑁 +s 1s ) ) )
58	57	oveq2d	⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
59	55 58	eqeq12d	⊢ ( 𝑥 = 𝑁 → ( ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ↔ ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) )
60	59	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑥 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑥 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ↔ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) ) )
61	1	divs1d	⊢ ( 𝜑 → ( 𝐴 /su 1s ) = 𝐴 )
62	61	sneqd	⊢ ( 𝜑 → { ( 𝐴 /su 1s ) } = { 𝐴 } )
63	2	divs1d	⊢ ( 𝜑 → ( 𝐵 /su 1s ) = 𝐵 )
64	63	sneqd	⊢ ( 𝜑 → { ( 𝐵 /su 1s ) } = { 𝐵 } )
65	62 64	oveq12d	⊢ ( 𝜑 → ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) = ( { 𝐴 } |s { 𝐵 } ) )
66		eqid	⊢ ( { 𝐴 } |s { 𝐵 } ) = ( { 𝐴 } |s { 𝐵 } )
67	1 2 4 5 66	halfcut	⊢ ( 𝜑 → ( { 𝐴 } |s { 𝐵 } ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) )
68	65 67	eqtrd	⊢ ( 𝜑 → ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) )
69	1	adantl	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝐴 ∈ No )
70		peano2n0s	⊢ ( 𝑦 ∈ ℕ0s → ( 𝑦 +s 1s ) ∈ ℕ0s )
71		expscl	⊢ ( ( 2s ∈ No ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ∈ No )
72	7 70 71	sylancr	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) ∈ No )
73	72	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ∈ No )
74		2ne0s	⊢ 2s ≠ 0s
75		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
76	7 74 75	mp3an12	⊢ ( ( 𝑦 +s 1s ) ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
77	70 76	syl	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
78	77	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
79	69 73 78	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
80	79	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
81	2	adantl	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝐵 ∈ No )
82	81 73 78	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
83	82	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
84	69 73 78	divscan1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ·s ( 2s ↑s ( 𝑦 +s 1s ) ) ) = 𝐴 )
85	4	adantl	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝐴 <s 𝐵 )
86	84 85	eqbrtrd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ·s ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s 𝐵 )
87		2nns	⊢ 2s ∈ ℕs
88		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
89	87 88	ax-mp	⊢ 0s <s 2s
90		expsgt0	⊢ ( ( 2s ∈ No ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
91	7 89 90	mp3an13	⊢ ( ( 𝑦 +s 1s ) ∈ ℕ0s → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
92	70 91	syl	⊢ ( 𝑦 ∈ ℕ0s → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
93	92	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
94	79 81 73 93	ltmuldivsd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ·s ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s 𝐵 ↔ ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) )
95	86 94	mpbid	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) )
96	95	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) )
97		expsp1	⊢ ( ( 2s ∈ No ∧ 𝑦 ∈ ℕ0s ) → ( 2s ↑s ( 𝑦 +s 1s ) ) = ( ( 2s ↑s 𝑦 ) ·s 2s ) )
98	7 97	mpan	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) = ( ( 2s ↑s 𝑦 ) ·s 2s ) )
99	98	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( 𝑦 +s 1s ) ) = ( ( 2s ↑s 𝑦 ) ·s 2s ) )
100	99	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( 𝐴 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
101		expscl	⊢ ( ( 2s ∈ No ∧ 𝑦 ∈ ℕ0s ) → ( 2s ↑s 𝑦 ) ∈ No )
102	7 101	mpan	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s 𝑦 ) ∈ No )
103	102	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s 𝑦 ) ∈ No )
104	7	a1i	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 2s ∈ No )
105		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑦 ∈ ℕ0s ) → ( 2s ↑s 𝑦 ) ≠ 0s )
106	7 74 105	mp3an12	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s 𝑦 ) ≠ 0s )
107	106	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s 𝑦 ) ≠ 0s )
108	74	a1i	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 2s ≠ 0s )
109	69 103 104 107 108	divdivs1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) = ( 𝐴 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
110	100 109	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) )
111	110	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 2s ·s ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) )
112	69 103 107	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s 𝑦 ) ) ∈ No )
113	112 104 108	divscan2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
114	111 113	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
115	114	sneqd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } = { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } )
116	99	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( 𝐵 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
117	81 103 104 107 108	divdivs1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) = ( 𝐵 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
118	116 117	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) )
119	118	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 2s ·s ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) )
120	81 103 107	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s 𝑦 ) ) ∈ No )
121	120 104 108	divscan2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) = ( 𝐵 /su ( 2s ↑s 𝑦 ) ) )
122	119 121	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 𝐵 /su ( 2s ↑s 𝑦 ) ) )
123	122	sneqd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } = { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } )
124	115 123	oveq12d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } |s { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) )
125	124	eqcomd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } |s { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } ) )
126	69 81 73 78	divsdird	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) )
127	125 126	eqeq12d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ↔ ( { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } |s { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } ) = ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) ) )
128	127	biimp3a	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } |s { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } ) = ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) )
129		eqid	⊢ ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } )
130	80 83 96 128 129	halfcut	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) /su 2s ) )
131	126	oveq1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) = ( ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) /su 2s ) )
132	131	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) = ( ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) /su 2s ) )
133	130 132	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) )
134		expsp1	⊢ ( ( 2s ∈ No ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) )
135	7 70 134	sylancr	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) )
136	135	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) )
137	136	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) = ( ( 𝐴 +s 𝐵 ) /su ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) ) )
138	69 81	addscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 +s 𝐵 ) ∈ No )
139	138 73 104 78 108	divdivs1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) = ( ( 𝐴 +s 𝐵 ) /su ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) ) )
140	137 139	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) = ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) )
141	140	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) = ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) )
142	133 141	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) )
143	142	3exp	⊢ ( 𝑦 ∈ ℕ0s → ( 𝜑 → ( ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) → ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) ) ) )
144	143	a2d	⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) ) ) )
145	27 38 49 60 68 144	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) )
146	3 145	mpcom	⊢ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )