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		2sno	⊢ 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		1sno	⊢ 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		divs1	⊢ ( 𝐴 ∈ No → ( 𝐴 /su 1s ) = 𝐴 )
62	1 61	syl	⊢ ( 𝜑 → ( 𝐴 /su 1s ) = 𝐴 )
63	62	sneqd	⊢ ( 𝜑 → { ( 𝐴 /su 1s ) } = { 𝐴 } )
64		divs1	⊢ ( 𝐵 ∈ No → ( 𝐵 /su 1s ) = 𝐵 )
65	2 64	syl	⊢ ( 𝜑 → ( 𝐵 /su 1s ) = 𝐵 )
66	65	sneqd	⊢ ( 𝜑 → { ( 𝐵 /su 1s ) } = { 𝐵 } )
67	63 66	oveq12d	⊢ ( 𝜑 → ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) = ( { 𝐴 } |s { 𝐵 } ) )
68		eqid	⊢ ( { 𝐴 } |s { 𝐵 } ) = ( { 𝐴 } |s { 𝐵 } )
69	1 2 4 5 68	halfcut	⊢ ( 𝜑 → ( { 𝐴 } |s { 𝐵 } ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) )
70	67 69	eqtrd	⊢ ( 𝜑 → ( { ( 𝐴 /su 1s ) } |s { ( 𝐵 /su 1s ) } ) = ( ( 𝐴 +s 𝐵 ) /su 2s ) )
71	1	adantl	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝐴 ∈ No )
72		peano2n0s	⊢ ( 𝑦 ∈ ℕ0s → ( 𝑦 +s 1s ) ∈ ℕ0s )
73		expscl	⊢ ( ( 2s ∈ No ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ∈ No )
74	7 72 73	sylancr	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) ∈ No )
75	74	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ∈ No )
76		2ne0s	⊢ 2s ≠ 0s
77		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
78	7 76 77	mp3an12	⊢ ( ( 𝑦 +s 1s ) ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
79	72 78	syl	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
80	79	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( 𝑦 +s 1s ) ) ≠ 0s )
81	71 75 80	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
82	81	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
83	2	adantl	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝐵 ∈ No )
84	83 75 80	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
85	84	3adant3	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ∧ ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ∈ No )
86	71 75 80	divscan1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ·s ( 2s ↑s ( 𝑦 +s 1s ) ) ) = 𝐴 )
87	4	adantl	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝐴 <s 𝐵 )
88	86 87	eqbrtrd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ·s ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s 𝐵 )
89		2nns	⊢ 2s ∈ ℕs
90		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
91	89 90	ax-mp	⊢ 0s <s 2s
92		expsgt0	⊢ ( ( 2s ∈ No ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
93	7 91 92	mp3an13	⊢ ( ( 𝑦 +s 1s ) ∈ ℕ0s → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
94	72 93	syl	⊢ ( 𝑦 ∈ ℕ0s → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
95	94	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 0s <s ( 2s ↑s ( 𝑦 +s 1s ) ) )
96	81 83 75 95	sltmuldivd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ·s ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s 𝐵 ↔ ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) )
97	88 96	mpbid	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) <s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) )
98	97	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 ) ) ) )
99		expsp1	⊢ ( ( 2s ∈ No ∧ 𝑦 ∈ ℕ0s ) → ( 2s ↑s ( 𝑦 +s 1s ) ) = ( ( 2s ↑s 𝑦 ) ·s 2s ) )
100	7 99	mpan	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( 𝑦 +s 1s ) ) = ( ( 2s ↑s 𝑦 ) ·s 2s ) )
101	100	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( 𝑦 +s 1s ) ) = ( ( 2s ↑s 𝑦 ) ·s 2s ) )
102	101	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( 𝐴 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
103		expscl	⊢ ( ( 2s ∈ No ∧ 𝑦 ∈ ℕ0s ) → ( 2s ↑s 𝑦 ) ∈ No )
104	7 103	mpan	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s 𝑦 ) ∈ No )
105	104	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s 𝑦 ) ∈ No )
106	7	a1i	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 2s ∈ No )
107		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑦 ∈ ℕ0s ) → ( 2s ↑s 𝑦 ) ≠ 0s )
108	7 76 107	mp3an12	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s 𝑦 ) ≠ 0s )
109	108	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s 𝑦 ) ≠ 0s )
110	76	a1i	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 2s ≠ 0s )
111	71 105 106 109 110	divdivs1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) = ( 𝐴 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
112	102 111	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) )
113	112	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 2s ·s ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) )
114	71 105 109	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 /su ( 2s ↑s 𝑦 ) ) ∈ No )
115	114 106 110	divscan2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( ( 𝐴 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
116	113 115	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
117	116	sneqd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } = { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } )
118	101	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( 𝐵 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
119	83 105 106 109 110	divdivs1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) = ( 𝐵 /su ( ( 2s ↑s 𝑦 ) ·s 2s ) ) )
120	118 119	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) )
121	120	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 2s ·s ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) )
122	83 105 109	divscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐵 /su ( 2s ↑s 𝑦 ) ) ∈ No )
123	122 106 110	divscan2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( ( 𝐵 /su ( 2s ↑s 𝑦 ) ) /su 2s ) ) = ( 𝐵 /su ( 2s ↑s 𝑦 ) ) )
124	121 123	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) = ( 𝐵 /su ( 2s ↑s 𝑦 ) ) )
125	124	sneqd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } = { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } )
126	117 125	oveq12d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } |s { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) )
127	126	eqcomd	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( { ( 𝐴 /su ( 2s ↑s 𝑦 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑦 ) ) } ) = ( { ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } |s { ( 2s ·s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) } ) )
128	71 83 75 80	divsdird	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) = ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) )
129	127 128	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 ) ) ) ) ) )
130	129	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 ) ) ) ) )
131		eqid	⊢ ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } ) = ( { ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } |s { ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) } )
132	82 85 98 130 131	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 ) )
133	128	oveq1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) = ( ( ( 𝐴 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) +s ( 𝐵 /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) ) /su 2s ) )
134	133	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 ) )
135	132 134	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 ) )
136		expsp1	⊢ ( ( 2s ∈ No ∧ ( 𝑦 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) )
137	7 72 136	sylancr	⊢ ( 𝑦 ∈ ℕ0s → ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) )
138	137	adantr	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) = ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) )
139	138	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) = ( ( 𝐴 +s 𝐵 ) /su ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) ) )
140	71 83	addscld	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( 𝐴 +s 𝐵 ) ∈ No )
141	140 75 106 80 110	divdivs1d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) = ( ( 𝐴 +s 𝐵 ) /su ( ( 2s ↑s ( 𝑦 +s 1s ) ) ·s 2s ) ) )
142	139 141	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( ( 𝑦 +s 1s ) +s 1s ) ) ) = ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑦 +s 1s ) ) ) /su 2s ) )
143	142	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 ) )
144	135 143	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 ) ) ) )
145	144	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 ) ) ) ) ) )
146	145	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 ) ) ) ) ) )
147	27 38 49 60 70 146	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) ) )
148	3 147	mpcom	⊢ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( 𝐵 /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )