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		2no	⊢ 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		zcuts	⊢ ( 𝐴 ∈ ℤs → 𝐴 = ( { ( 𝐴 -s 1s ) } |s { ( 𝐴 +s 1s ) } ) )
42		zno	⊢ ( 𝐴 ∈ ℤs → 𝐴 ∈ No )
43	42	divs1d	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = 𝐴 )
44		1no	⊢ 1s ∈ No
45	44	a1i	⊢ ( 𝐴 ∈ ℤs → 1s ∈ No )
46	42 45	subscld	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 -s 1s ) ∈ No )
47	46	divs1d	⊢ ( 𝐴 ∈ ℤs → ( ( 𝐴 -s 1s ) /su 1s ) = ( 𝐴 -s 1s ) )
48	47	sneqd	⊢ ( 𝐴 ∈ ℤs → { ( ( 𝐴 -s 1s ) /su 1s ) } = { ( 𝐴 -s 1s ) } )
49	42 45	addscld	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 +s 1s ) ∈ No )
50	49	divs1d	⊢ ( 𝐴 ∈ ℤs → ( ( 𝐴 +s 1s ) /su 1s ) = ( 𝐴 +s 1s ) )
51	50	sneqd	⊢ ( 𝐴 ∈ ℤs → { ( ( 𝐴 +s 1s ) /su 1s ) } = { ( 𝐴 +s 1s ) } )
52	48 51	oveq12d	⊢ ( 𝐴 ∈ ℤs → ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) = ( { ( 𝐴 -s 1s ) } |s { ( 𝐴 +s 1s ) } ) )
53	41 43 52	3eqtr4d	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = ( { ( ( 𝐴 -s 1s ) /su 1s ) } |s { ( ( 𝐴 +s 1s ) /su 1s ) } ) )
54		simp2	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝐴 ∈ ℤs )
55	54	znod	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝐴 ∈ No )
56	44	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 1s ∈ No )
57	55 56	subscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 -s 1s ) ∈ No )
58		simp1	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝑛 ∈ ℕ0s )
59		peano2n0s	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) ∈ ℕ0s )
60	58 59	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
61	57 60	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 )
62	55 56	addscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 +s 1s ) ∈ No )
63	62 60	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 )
64	55	ltsm1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 -s 1s ) <s 𝐴 )
65	55	ltsp1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 𝐴 <s ( 𝐴 +s 1s ) )
66	57 55 62 64 65	ltstrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 -s 1s ) <s ( 𝐴 +s 1s ) )
67	57 62 60	pw2ltsdiv1d	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) ) )
68	66 67	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 ) ) ) )
69	61 63 68	sltssn	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } )
70	69	cutscld	⊢ ( ( 𝑛 ∈ ℕ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 )
71	61 70	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 )
72	63 70	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 )
73	61 63 70	ltadds1d	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) ) ) )
74	68 73	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 ) ) ) } ) ) )
75	71 72 74	sltssn	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) ) } )
76	57 58	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No )
77	62 58	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No )
78	57 62 58	pw2ltsdiv1d	⊢ ( ( 𝑛 ∈ ℕ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 𝑛 ) ) ) )
79	66 78	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 𝑛 ) ) )
80	76 77 79	sltssn	⊢ ( ( 𝑛 ∈ ℕ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 𝑛 ) ) } )
81		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 ) ) ) } ) ) } ) )
82		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 𝑛 ) ) } ) )
83	55 58	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) ∈ No )
84		cutcuts	⊢ ( { ( ( 𝐴 -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 ) ) ) } ) )
85	69 84	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 ) ) ) } ) )
86	85	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 ) ) ) } )
87		ovex	⊢ ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } ) ∈ V
88	87	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 ) ) ) } ) }
89	88	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 ) ) ) } ) } )
90		ovex	⊢ ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ V
91	90	snid	⊢ ( ( 𝐴 +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ { ( ( 𝐴 +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 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) } )
93	86 89 92	sltssepcd	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) )
94	70 63 61	ltadds2d	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) ) ) )
95	93 94	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 ) ) ) ) )
96	55 55 56	addsassd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 +s 𝐴 ) +s 1s ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
97	96	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 ) )
98	55 55	addscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 +s 𝐴 ) ∈ No )
99		pncans	⊢ ( ( ( 𝐴 +s 𝐴 ) ∈ No ∧ 1s ∈ No ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( 𝐴 +s 𝐴 ) )
100	98 44 99	sylancl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( 𝐴 +s 𝐴 ) )
101		no2times	⊢ ( 𝐴 ∈ No → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
102	55 101	syl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
103	100 102	eqtr4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( ( 𝐴 +s 𝐴 ) +s 1s ) -s 1s ) = ( 2s ·s 𝐴 ) )
104	55 62 56	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 ) ) )
105	97 103 104	3eqtr3rd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( ( 𝐴 -s 1s ) +s ( 𝐴 +s 1s ) ) = ( 2s ·s 𝐴 ) )
106	105	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 ) ) ) )
107	57 62 60	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 ) ) ) ) )
108		1n0s	⊢ 1s ∈ ℕ0s
109	108	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 1s ∈ ℕ0s )
110	55 58 109	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 ) ) ) )
111		exps1	⊢ ( 2s ∈ No → ( 2s ↑s 1s ) = 2s )
112	2 111	ax-mp	⊢ ( 2s ↑s 1s ) = 2s
113	112	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s 𝐴 ) = ( 2s ·s 𝐴 )
114	113	oveq1i	⊢ ( ( ( 2s ↑s 1s ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ·s 𝐴 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) )
115	110 114	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 𝑛 ) ) )
116	106 107 115	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 𝑛 ) ) )
117	95 116	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 𝑛 ) ) )
118	71 83 117	sltssn	⊢ ( ( 𝑛 ∈ ℕ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 𝑛 ) ) } )
119	63 61	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 ) ) ) ) )
120	119 116	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 𝑛 ) ) )
121	85	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 ) ) ) } ) } )
122		ovex	⊢ ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ V
123	122	snid	⊢ ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ { ( ( 𝐴 -s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) }
124	123	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 ) ) ) } )
125	121 124 89	sltssepcd	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) )
126	61 70 63	ltadds2d	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) ) ) )
127	125 126	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 ) ) ) } ) ) )
128	120 127	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 ) ) ) } ) ) )
129	83 72 128	sltssn	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) ) } )
130	57 58 109	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 ) ) ) )
131	112	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s ( 𝐴 -s 1s ) ) = ( 2s ·s ( 𝐴 -s 1s ) )
132		no2times	⊢ ( ( 𝐴 -s 1s ) ∈ No → ( 2s ·s ( 𝐴 -s 1s ) ) = ( ( 𝐴 -s 1s ) +s ( 𝐴 -s 1s ) ) )
133	57 132	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 ) ) )
134	131 133	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 ) ) )
135	134	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 ) ) ) )
136	57 57 60	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 ) ) ) ) )
137	130 135 136	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 𝑛 ) ) )
138	61 70 61	ltadds2d	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) ) ) )
139	125 138	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 ) ) ) } ) ) )
140	137 139	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 ) ) ) } ) ) )
141		ltsasym	⊢ ( ( ( ( 𝐴 -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 𝑛 ) ) ) )
142	76 71 141	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 𝑛 ) ) ) )
143	140 142	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 𝑛 ) ) )
144	71 76	sltssnb	⊢ ( ( 𝑛 ∈ ℕ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 𝑛 ) ) ) )
145	143 144	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 𝑛 ) ) } )
146	145	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 ) ) ) } ) ) } ) )
147		ovex	⊢ ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ V
148		sneq	⊢ ( 𝑥𝑂 = ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) → { 𝑥𝑂 } = { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
149	148	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 𝑛 ) ) } ) )
150	148	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 ) ) ) } ) ) } ) )
151	149 150	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 ) ) ) } ) ) } ) ) )
152	151	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 ) ) ) } ) ) } ) ) )
153	147 152	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 ) ) ) } ) ) } ) )
154	146 153	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 ) ) ) } ) ) } ) )
155	70 63 63	ltadds2d	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) ) ) )
156	93 155	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 ) ) ) ) )
157	62 58 109	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 ) ) ) )
158	112	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s ( 𝐴 +s 1s ) ) = ( 2s ·s ( 𝐴 +s 1s ) )
159		no2times	⊢ ( ( 𝐴 +s 1s ) ∈ No → ( 2s ·s ( 𝐴 +s 1s ) ) = ( ( 𝐴 +s 1s ) +s ( 𝐴 +s 1s ) ) )
160	62 159	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 ) ) )
161	158 160	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 ) ) )
162	161	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 ) ) ) )
163	62 62 60	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 ) ) ) ) )
164	157 162 163	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 𝑛 ) ) )
165	156 164	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 𝑛 ) ) )
166		ltsasym	⊢ ( ( ( ( ( 𝐴 +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 ) ) ) } ) ) ) )
167	72 77 166	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 ) ) ) } ) ) ) )
168	165 167	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 ) ) ) } ) ) )
169	77 72	sltssnb	⊢ ( ( 𝑛 ∈ ℕ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 ) ) ) } ) ) ) )
170	168 169	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 ) ) ) } ) ) } )
171	170	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 ) ) ) } ) ) } ) )
172		ovex	⊢ ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ V
173		sneq	⊢ ( 𝑥𝑂 = ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) → { 𝑥𝑂 } = { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
174	173	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 𝑛 ) ) } ) )
175	173	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 ) ) ) } ) ) } ) )
176	174 175	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 ) ) ) } ) ) } ) ) )
177	176	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 ) ) ) } ) ) } ) ) )
178	172 177	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 ) ) ) } ) ) } ) )
179	171 178	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 ) ) ) } ) ) } ) )
180		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 ) ) ) } ) ) } ) ) )
181	154 179 180	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 ) ) ) } ) ) } ) )
182	75 80 81 82 118 129 181	eqcuts3	⊢ ( ( 𝑛 ∈ ℕ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 𝑛 ) ) )
183		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 ) ) ) } ) ) )
184	70 183	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 ) ) ) } ) ) )
185		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 ) ) ) } ) )
186	69 69 185 185	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 𝑏 ) } ) ) )
187		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 ) ) ) } ) ) )
188	187	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 ) ) ) } ) ) ) )
189	122 188	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 ) ) ) } ) ) )
190	189	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 ) ) ) } ) ) }
191	190	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 ) ) ) } ) ) } )
192		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 ) ) ) ) )
193	192	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 ) ) ) ) ) )
194	122 193	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 ) ) ) ) )
195	70 61	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 ) ) ) } ) ) )
196	195	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 ) ) ) } ) ) ) )
197	194 196	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 ) ) ) } ) ) ) )
198	197	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 ) ) ) } ) ) } )
199	191 198	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 ) ) ) } ) ) } ) )
200		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 ) ) ) } ) ) }
201		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 ) ) ) } ) ) }
202	200 201	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 ) ) ) } ) ) }
203	199 202	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 ) ) ) } ) ) } )
204		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 ) ) ) } ) ) )
205	204	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 ) ) ) } ) ) ) )
206	90 205	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 ) ) ) } ) ) )
207	206	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 ) ) ) } ) ) }
208	207	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 ) ) ) } ) ) } )
209		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 ) ) ) ) )
210	209	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 ) ) ) ) ) )
211	90 210	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 ) ) ) ) )
212	70 63	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 ) ) ) } ) ) )
213	212	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 ) ) ) } ) ) ) )
214	211 213	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 ) ) ) } ) ) ) )
215	214	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 ) ) ) } ) ) } )
216	208 215	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 ) ) ) } ) ) } ) )
217		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 ) ) ) } ) ) }
218		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 ) ) ) } ) ) }
219	217 218	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 ) ) ) } ) ) }
220	216 219	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 ) ) ) } ) ) } )
221	203 220	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 ) ) ) } ) ) } ) )
222	184 186 221	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 ) ) ) } ) ) } ) )
223	2	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 2s ∈ No )
224	223 55 60	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 ) ) ) ) )
225	114 224	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 ) ) ) )
226	225 110	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 𝑛 ) ) )
227	182 222 226	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 ) ) ) } ) ) )
228	55 60	pw2divscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → ( 𝐴 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
229		2ne0s	⊢ 2s ≠ 0s
230	229	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ ℤs ∧ ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) → 2s ≠ 0s )
231	228 70 223 230	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 ) ) ) } ) ) )
232	227 231	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 ) ) ) } ) )
233	232	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 ) ) ) } ) ) ) )
234	233	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 ) ) ) } ) ) ) )
235	13 22 31 40 53 234	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ ℤs → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) ) )
236	235	impcom	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( { ( ( 𝐴 -s 1s ) /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) )