Theorem pw2cut2

Description: Cut expression for powers of two. Theorem 12 of Conway p. 12-13. (Contributed by Scott Fenton, 18-Jan-2026)

	Ref	Expression
Assertion	pw2cut2	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = ( 2s ↑s 0s ) )
2		2sno	⊢ 2s ∈ No
3		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
4	2 3	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
5	1 4	eqtrdi	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = 1s )
6	5	oveq2d	⊢ ( 𝑚 = 0s → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( 𝐴 /su 1s ) )
7	5	oveq2d	⊢ ( 𝑚 = 0s → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 -s 1s ) /su 1s ) )
8	7	sneqd	⊢ ( 𝑚 = 0s → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 -s 1s ) /su 1s ) } )
9	5	oveq2d	⊢ ( 𝑚 = 0s → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 +s 1s ) /su 1s ) )
10	9	sneqd	⊢ ( 𝑚 = 0s → { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 +s 1s ) /su 1s ) } )
11	8 10	oveq12d	⊢ ( 𝑚 = 0s → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) = ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) )
12	6 11	eqeq12d	⊢ ( 𝑚 = 0s → ( ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 𝐴 /su 1s ) = ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) ) )
13	12	imbi2d	⊢ ( 𝑚 = 0s → ( ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ) ↔ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) ) ) )
14		oveq2	⊢ ( 𝑚 = 𝑛 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑛 ) )
15	14	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
16	14	oveq2d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) )
17	16	sneqd	⊢ ( 𝑚 = 𝑛 → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
18	14	oveq2d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) )
19	18	sneqd	⊢ ( 𝑚 = 𝑛 → { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
20	17 19	oveq12d	⊢ ( 𝑚 = 𝑛 → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
21	15 20	eqeq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
22	21	imbi2d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ) ↔ ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ) )
23		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s 𝑚 ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
24	23	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
25	23	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
26	25	sneqd	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
27	23	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
28	27	sneqd	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
29	26 28	oveq12d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
30	24 29	eqeq12d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
31	30	imbi2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ) ↔ ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
32		oveq2	⊢ ( 𝑚 = 𝑁 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑁 ) )
33	32	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( 𝐴 /su ( 2s ↑s 𝑁 ) ) )
34	32	oveq2d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) )
35	34	sneqd	⊢ ( 𝑚 = 𝑁 → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } )
36	32	oveq2d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) )
37	36	sneqd	⊢ ( 𝑚 = 𝑁 → { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } = { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } )
38	35 37	oveq12d	⊢ ( 𝑚 = 𝑁 → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) )
39	33 38	eqeq12d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ↔ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) ) )
40	39	imbi2d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑚 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑚 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑚 ) ) } ) ) ↔ ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) ) ) )
41		zscut	⊢ ( 𝐴 ∈ ℤs → 𝐴 = ( { ( 𝐴 -s 1s ) } |s { ( 𝐴 +s 1s ) } ) )
42		zno	⊢ ( 𝐴 ∈ ℤs → 𝐴 ∈ No )
43		divs1	⊢ ( 𝐴 ∈ No → ( 𝐴 /su 1s ) = 𝐴 )
44	42 43	syl	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = 𝐴 )
45		1sno	⊢ 1s ∈ No
46	45	a1i	⊢ ( 𝐴 ∈ ℤs → 1s ∈ No )
47	42 46	subscld	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 -s 1s ) ∈ No )
48		divs1	⊢ ( ( 𝐴 -s 1s ) ∈ No → ( ( 𝐴 -s 1s ) /su 1s ) = ( 𝐴 -s 1s ) )
49	47 48	syl	⊢ ( 𝐴 ∈ ℤs → ( ( 𝐴 -s 1s ) /su 1s ) = ( 𝐴 -s 1s ) )
50	49	sneqd	⊢ ( 𝐴 ∈ ℤs → { ( ( 𝐴 -s 1s ) /su 1s ) } = { ( 𝐴 -s 1s ) } )
51	42 46	addscld	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 +s 1s ) ∈ No )
52		divs1	⊢ ( ( 𝐴 +s 1s ) ∈ No → ( ( 𝐴 +s 1s ) /su 1s ) = ( 𝐴 +s 1s ) )
53	51 52	syl	⊢ ( 𝐴 ∈ ℤs → ( ( 𝐴 +s 1s ) /su 1s ) = ( 𝐴 +s 1s ) )
54	53	sneqd	⊢ ( 𝐴 ∈ ℤs → { ( ( 𝐴 +s 1s ) /su 1s ) } = { ( 𝐴 +s 1s ) } )
55	50 54	oveq12d	⊢ ( 𝐴 ∈ ℤs → ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) = ( { ( 𝐴 -s 1s ) } |s { ( 𝐴 +s 1s ) } ) )
56	41 44 55	3eqtr4d	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) )
57		simp2	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝐴 ∈ ℤs )
58	57	znod	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝐴 ∈ No )
59	45	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 1s ∈ No )
60	58 59	subscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 -s 1s ) ∈ No )
61		simp1	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝑛 ∈ ℕ0s )
62		peano2n0s	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) ∈ ℕ0s )
63	61 62	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
64	60 63	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
65	58 59	addscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 +s 1s ) ∈ No )
66	65 63	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
67	58	sltm1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 -s 1s ) <s 𝐴 )
68	58	sltp1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝐴 <s ( 𝐴 +s 1s ) )
69	60 58 65 67 68	slttrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 -s 1s ) <s ( 𝐴 +s 1s ) )
70	60 65 63	pw2sltdiv1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) <s ( 𝐴 +s 1s ) ↔ ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
71	69 70	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
72	64 66 71	ssltsn	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
73	72	scutcld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ No )
74	64 73	addscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ∈ No )
75	66 73	addscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ∈ No )
76	64 66 73	sltadd1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
77	71 76	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
78	74 75 77	ssltsn	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
79	60 61	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No )
80	65 61	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No )
81	60 65 61	pw2sltdiv1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) <s ( 𝐴 +s 1s ) ↔ ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
82	69 81	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) )
83	79 80 82	ssltsn	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
84		eqidd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } |s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) = ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } |s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
85		simp3	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
86	58 61	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) ∈ No )
87		scutcut	⊢ ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ No ∧ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } ∧ { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
88	72 87	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ No ∧ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } ∧ { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
89	88	simp3d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
90		ovex	⊢ ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ V
91	90	snid	⊢ ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) }
92	91	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } )
93		ovex	⊢ ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ V
94	93	snid	⊢ ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) }
95	94	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
96	89 92 95	ssltsepcd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
97	73 66 64	sltadd2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ) )
98	96 97	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
99	58 58 59	addsassd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 𝐴 ) +s 1s ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
100	99	oveq1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( ( 𝐴 +s ( 𝐴 +s 1s ) ) -s 1s ) )
101	58 58	addscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 +s 𝐴 ) ∈ No )
102		pncans	⊢ ( ( ( 𝐴 +s 𝐴 ) ∈ No ∧ 1s ∈ No ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( 𝐴 +s 𝐴 ) )
103	101 45 102	sylancl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( 𝐴 +s 𝐴 ) )
104		no2times	⊢ ( 𝐴 ∈ No → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
105	58 104	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
106	103 105	eqtr4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( 2s ·s 𝐴 ) )
107	58 65 59	addsubsd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s ( 𝐴 +s 1s ) ) -s 1s ) = ( ( 𝐴 -s 1s ) +s ( 𝐴 +s 1s ) ) )
108	100 106 107	3eqtr3rd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) +s ( 𝐴 +s 1s ) ) = ( 2s ·s 𝐴 ) )
109	108	oveq1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) +s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
110	60 65 63	pw2divsdird	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) +s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
111		1n0s	⊢ 1s ∈ ℕ0s
112	111	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 1s ∈ ℕ0s )
113	58 61 112	pw2divscan4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( ( ( 2s ↑s 1s ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
114		exps1	⊢ ( 2s ∈ No → ( 2s ↑s 1s ) = 2s )
115	2 114	ax-mp	⊢ ( 2s ↑s 1s ) = 2s
116	115	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s 𝐴 ) = ( 2s ·s 𝐴 )
117	116	oveq1i	⊢ ( ( ( 2s ↑s 1s ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) )
118	113 117	eqtr2di	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 2s ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
119	109 110 118	3eqtr3d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
120	98 119	breqtrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
121	74 86 120	ssltsn	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( 𝐴 /su ( 2s ↑s 𝑛 ) ) } )
122	66 64	addscomd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
123	122 119	eqtrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
124	88	simp2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } <<s { ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) } )
125		ovex	⊢ ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ V
126	125	snid	⊢ ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) }
127	126	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
128	124 127 92	ssltsepcd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
129	64 73 66	sltadd2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ↔ ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
130	128 129	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
131	123 130	eqbrtrrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
132	86 75 131	ssltsn	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { ( 𝐴 /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
133	60 61 112	pw2divscan4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) = ( ( ( 2s ↑s 1s ) ·s ( 𝐴 -s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
134	115	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s ( 𝐴 -s 1s ) ) = ( 2s ·s ( 𝐴 -s 1s ) )
135		no2times	⊢ ( ( 𝐴 -s 1s ) ∈ No → ( 2s ·s ( 𝐴 -s 1s ) ) = ( ( 𝐴 -s 1s ) +s ( 𝐴 -s 1s ) ) )
136	60 135	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( 𝐴 -s 1s ) ) = ( ( 𝐴 -s 1s ) +s ( 𝐴 -s 1s ) ) )
137	134 136	eqtrid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 2s ↑s 1s ) ·s ( 𝐴 -s 1s ) ) = ( ( 𝐴 -s 1s ) +s ( 𝐴 -s 1s ) ) )
138	137	oveq1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 2s ↑s 1s ) ·s ( 𝐴 -s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( ( 𝐴 -s 1s ) +s ( 𝐴 -s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
139	60 60 63	pw2divsdird	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) +s ( 𝐴 -s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
140	133 138 139	3eqtrrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) )
141	64 73 64	sltadd2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) <s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ↔ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
142	128 141	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
143	140 142	eqbrtrrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
144		sltasym	⊢ ( ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No ∧ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ∈ No ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) → ¬ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
145	79 74 144	syl2anc	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) → ¬ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
146	143 145	mpd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ¬ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) )
147	74 79	ssltsnb	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ↔ ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
148	146 147	mtbird	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ¬ { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
149	148	intnanrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
150		ovex	⊢ ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ V
151		sneq	⊢ ( 𝑥𝑂 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) → { 𝑥𝑂 } = { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
152	151	breq2d	⊢ ( 𝑥𝑂 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ↔ { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
153	151	breq1d	⊢ ( 𝑥𝑂 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ↔ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
154	152 153	anbi12d	⊢ ( 𝑥𝑂 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ) )
155	154	notbid	⊢ ( 𝑥𝑂 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ) )
156	150 155	ralsn	⊢ ( ∀ 𝑥𝑂 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
157	149 156	sylibr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ∀ 𝑥𝑂 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
158	73 66 66	sltadd2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ) )
159	96 158	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
160	65 61 112	pw2divscan4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) = ( ( ( 2s ↑s 1s ) ·s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
161	115	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s ( 𝐴 +s 1s ) ) = ( 2s ·s ( 𝐴 +s 1s ) )
162		no2times	⊢ ( ( 𝐴 +s 1s ) ∈ No → ( 2s ·s ( 𝐴 +s 1s ) ) = ( ( 𝐴 +s 1s ) +s ( 𝐴 +s 1s ) ) )
163	65 162	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( 𝐴 +s 1s ) ) = ( ( 𝐴 +s 1s ) +s ( 𝐴 +s 1s ) ) )
164	161 163	eqtrid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 2s ↑s 1s ) ·s ( 𝐴 +s 1s ) ) = ( ( 𝐴 +s 1s ) +s ( 𝐴 +s 1s ) ) )
165	164	oveq1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 2s ↑s 1s ) ·s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( ( 𝐴 +s 1s ) +s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
166	65 65 63	pw2divsdird	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) +s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
167	160 165 166	3eqtrrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) )
168	159 167	breqtrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) )
169		sltasym	⊢ ( ( ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ∈ No ∧ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No ) → ( ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → ¬ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
170	75 80 169	syl2anc	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) <s ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → ¬ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
171	168 170	mpd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ¬ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
172	80 75	ssltsnb	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ↔ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) <s ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
173	171 172	mtbird	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ¬ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
174	173	intnand	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
175		ovex	⊢ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ V
176		sneq	⊢ ( 𝑥𝑂 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → { 𝑥𝑂 } = { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
177	176	breq2d	⊢ ( 𝑥𝑂 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ↔ { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
178	176	breq1d	⊢ ( 𝑥𝑂 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ↔ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
179	177 178	anbi12d	⊢ ( 𝑥𝑂 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ) )
180	179	notbid	⊢ ( 𝑥𝑂 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → ( ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ) )
181	175 180	ralsn	⊢ ( ∀ 𝑥𝑂 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
182	174 181	sylibr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ∀ 𝑥𝑂 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
183		ralunb	⊢ ( ∀ 𝑥𝑂 ∈ ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ↔ ( ∀ 𝑥𝑂 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ∧ ∀ 𝑥𝑂 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) ) )
184	157 182 183	sylanbrc	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ∀ 𝑥𝑂 ∈ ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ¬ ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
185	78 83 84 85 121 132 184	eqscut3	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } |s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
186		no2times	⊢ ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ No → ( 2s ·s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
187	73 186	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
188		eqidd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
189	72 72 188 188	addsunif	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) ) )
190		oveq1	⊢ ( 𝑏 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
191	190	eqeq2d	⊢ ( 𝑏 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ↔ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
192	125 191	rexsn	⊢ ( ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ↔ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
193	192	abbii	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
194	193	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
195		oveq2	⊢ ( 𝑏 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
196	195	eqeq2d	⊢ ( 𝑏 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) ↔ 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ) )
197	125 196	rexsn	⊢ ( ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) ↔ 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
198	73 64	addscomd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
199	198	eqeq2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ↔ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
200	197 199	bitrid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) ↔ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
201	200	abbidv	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
202	194 201	uneq12d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) = ( { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
203		unidm	⊢ ( { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
204		df-sn	⊢ { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
205	203 204	eqtr4i	⊢ ( { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) = { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
206	202 205	eqtrdi	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) = { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
207		oveq1	⊢ ( 𝑏 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
208	207	eqeq2d	⊢ ( 𝑏 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ↔ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
209	93 208	rexsn	⊢ ( ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ↔ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
210	209	abbii	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
211	210	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
212		oveq2	⊢ ( 𝑏 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
213	212	eqeq2d	⊢ ( 𝑏 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) → ( 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) ↔ 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ) )
214	93 213	rexsn	⊢ ( ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) ↔ 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
215	73 66	addscomd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
216	215	eqeq2d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ↔ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
217	214 216	bitrid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) ↔ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
218	217	abbidv	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
219	211 218	uneq12d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) = ( { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
220		unidm	⊢ ( { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
221		df-sn	⊢ { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } = { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
222	220 221	eqtr4i	⊢ ( { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ 𝑎 = ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) = { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) }
223	219 222	eqtrdi	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) = { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } )
224	206 223	oveq12d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( 𝑏 +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } 𝑎 = ( ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) +s 𝑏 ) } ) ) = ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } |s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
225	187 189 224	3eqtrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) = ( { ( ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } |s { ( ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) +s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) } ) )
226	2	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 2s ∈ No )
227	226 58 63	pw2divsassd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 2s ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
228	117 227	eqtr2id	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( ( ( 2s ↑s 1s ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
229	228 113	eqtr4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
230	185 225 229	3eqtr4rd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 2s ·s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
231	58 63	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
232		2ne0s	⊢ 2s ≠ 0s
233	232	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 2s ≠ 0s )
234	231 73 226 233	mulscan1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 2s ·s ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 2s ·s ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ↔ ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) )
235	230 234	mpbid	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) )
236	235	3exp	⊢ ( 𝑛 ∈ ℕ0s → ( 𝐴 ∈ ℤs → ( ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) → ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
237	236	a2d	⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ) ) )
238	13 22 31 40 56 237	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) ) )
239	238	impcom	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) )